diff --git a/generic/pg-goals.el b/generic/pg-goals.el index f7cb9b3c7..e5e79ef8c 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -79,6 +79,63 @@ May enable proof-by-pointing or similar features. ;; ;; Goals buffer processing ;; + +;; update *goals* buffer modeline +(defun coq-parse-goals-info (goals-output) + "Parse output to extract and update goals information in modeline." + (let ((goals-count-regexp "^\\([0-9]+\\) goals? (ID \\([0-9]+\\))") + (num-goals 0) + (current-goal-id nil)) + (when (string-match goals-count-regexp goals-output) + (setq num-goals (string-to-number (match-string 1 goals-output))) + (setq current-goal-id (match-string 2 goals-output))) + (update-goals-modeline num-goals current-goal-id) + ; hide goals info on first line + (with-current-buffer proof-goals-buffer + (goto-char (point-min)) + (let ((line-end (line-end-position))) + (let ((overlay (make-overlay (point-min) line-end))) + ; invisible line + (overlay-put overlay 'invisible t)))))) + +(defun update-goals-modeline (goal id) + "Extracts proof state and updates the goals buffer modeline dynamically." + (with-current-buffer proof-goals-buffer + (let ((goal-str (if (> goal 1) "goals" "goal"))) + (setq-local my-goals-info + (format "%d %s, ID: %s" goal goal-str id))) + (let ((baseline-mode-line-format + '("%e" + mode-line-front-space + mode-line-mule-info + mode-line-client + mode-line-modified + mode-line-remote + mode-line-frame-identification + mode-line-buffer-identification + " " + mode-line-position + " " + mode-line-modes + mode-line-misc-info + mode-line-end-spaces))) + + (setq-local mode-line-format + (append baseline-mode-line-format + `((" " (:eval my-goals-info))))) ; update + + (force-mode-line-update)))) + +(defun reset-goals-modeline () + "Resets the *goals* buffer modeline to indicate no active proof." + (with-current-buffer proof-goals-buffer + (setq-local my-goals-info "") + (setq-local mode-line-format + (append + '("%e" mode-line-front-space mode-line-mule-info mode-line-client mode-line-modified mode-line-remote mode-line-frame-identification mode-line-buffer-identification " " mode-line-position " " mode-line-modes mode-line-misc-info mode-line-end-spaces) + `((" " (:eval my-goals-info))))) + (force-mode-line-update))) + (defun pg-goals-display (string keepresponse) "Display STRING in the `proof-goals-buffer', properly marked up. Converts term substructure markup into mouse-highlighted extents. @@ -98,6 +155,9 @@ so the response buffer should not be cleared." ;; window. Indicate it should be erased before the next output. (pg-response-maybe-erase t t nil keepresponse) + ;; ;; commit modif + ;; (reset-goals-modeline) + ;; Erase the goals buffer and add in the new string (with-current-buffer proof-goals-buffer @@ -106,13 +166,15 @@ so the response buffer should not be cleared." (unless (eq 0 (buffer-size)) (bufhist-checkpoint-and-erase)) - ;; Only display if string is non-empty. - (unless (string-equal string "") - (funcall pg-insert-text-function string)) + ;; Display the string only if it's non-empty. + ;; In that case, parse and update goals information in string. + (when (not (string-equal string "")) + (funcall pg-insert-text-function string) + (coq-parse-goals-info string)) (setq buffer-read-only t) (set-buffer-modified-p nil) - + ;; Keep point at the start of the buffer. (proof-display-and-keep-buffer proof-goals-buffer (point-min)))) diff --git a/generic/proof-script.el b/generic/proof-script.el index 854bd6bf8..07212e060 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1486,6 +1486,7 @@ Besides stuff that is not yet documented here, this function and sections. - enters some commands and their spans in some database (with for me unknown purpose)" + (reset-goals-modeline) ; Erase goal buffer when a proof is closed (unless (or (eq proof-shell-proof-completed 1) ;; (eq proof-assistant-symbol 'isar) ) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index a3f8ae39c..ba26ffb61 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -870,7 +870,8 @@ after a completed proof." (proof-shell-exec-loop)) ((proof-re-search-forward-safe proof-shell-proof-completed-regexp end t) - (setq proof-shell-proof-completed 0))) ; commands since complete + (setq proof-shell-proof-completed 0))) + ;; (reset-goals-modeline))) ; commands since complete ;; PG4.0 change: simplify and run earlier (if proof-shell-handle-output-system-specific @@ -1788,7 +1789,10 @@ i.e., 'goals or 'response." gmark)) (rstart start) ; possible response before goals (gend end) - both) ; flag for response+goals + both + (proof-termination-regexp + (concat "\\(" coq-proof-end-regexp "\\|" + coq-definition-end-regexp "\\)"))) ;flag for response+goals (goto-char gstart) (while (re-search-forward proof-shell-start-goals-regexp end t) diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 148ff3871..d4f6d9c74 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -407,7 +407,6 @@ a proof. Therefore, if non-nil, this variable must either hold a nonempty list (the to be delayed action items) or t (if there are no action items to be delayed.") - ;;; Missing in the library (defun list-pred-partition (p l) @@ -422,7 +421,8 @@ that takes one argument." (if (funcall p x) (push x yes) (push x no))))) - + + ;; ;; process filter function that receives prooftree output ;; @@ -894,7 +894,6 @@ current buffer." (list sequent-id sequent-text additional-goal-ids)) nil)) - (defun proof-tree-extract-existential-info (start end) "Extract the information display of existential variables. This function cuts out the text between @@ -982,7 +981,6 @@ The delayed output of the navigation command is in the region ;; send all to prooftree (proof-tree-send-switch-goal proof-state proof-name current-id))))) - (defun proof-tree-handle-proof-command (old-proof-marker cmd proof-info) "Display current goal in prooftree unless CMD should be ignored." ;; (message "PTHPC") @@ -998,7 +996,7 @@ The delayed output of the navigation command is in the region (proof-tree-handle-proof-progress old-proof-marker cmd-string proof-info))) (setq proof-tree-last-state (car proof-info)))) - + (defun proof-tree-handle-undo (proof-info) "Undo prooftree to current state." ;; (message "PTHU info %s" proof-info) @@ -1016,7 +1014,6 @@ The delayed output of the navigation command is in the region (proof-tree-send-undo proof-state)) (setq proof-tree-last-state proof-state))) - (defun proof-tree-update-sequent (proof-name) "Prepare an update-sequent command for prooftree. This function processes delayed output that the proof assistant @@ -1072,6 +1069,20 @@ the flags and SPAN is the span." (unless (or (memq 'invisible flags) (memq 'proof-tree-show-subgoal flags)) (let* ((proof-info (funcall proof-tree-get-proof-info)) (current-proof-name (cadr proof-info))) + +;; commit first issue + (save-excursion + (goto-char proof-shell-delayed-output-start) + (when (re-search-forward proof-tree-current-goal-regexp proof-shell-delayed-output-end t) + (let ((goal (match-string-no-properties 1)) + (id (match-string-no-properties 2)) + (shelved (match-string-no-properties 3))) + ;; Now call the update function with extracted information + (update-goals-modeline goal id shelved)))) + +;; + + (save-excursion (if (< (car proof-info) proof-tree-last-state) ;; went back to some old state: there must have been an undo command