Check for idr and lidr file in idris-switch-to-repl

Author: keram

idris-common-utils.el

@@ -365,15 +365,15 @@ corresponding values in the CDR of VALUE."
                '()
              `((t (error "ELISP destructure-case failed: %S" ,tmp))))))))
 
+(defun idris-idr-p (&optional buffer)
+  "Return t if BUFFER is an Idris file (.idr)."
+  (if-let* ((file-name (buffer-file-name buffer)))
+      (string-equal (downcase (file-name-extension file-name)) "idr")))
+
 (defun idris-lidr-p (&optional buffer)
-  "Return t if BUFFER is a literate Idris file, or nil otherwise.
-Use the current buffer if BUFFER is not supplied or is nil."
-  (let ((file-name (buffer-file-name buffer)))
-    ;; We check for nil here because idris-lidr-p might be called on
-    ;; buffers that don't have associated files, such as the REPL
-    ;; buffer or an info buffer
-    (and (stringp file-name)
-         (string= (file-name-extension file-name) "lidr"))))
+  "Return t if BUFFER is a literate Idris file (.lidr)."
+  (if-let* ((file-name (buffer-file-name buffer)))
+      (string-equal (downcase (file-name-extension file-name)) "lidr")))
 
 (defun idris-make-file-link-overlay (start end keymap help-echo)
   (let ((overlay (make-overlay start end)))

idris-repl.el

@@ -189,13 +189,11 @@ If ALWAYS-INSERT is non-nil, always insert a prompt at the end of the buffer."
 (autoload 'idris-load-file "idris-commands.el")
 ;;;###autoload
 (defun idris-switch-to-repl ()
-  "Select the output buffer and scroll to bottom."
+  "Load the current Idris file buffer and jump to the Idris REPL."
   (interactive)
-  (if (and buffer-file-name
-           ;; in Emacs 29.1 > we can use string-equal-ignore-case
-           (string= "idr" (downcase (file-name-extension buffer-file-name))))
-      (idris-load-file)
-    (user-error "This command can only be run from a buffer visiting an Idris `.idr' file"))
+  (if (or (idris-idr-p) (idris-lidr-p))
+      (idris-load-file-sync)
+    (user-error "This command can only be run from a buffer visiting an Idris `.idr' or `.lidr' file"))
   (pop-to-buffer (idris-repl-buffer))
   (goto-char (point-max)))