- support bullets and braces in Prooftree

- prooftree protocol change to version 3

6 files changed, 84 insertions, 42 deletions

diff --git a/CHANGES b/CHANGES
index 8dd018e8..55034825 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,12 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
 
 * Changes of Proof General 4.3 from Proof General 4.2
 
+** Generic/misc changes
+
+*** Require Prooftree version 0.11
+    Check the Prooftree website to see which other versions of
+    Prooftree are compatible with Proof General 4.3.
+
 ** Coq changes
 
 *** Asynchronous parallel compilation of required modules
@@ -15,6 +21,7 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
     to compile modules in parallel in the background while Proof
     General stays responsive.
 
+*** Support for bullets and braces for Prooftree.
 
 * Changes of Proof General 4.2 from Proof General 4.1
 
diff --git a/coq/coq.el b/coq/coq.el
index 89a380ce..b0906f65 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -190,7 +190,8 @@ See also `coq-hide-additional-subgoals'."
   :group 'coq-proof-tree)
 
 (defcustom coq-navigation-command-regexp
-  "^\\(Focus\\)\\|\\(Unfocus\\)"
+  (concat "^\\(\\(Focus\\)\\|\\(Unfocus\\)\\|"
+          "\\(\\+\\)\\|\\(-\\)\\|\\(\\*\\)\\|\\({\\)\\|\\(}\\)\\)")
   "Regexp for `proof-tree-navigation-command-regexp'."
   :type 'regexp
   :group 'coq-proof-tree)
@@ -203,8 +204,8 @@ See also `coq-hide-additional-subgoals'."
 
 (defcustom coq-proof-tree-current-goal-regexp
   (concat "^[0-9]+ \\(?:focused \\)?subgoal\\(?:s\\)?"
-          "\\(?: (unfocused: [0-9]+)\\)?\\(?:\\s-*, subgoal 1\\)? "
-          "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)")
+          "\\(?: (unfocused: [-0-9]+)\\)?\\(?:\\s-*, subgoal 1\\)? "
+          "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?: .*\n\\)+\\)\\(?:\n\\|$\\)")
   "Regexp for `proof-tree-current-goal-regexp'."
   :type 'regexp
   :group 'coq-proof-tree)
