support for nested goals is now restricted to Coq

4 files changed, 85 insertions, 89 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 6587a9da..c4390a9a 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -186,6 +186,28 @@
     (cons 'hyp (match-string 1)))
    (t nil)))
 
+(defun coq-lift-global (glob-span)
+  "This function lifts local lemmas from inside goals out to top level."
+  (let (start (next (span-at 1 'type)) str (goal-p nil))
+    (while (and next (and (not (eq next glob-span)) (not goal-p)))
+      (if (and (eq (span-property next 'type) 'vanilla)
+	       (funcall proof-goal-command-p (span-property next 'cmd)))
+	  (setq goal-p t)
+	(setq next (next-span next 'type))))
+
+    (if (and next (not (eq next glob-span)))
+	(progn
+	  (proof-unlock-locked)
+	  (setq str (buffer-substring (span-start glob-span)
+				      (span-end glob-span)))
+	  (delete-region (span-start glob-span) (span-end glob-span))
+	  (goto-char (span-start next))
+	  (setq start (point))
+	  (insert str "\n")
+	  (set-span-endpoints glob-span start (point))
+	  (set-span-start next (point))
+	  (proof-lock-unlocked)))))
+
 (defun coq-state-preserving-p (cmd)
   (not (string-match coq-undoable-commands-regexp cmd)))
 
@@ -386,7 +408,8 @@
         proof-shell-start-goals-regexp "[0-9]+ subgoals?"
         proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp
         proof-shell-init-cmd nil
-	proof-analyse-using-stack t)
+	proof-analyse-using-stack t
+	proof-lift-global coq-lift-global)
 
   ;; The following hook is removed once it's called.
   (add-hook 'proof-shell-insert-hook 'coq-shell-init-hook nil t)
diff --git a/etc/lego/GoalGoal.l b/etc/lego/GoalGoal.l
new file mode 100644
index 00000000..c4826e0d
--- /dev/null
+++ b/etc/lego/GoalGoal.l
@@ -0,0 +1,13 @@
+Module GoalGoal;
+
+Goal first : {A:Prop}A->A;
+intros; Immed;
+(* no Save *)
+
+Goal second : {A:Prop}A->A;
+intros; Immed;
+Save second;
+(* asserting until here caused Proof General to swap first and second.
+This is a bug for LEGO. Thanks to Martin Hofmann for pointing this
+out. An obvious bug fix would be to make the function
+proof-lift-global Coq specific. *)
\ No newline at end of file
diff --git a/generic/proof.el b/generic/proof.el
index 1c5ba100..ba556b4e 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -340,6 +340,13 @@ The script buffer's comment-end is set to this string plus a space."
   :type 'function
   :group 'proof-script)
 
+(defcustom proof-lift-global nil
+  "This function lifts local lemmas from inside goals out to top level.
+This function takes the local goalsave span as an argument. Set this
+to `nil' of the proof assistant does not support nested goals."
+  :type '(choice nil function)
+  :group 'proof-script)
+
 (defcustom proof-count-undos-fn nil 
   "Compute number of undos in a target segment"
   :type 'function
@@ -726,14 +733,6 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
   (set-span-property proof-queue-span 'end-open t)
   (span-read-only proof-queue-span)
 
-;; old code, pending test of defface above:
-;; (make-face 'proof-queue-face)
-;;  (cond ((proof-have-color)
-;;	 (set-face-background 'proof-queue-face "mistyrose"))
-;;	(t (progn
-;;	     (set-face-background 'proof-queue-face "Black")
-;;	     (set-face-foreground 'proof-queue-face "White"))))
-  
   (set-span-property proof-queue-span 'face 'proof-queue-face)
 
   (detach-span proof-queue-span)
@@ -745,11 +744,6 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
   (set-span-property proof-locked-span 'end-open t)
   (span-read-only proof-locked-span)
 
-;; old code, pending test of defface above:
-;;  (make-face 'proof-locked-face)
-;;  (cond ((proof-have-color)
-;;	 (set-face-background 'proof-locked-face "lavender"))
-;;	(t (set-face-property 'proof-locked-face 'underline t)))
   (set-span-property proof-locked-span 'face 'proof-locked-face)
 
   (detach-span proof-locked-span))
@@ -835,7 +829,10 @@ Only call this from a scripting buffer."
 	       (setq buffer-display-table disp)))))
 
 (defun proof-mark-buffer-atomic (buffer)
-  "Mark BUFFER as having processed in a single step."
+  "Mark BUFFER as having processed in a single step.
+
+If buffer already contains a locked region, only the remainder of the
+buffer is closed off atomically." 
   (save-excursion
     (set-buffer buffer)
     (let ((span (make-span (proof-unprocessed-begin) (point-max)))
@@ -853,16 +850,9 @@ Only call this from a scripting buffer."
       (set-span-property span 'type 'vanilla)
       (set-span-property span 'cmd cmd)
       (proof-set-locked-end (point-max))
-      (setq proof-script-buffer-list
-	    (append proof-script-buffer-list (list buffer))))))
-
-(defun proof-filter-list (p list)
-  "Returns all elements in LIST for which P holds."
-  (let (head tail)
-    (if (null list) list
-      (setq head (car list)
-	    tail (proof-filter-list p (cdr list)))
-      (if (funcall p head) (cons head tail) tail))))
+      (or (member buffer proof-script-buffer-list)
+	  (setq proof-script-buffer-list
+		(append proof-script-buffer-list (list buffer)))))))
 
 (defun proof-file-truename (filename)
   "Returns the true name of the file FILENAME or nil."
@@ -872,13 +862,10 @@ Only call this from a scripting buffer."
   "Register a new FILE as having been processed by the prover."
   (let* ((cfile (file-truename file))
 	 (buffer (proof-file-to-buffer cfile)))
+    (assert (not (member cfile proof-included-files-list))
+	    'showargs "proof-register-new-processed-file")
     (setq proof-included-files-list
-	  (cons cfile
-		;; remove is for redundency. The following assertion
-		;; ought to be true:
-		;; { (equal proof-included-files-list
-		;;   (remove cfile proof-included-files-list) }
-		(remove cfile proof-included-files-list)))
+	  (cons cfile proof-included-files-list))
     (or (equal cfile
 	       (file-truename (buffer-file-name
 			       (car proof-script-buffer-list))))
@@ -986,7 +973,11 @@ Only call this from a scripting buffer."
        proof-shell-buffer))
 
 (defun proof-start-shell ()
-  "Initialise a shell-like buffer for a proof assistant."
+  "Initialise a shell-like buffer for a proof assistant.
+
+Also generates goal and response buffers.
+Initialises current buffer for scripting.
+Does nothing if proof assistant is already running."
   (if (proof-shell-live-buffer)
       ()
     (run-hooks 'proof-pre-shell-start-hook)
@@ -1498,31 +1489,35 @@ assistant."
   (save-excursion (proof-shell-insert string)))
 
 (defun proof-check-process-available (&optional relaxed)
-  "Checks whether the proof process is available.
-Specifically:
-     (1) Is the current buffer a proof script?
-     (2) Is the proof process idle?
-     (3) Is a proof process running?
-It signals an error if at least one of the conditions is not
-fulfilled. If optional arg RELAXED is set, only (2) and (3) are 
-tested.
-
-The current buffer will become the current scripting buffer provided
-the current scripting buffer has either no locked region or everything 
-in it has been processed."
+  "Adjust internal variables for scripting of current buffer.
+
+Signals an error if current buffer is not a proof script or if the
+proof process is not idle. If RELAXED is set, nothing more is done. No
+changes are necessary if the current buffer is already in Scripting
+minor mode. Otherwise, the current buffer will become the current
+scripting buffer provided the current scripting buffer has either no
+locked region or everything in it has been processed."
   (proof-start-shell)
   (cond
    ((not (or relaxed (eq proof-buffer-type 'script)))
     (error "Must be running in a script buffer"))
    (proof-shell-busy (error "Proof Process Busy!"))
    (relaxed ())			;exit cond
+
+   ;; No buffer is in Scripting minor mode.
+   ;; We assume the setup is done somewhere else
    ((null proof-script-buffer-list) ())
+
+   ;; The current buffer is in Scripting minor mode
    ((equal (current-buffer) (car proof-script-buffer-list)) ())
    (t
     (let ((script-buffer (car proof-script-buffer-list))
 	  (current-buffer (current-buffer)))
       (save-excursion
 	(set-buffer script-buffer)
+
+	;; We only allow switching of the Scripting buffer if the
+	;; locked region is either empty of full for all buffers.
 	(if (member (proof-unprocessed-begin) (list (point-min)
 						     (point-max)))
 
@@ -1530,6 +1525,8 @@ in it has been processed."
 	   (progn
 	     (setq proof-active-buffer-fake-minor-mode nil)
 	     (set-buffer current-buffer)
+
+	     ;; does the current buffer contain locked regions already?
 	     (if (member current-buffer proof-script-buffer-list)
 		 (setq proof-script-buffer-list
 		       (remove current-buffer proof-script-buffer-list))
@@ -1694,7 +1691,7 @@ arrive."
 	  
 		  
 (defun proof-shell-process-urgent-message (message)
-  "Display and analyse urgent MESSAGE."
+  "Display and analyse urgent MESSAGE for asserting or retracting files."
   (proof-message message)
   (proof-response-buffer-display message 'font-lock-eager-annotation-face)
 
@@ -1840,31 +1837,6 @@ how far we've got."
 ;;         setup and callback                                       ;;
 
 
-;; This code is for nested goals in Coq, and shouldn't affect things
-;; in LEGO.
-;; FIXME da: perhaps this belongs in coq.el?
-(defun proof-lift-global (glob-span)
-  "This function lifts local lemmas from inside goals out to top level."
-  (let (start (next (span-at 1 'type)) str (goal-p nil))
-    (while (and next (and (not (eq next glob-span)) (not goal-p)))
-      (if (and (eq (span-property next 'type) 'vanilla)
-	       (funcall proof-goal-command-p (span-property next 'cmd)))
-	  (setq goal-p t)
-	(setq next (next-span next 'type))))
-
-    (if (and next (not (eq next glob-span)))
-	(progn
-	  (proof-unlock-locked)
-	  (setq str (buffer-substring (span-start glob-span)
-				      (span-end glob-span)))
-	  (delete-region (span-start glob-span) (span-end glob-span))
-	  (goto-char (span-start next))
-	  (setq start (point))
-	  (insert str "\n")
-	  (set-span-endpoints glob-span start (point))
-	  (set-span-start next (point))
-	  (proof-lock-unlocked)))))
-
 (defun proof-done-advancing (span)
   "The callback function for assert-until-point."
   (let ((end (span-end span)) nam gspan next cmd)
@@ -1903,12 +1875,14 @@ how far we've got."
       (set-span-property gspan 'type 'goalsave)
       (set-span-property gspan 'name nam)
 
-      (proof-lift-global gspan))
+      (and proof-lift-global
+	   (funcall proof-lift-global gspan)))
      (t
       (set-span-property span 'mouse-face 'highlight)
-      (and proof-global-p
+      (and proof-global-p 
 	   (funcall proof-global-p cmd)
-	   (proof-lift-global span))))))
+	   proof-lift-global
+	   (funcall proof-lift-global span))))))
 
 
 
diff --git a/todo b/todo
index 18b494c1..1882bba6 100644
--- a/todo
+++ b/todo
@@ -60,12 +60,9 @@ D Add proof-quit-command: some provers may like a quit command to be
   Also reconcile proof-restart-script and proof-stop-shell, see
   comments in code.
 
-D Multiple files (after basic feature added): handle failures in
+D Multiple files: handle failures in
   reading ancestors.
 
-A Add support for putting a locked region in processed files.
-  (tms 4h)
-
 B Clean up proof-assert-until-point behaviour.  Discussion results:
     1.  At the moment we get an odd error if it is run in
     the locked region.    This is a bug.  Should behave same
@@ -88,10 +85,6 @@ B Clean up proof-assert-until-point behaviour.  Discussion results:
     when new commands are added to the buffer needs careful
     thought!
 
-A Write function proof-retract-file. (30min tms)
-  Currently, the command ForgetMark (for LEGO) is hardwired in
-  proof-steal-process.
-
 A Implement more generic mechanism for large undos (2h tms)
 
     COQ: C-c u inside a Section should reset the whole section, then
@@ -100,13 +93,6 @@ A Implement more generic mechanism for large undos (2h tms)
     LEGO: consider Discharge; perhaps unrol to the beginning of the
           module?
 
-A Multiple files are sometimes handled incorrectly, because the
-  function `proof-steal-process' cannot figure out that some files have
-  already been processed. This is most likely caused by the ad-hoc
-  equality test on file names. Instead, one could employ
-  the built-in `file-truename' to trigger *canonical* file names.
-  (1h tms)
-
 A replace (current-buffer) by proof-shell-buffer/proof-script-buffer
   where ever possible (30 min tms)
 
@@ -347,7 +333,7 @@ B `lego-get-path' assumes that LEGOPATH has been set in the
 
 B release new version of the LEGO proof engine (4h tms)
 
-C Equiv, Next,... aren't handled properly, because LEGO does not
+B Equiv, Next,... aren't handled properly, because LEGO does not
   refresh the proof state. Perhaps it would be easiest to get LEGO to
   output more information in proof script mode (2h)