- implement retract from prooftree

4 files changed, 46 insertions, 5 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 0bf24650..d89018ea 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1115,7 +1115,7 @@ flag Printing All set."
    proof-tree-configured t
    proof-tree-get-proof-info 'coq-proof-tree-get-proof-info
    proof-tree-find-begin-of-unfinished-proof
-     'coq-find-begin-of-unfinished-proof)   
+     'coq-find-begin-of-unfinished-proof)
 
   (proof-config-done)
 
@@ -1211,6 +1211,7 @@ flag Printing All set."
    proof-tree-extract-instantiated-existentials
      'coq-extract-instantiated-existentials
    proof-tree-show-sequent-command 'coq-show-sequent-command
+   proof-tree-find-undo-position 'coq-proof-tree-find-undo-position
    )
         
   (proof-shell-config-done))
@@ -1386,6 +1387,19 @@ The not yet delayed output is in the region
         (span-start span)
       nil)))
     
+(defun coq-proof-tree-find-undo-position (state)
+  "Return the position for undo state STATE.
+This is the Coq incarnation of `proof-tree-find-undo-position'."
+  (let ((span-res nil)
+        (span-cur (span-at (1- (proof-unprocessed-begin)) 'type))
+        (state (1- state)))
+    ;; go backward as long as the statenum property in the span is greater or
+    ;; equal than state
+    (while (<= state (span-property span-cur 'statenum))
+      (setq span-res span-cur)
+      (setq span-cur (span-at (1- (span-start span-cur)) 'type)))
+    (span-start span-res)))
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index a23a91e7..67248cb4 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -2740,10 +2740,12 @@ communication between Proof General and Prooftree is almost one
 way only. Proof General sends proof status messages to Prooftree,
 from which Prooftree reconstructs the current proof status and
 the complete proof tree. Prooftree never requests additional
-information from Proof General. The only message that is sent
-from Prooftree to Proof General is a @code{stop-displaying}
-command, when the user closes the proof-tree display of the
-current proof.
+information from Proof General. 
+
+There are only a few messages that Prooftree sends to Proof
+General. These messages communicate user requests to Proof
+General, for instance, when the user selects the undo menu item,
+or when he closes the Prooftree window.
 
 The communication protocol is completely described in the
 @code{ocamldoc} documentation of @code{input.ml} in the Prooftree
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 628fae0f..30e19cfc 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3158,6 +3158,8 @@ dependencies.
 given existential variable.
 @item Snapshots of proof trees for reference when you retract
 your proof to try a different approach.
+@item Trigger a retract (undo) operation with a selected sequent
+as target.
 @end itemize
 
 For a more elaborated description please consult the help dialog
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index bca6baf8..c15356f8 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -305,6 +305,16 @@ proof. If there is no such proof, this function must return nil."
   :type 'function
   :group 'proof-tree-internals)
 
+(defcustom proof-tree-find-undo-position nil
+  "Proof assistant specific function for finding the point to undo to.
+This function is used to convert the state number, which comes
+with an undo command from Prooftree, into a point position for
+`proof-retract-until-point'. This function is called in the
+current scripting buffer with the state number as argument. It
+must return a buffer position."
+  :type 'function
+  :group 'proof-tree-internals)
+
 (defcustom proof-tree-urgent-action-hook ()
   "Normal hook for prooftree actions that cannot be delayed.
 This hook is called (indirectly) from inside
@@ -405,6 +415,17 @@ Needed for undo.")
   (proof-tree-quit-proof)
   (setq proof-tree-external-display nil))
 
+(defun proof-tree-handle-proof-tree-undo (data)
+  "Handle an undo command that arrives from prooftree."
+  (let ((undo-state (string-to-number data)))
+    (if (and (integerp undo-state) (> undo-state 0))
+	(with-current-buffer proof-script-buffer
+	  (goto-char (funcall proof-tree-find-undo-position undo-state))
+	  (proof-retract-until-point))
+      (display-warning
+       '(proof-general proof-tree)
+       "Prooftree sent an invalid state for undo"
+       :warning))))			  
 
 (defun proof-tree-insert-output (string)
   "Insert output or a message into the prooftree process buffer."
@@ -431,6 +452,8 @@ callback function requests."
 	  (cond
 	   ((equal cmd "stop-displaying")
 	    (proof-tree-stop-external-display))
+	   ((equal cmd "undo")
+	    (proof-tree-handle-proof-tree-undo data))
 	   (t
 	    (display-warning
 	     '(proof-general proof-tree)