@@ -244,9 +245,13 @@ See also `coq-hide-additional-subgoals'."
   :type 'regexp
   :group 'coq-proof-tree)
 
-(defcustom coq-proof-tree-proof-finished-regexp
-  "^\\(?:Proof completed\\)\\|\\(?:No more subgoals\\)\\."
-  "Regexp for `proof-tree-proof-finished-regexp'."
+(defcustom coq-proof-tree-branch-finished-regexp
+  (concat "^\\(\\(?:Proof completed\\.\\)\\|\\(?:No more subgoals\\.\\)\\|"
+          "\\(No more subgoals but non-instantiated "
+          "existential variables:\\)\\|"
+          "\\(<infomsg>This subproof is complete, but there are "
+          "still unfocused goals.</infomsg>\\)\\)")
+  "Regexp for `proof-tree-branch-finished-regexp'."
   :type 'regexp
   :group 'coq-proof-tree)
 
@@ -1195,7 +1200,7 @@ flag Printing All set."
                         coq-proof-tree-existentials-state-end-regexp
    proof-tree-additional-subgoal-ID-regexp
                               coq-proof-tree-additional-subgoal-ID-regexp
-   proof-tree-proof-finished-regexp coq-proof-tree-proof-finished-regexp
+   proof-tree-branch-finished-regexp coq-proof-tree-branch-finished-regexp
    proof-tree-extract-instantiated-existentials
      'coq-extract-instantiated-existentials
    proof-tree-show-sequent-command 'coq-show-sequent-command
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index f5149df8..58119672 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3081,7 +3081,16 @@ Query the prover about the identifier near mouse click @var{event}.
 Since version 4.2, Proof General supports proof-tree
 visualization on graphical desktops via the additional program
 Prooftree. Currently, proof-tree visualization is only supported
-for the Coq proof assistant. For installation instructions and
+for the Coq proof assistant. 
+
+This version of Proof General requires Prooftree version 0.11.
+Check the @uref{http://askra.de/software/prooftree/, Prooftree website},
+to see if some later versions are also compatible. (Because of
+the communication protocol, Proof General is always only
+compatible with certain versions of Prooftree.)
+
+
+For installation instructions and
 more detailed information about Prooftree, please refer to the
 @uref{http://askra.de/software/prooftree/, Prooftree website} and
 the @uref{http://askra.de/software/prooftree/prooftree.man.html,
@@ -4879,10 +4888,13 @@ you want to save abbrevs; answer yes.
 
 Starting with Proof General version 4.2 and Coq version 8.4, Coq
 Proof General has full support for proof-tree visualization, 
-@pxref{Graphical Proof-Tree Visualization}.
+@pxref{Graphical Proof-Tree Visualization}. To find out which
+versions of Prooftree are compatible with this version of Proof
+General, @pxref{Graphical Proof-Tree Visualization} or the 
+@uref{http://askra.de/software/prooftree/, Prooftree website}.
 
-Proof-tree visualization does currently neither support bullets
-and braces nor the command ``Grab Existential Variables''.
+Proof-tree visualization does currently not support the command
+``Grab Existential Variables''.
 
 For the visualization to work properly, proofs must be started
 with ``Proof.'', which is encouraged practice anyway (see Coq Bug
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index c304f61d..cc7e56f8 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1513,7 +1513,8 @@ After processing the current output, the last step undertaken
 by the filter is to send the next command from the queue."
   (let ((span  (caar proof-action-list))
 	(cmd   (nth 1 (car proof-action-list)))
-	(flags (nth 3 (car proof-action-list))))
+	(flags (nth 3 (car proof-action-list)))
+	(old-proof-marker (marker-position proof-marker)))
 
     ;; A copy of the last message, verbatim, never modified.
     (setq proof-shell-last-output
@@ -1532,7 +1533,7 @@ by the filter is to send the next command from the queue."
 		(proof-shell-handle-delayed-output)))
       ;; send output to the proof tree visualizer
       (if proof-tree-external-display
-	  (proof-tree-handle-delayed-output cmd flags span)))))
+	  (proof-tree-handle-delayed-output old-proof-marker cmd flags span)))))
 
 
 (defsubst proof-shell-display-output-as-response (flags str)
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index b73c2308..969dce05 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -211,8 +211,13 @@ the state display expands to the end of the prover output."
   :type '(choice regexp (const nil))
   :group 'proof-tree-internals)
 
-(defcustom proof-tree-proof-finished-regexp nil
-  "Regexp to match the no-more-subgoals message."
+(defcustom proof-tree-branch-finished-regexp nil
+  "Regexp to recognize that the current branch has been finished.
+This must match in precisely the following cases:
+- The current branch has been finished but there is no current
+  open subgoal because the prover has not switched to the next
+  subgoal.
+- The last open goal has been proved. "
   :type 'regexp
   :group 'proof-tree-internals)
 
@@ -472,7 +477,7 @@ variables."
 ;; Low-level communication primitives
 ;;
 
-(defconst proof-tree-protocol-version 2
+(defconst proof-tree-protocol-version 3
   "Version of the communication protocol between Proof General and Prooftree.
 Must be increased if one of the low-level communication
 primitives is changed.")
@@ -547,12 +552,12 @@ DATA as data sections to Prooftree."
 		 (1+ (string-bytes proof-name)))))
     (proof-tree-send-message second-line (list proof-name))))
 
