Minor Fixes in the Emacs extension

editors/emacs/CHANGES.md

@@ -0,0 +1,16 @@
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/),
+and this project adheres to [Semantic Versioning](https://semver.org/).
+
+## Unreleased
+
+### Added
+- Auto scroll to the first goal in the `Goals` buffer in case of many hypothesis
+- Check that the Goals and Logs buffers are displayed before displaying logs and goals 
+
+### Fixed
+- Show the error at the end of file if any. That was not working because navigation stoped at the location of last command and not further (see issue #1111)
+
+
+### Changed

editors/emacs/lambdapi-proofs.el

@@ -129,10 +129,20 @@ This works for both graphical and text displays."
             (erase-buffer)
             (goto-char (point-max))
             (mapc 'insert hypsstr)
+            (setq saved-point (point))
             (mapc (lambda (gstr)
                     (lp--draw-horizontal-line)
                     (insert gstr))
-                  goalsstr))
+                  goalsstr)
+
+            (let ((goalswin (get-buffer-window goalsbuf)))
+              (if goalswin
+                  (with-selected-window goalswin
+                    (goto-char (+ 1 saved-point))
+                    (beginning-of-line)
+                    (recenter -1))))
+
+                  )
         (remove-overlays)
         (erase-buffer)
         (insert "No goals"))
@@ -174,6 +184,7 @@ This works for both graphical and text displays."
         (let ((response (jsonrpc-request server :proof/goals params)))
           (if response
               (progn
+                (lambdapi-refresh-window-layout)
                 (lp-display-goals (plist-get response :goals))
                 (lp-display-logs (plist-get response :logs)))
             (let ((goalsbuf (get-buffer-create "*Goals*"))
@@ -330,7 +341,7 @@ and 0 if there is no previous command."
 
 (defun lp--next-command-pos (&optional pos)
   "Return the position of the next command's terminator
-and POS if there is no next command"
+and (point-max) if there is no next command to display the last error in logs"
   (setq npos (1+ (or pos (point))))
   (save-excursion
     (let ((term-regex
@@ -343,7 +354,7 @@ and POS if there is no next command"
             (setq npos (re-search-forward term-regex nil t))
             (and npos (lp--in-comment-p npos)))
         (goto-char npos))
-      (if npos (max (point-min) (1- npos)) pos))))
+      (if npos (max (point-min) (1- npos)) (point-max)))))
 
 (defun lp--post-self-insert-function ()
   (save-excursion