diff --git a/idris-common-utils.el b/idris-common-utils.el
index 3b8b803..4872bb2 100644
--- a/idris-common-utils.el
+++ b/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)))
diff --git a/idris-repl.el b/idris-repl.el
index 785881d..b6d5845 100644
--- a/idris-repl.el
+++ b/idris-repl.el
@@ -186,9 +186,14 @@ If ALWAYS-INSERT is non-nil, always insert a prompt at the end of the buffer."
       (idris-repl-insert-prompt)
       (insert current-input))))
 
+(autoload 'idris-load-file-sync "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 (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)))
 
@@ -199,7 +204,8 @@ If ALWAYS-INSERT is non-nil, always insert a prompt at the end of the buffer."
 (defun idris-repl ()
   (interactive)
   (idris-run)
-  (idris-switch-to-repl))
+  (pop-to-buffer (idris-repl-buffer))
+  (goto-char (point-max)))
 
 (defvar idris-repl-mode-map
   (let ((map (make-sparse-keymap)))