-(defun proof-tree-send-proof-finished (state proof-name cmd-string
+(defun proof-tree-send-branch-finished (state proof-name cmd-string
 					     cheated-flag existential-info)
-  "Send proof-finished to prooftree."
+  "Send branch-finished to prooftree."
   (proof-tree-send-message
    (format
-    (concat "proof-finished state %d %s proof-name-bytes %d command-bytes %d "
+    (concat "branch-finished state %d %s proof-name-bytes %d command-bytes %d "
 	    "existential-bytes %d")
     state
     (if cheated-flag "cheated" "not-cheated")
@@ -820,6 +825,7 @@ This function cuts out the text between
 output, including the matches of these regular expressions. If
 the start regexp is nil, the empty string is returned. If the end
 regexp is nil, the match expands to the end of the prover output."
+  (goto-char start)
   (if (and proof-tree-existentials-state-start-regexp
 	   (proof-re-search-forward proof-tree-existentials-state-start-regexp
 				    end t))
@@ -832,7 +838,7 @@ regexp is nil, the match expands to the end of the prover output."
 	(buffer-substring-no-properties start end))
     ""))
 
-(defun proof-tree-handle-proof-progress (cmd-string proof-info)
+(defun proof-tree-handle-proof-progress (old-proof-marker cmd-string proof-info)
   "Send CMD-STRING and goals in delayed output to prooftree.
 This function is called if there is some real progress in a
 proof. This function sends the current state, the current goal
@@ -840,9 +846,13 @@ and the list of additional open subgoals to Prooftree. Prooftree
 will sort out the rest.
 
 The delayed output is in the region
-\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
-  ;; (message "PTHPO cmd |%s| info %s flags %s start %s end %s"
+\[proof-shell-delayed-output-start, proof-shell-delayed-output-end].
+Urgent messages might be before that, following OLD-PROOF-MARKER,
+which contains the position of `proof-marker', before the next
+command was sent to the proof assistant."
+  ;; (message "PTHPO cmd |%s| info %s flags %s proof-marker %s start %s end %s"
   ;; 	   cmd proof-info flags
+  ;; 	   old-proof-marker
   ;; 	   proof-shell-delayed-output-start
   ;; 	   proof-shell-delayed-output-end)
   (let* ((start proof-shell-delayed-output-start)
@@ -852,10 +862,17 @@ The delayed output is in the region
 	 (cheated-flag
 	  (and proof-tree-cheating-regexp
 	       (proof-string-match proof-tree-cheating-regexp cmd-string)))
-	 (current-goals (proof-tree-extract-goals start end))
-	 (existential-info
-	  (proof-tree-extract-existential-info start end)))
-    (if current-goals
+	 current-goals)
+    ;; Check first for special cases, because Coq's output for finished
+    ;; branches is almost identical to proper goals.
+    (goto-char old-proof-marker)
+    (if (proof-re-search-forward proof-tree-branch-finished-regexp end t)
+	(proof-tree-send-branch-finished
+	 proof-state proof-name cmd-string cheated-flag
+	 (proof-tree-extract-existential-info start end))
+      (goto-char start)
+      (setq current-goals (proof-tree-extract-goals start end))
+      (when current-goals
 	(let ((current-sequent-id (car current-goals))
 	      (current-sequent-text (nth 1 current-goals))
 	      ;; nth 2 current-goals  contains the  additional ID's
@@ -867,21 +884,13 @@ The delayed output is in the region
 	   current-sequent-id
 	   current-sequent-text
 	   (nth 2 current-goals)
-	   existential-info)
+	   (proof-tree-extract-existential-info start end))
 	  ;; put current sequent into hash (if it is not there yet)
 	  (unless (gethash current-sequent-id proof-tree-sequent-hash)
 	    (puthash current-sequent-id proof-state proof-tree-sequent-hash))
 	  (proof-tree-register-existentials proof-state
 					    current-sequent-id
-					    current-sequent-text))
-      
-      ;; no current goal found, maybe the proof has been finished?
-      (goto-char start)
-      (if (proof-re-search-forward proof-tree-proof-finished-regexp end t)
-	  (progn
-	    (proof-tree-send-proof-finished
-	     proof-state proof-name cmd-string
-	     cheated-flag existential-info))))))
+					    current-sequent-text))))))
 
 (defun proof-tree-handle-navigation (proof-info)
   "Handle a navigation command.
@@ -901,7 +910,7 @@ The delayed output of the navigation command is in the region
 	  (proof-tree-send-switch-goal proof-state proof-name current-id)))))
 
 
-(defun proof-tree-handle-proof-command (cmd proof-info)
+(defun proof-tree-handle-proof-command (old-proof-marker cmd proof-info)
   "Display current goal in prooftree unless CMD should be ignored."
   ;; (message "PTHPC")
   (let ((proof-state (car proof-info))
@@ -913,7 +922,8 @@ The delayed output of the navigation command is in the region
 	       (proof-string-match proof-tree-navigation-command-regexp
 				   cmd-string))
 	  (proof-tree-handle-navigation proof-info)
-	(proof-tree-handle-proof-progress cmd-string proof-info)))
+	(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)
@@ -989,13 +999,19 @@ The delayed output is in the region
 						  sequent-text)))))))
 
 
-(defun proof-tree-handle-delayed-output (cmd flags span)
+(defun proof-tree-handle-delayed-output (old-proof-marker cmd flags span)
   "Process delayed output for prooftree.
 This function is the main entry point of the Proof General
 prooftree support. It examines the delayed output in order to
 take appropriate actions and maintains the internal state.
 
-All arguments are (former) fields of the `proof-action-list'
+The delayed output to handle is in the region
+\[proof-shell-delayed-output-start, proof-shell-delayed-output-end].
+Urgent messages might be before that, following OLD-PROOF-MARKER,
+which contains the position of `proof-marker', before the next
+command was sent to the proof assistant.
+
+All other arguments are (former) fields of the `proof-action-list'
 entry that is now finally retired. CMD is the command, FLAGS are
 the flags and SPAN is the span."
   ;; (message "PTHDO cmd %s flags %s span %s-%s" cmd flags
@@ -1035,7 +1051,8 @@ the flags and SPAN is the span."
 	  (when current-proof-name
 	    ;; we are inside a proof: display something
 	    (proof-tree-ensure-running)
-	    (proof-tree-handle-proof-command cmd proof-info)))))))
+	    (proof-tree-handle-proof-command old-proof-marker
+					     cmd proof-info)))))))
 
 
 ;;
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index f3c983b0..3201e2ff 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -400,7 +400,7 @@ the currently open proof.")
  proof-tree-find-begin-of-unfinished-proof 
            'hol-light-find-begin-of-unfinished-proof
  ;; These ones belong in shell mode
- proof-tree-proof-finished-regexp "No subgoals"	  
+ proof-tree-branch-finished-regexp "No subgoals"	  
  proof-tree-show-sequent-command 
  (lambda (id) (format "print_xgoal_of_id \"%s\";;" id))