Added some magic commands: proof-frob-locked-end, proof-try-command,

proof-interrupt-process. Added moving nested lemmas above goal for coq.
Changed the key mapping for assert-until-point to C-c RET.

6 files changed, 443 insertions, 270 deletions

diff --git a/coq.el b/coq.el
index 202dfdff..a51cd4a1 100644
--- a/coq.el
+++ b/coq.el
@@ -3,6 +3,11 @@
 ;; Author: Healfdene Goguen and Thomas Kleymann
 
 ;; $Log$
+;; Revision 1.10  1997/11/17 17:11:15  djs
+;; Added some magic commands: proof-frob-locked-end, proof-try-command,
+;; proof-interrupt-process. Added moving nested lemmas above goal for coq.
+;; Changed the key mapping for assert-until-point to C-c RET.
+;;
 ;; Revision 1.9  1997/11/12 15:56:15  hhg
 ;; Changed pbp-change-goal so that it only "Show"s the goal pointed at.
 ;;
@@ -310,7 +315,7 @@
    (t nil)))
 
 (defun coq-retract-target (target delete-region)
-  (let ((end (proof-end-of-locked))
+  (let ((end (proof-locked-end))
 	(start (span-start target))
 	(ext (proof-last-goal-or-goalsave))
 	actions)
@@ -339,7 +344,7 @@
 			      (coq-find-and-forget target)
 			      delete-region))))
       
-    (proof-start-queue (min start end) (proof-end-of-locked) actions)))
+    (proof-start-queue (min start end) (proof-locked-end) actions)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Commands specific to coq                                      ;;
diff --git a/lego.el b/lego.el
index 9a47d58a..cdcb198b 100644
--- a/lego.el
+++ b/lego.el
@@ -5,6 +5,11 @@
 
 
 ;; $Log$
+;; Revision 1.28  1997/11/17 17:11:17  djs
+;; Added some magic commands: proof-frob-locked-end, proof-try-command,
+;; proof-interrupt-process. Added moving nested lemmas above goal for coq.
+;; Changed the key mapping for assert-until-point to C-c RET.
+;;
 ;; Revision 1.27  1997/11/06 16:56:26  hhg
 ;; Assign new variable proof-goal-hyp-fn to lego-goal-hyp, which is
 ;; simply old code for picking up goal or hypothesis for pbp
@@ -57,6 +62,9 @@
   "Command to adjust the linewidth for pretty printing of the LEGO
   process.") 
 
+(defconst lego-interrupt-regexp "Interrupt.."
+  "Regexp corresponding to an interrupt")
+
 (defvar lego-test-all-name "test_all"
   "The name of the LEGO module which inherits all other modules of the
   library.")
@@ -311,16 +319,8 @@
       "COMMENT")))
   
 
-(defun lego-goal-hyp ()
-  (cond 
-   ((looking-at proof-shell-goal-regexp)
-    (cons 'goal (match-string 1)))
-   ((looking-at proof-shell-assumption-regexp)
-    (cons 'hyp (match-string 1)))
-   (t nil)))
-
 (defun lego-retract-target (target delete-region)
-  (let ((end (proof-end-of-locked))
+  (let ((end (proof-locked-end))
 	(start (span-start target))
 	(ext (proof-last-goal-or-goalsave))
 	actions)
@@ -349,7 +349,19 @@
 			      (lego-find-and-forget target)
 			      delete-region))))
       
-    (proof-start-queue (min start end) (proof-end-of-locked) actions)))
+    (proof-start-queue (min start end) (proof-locked-end) actions)))
+
+(defun lego-goal-hyp ()
+  (cond 
+   ((looking-at proof-shell-goal-regexp)
+    (cons 'goal (match-string 1)))
+   ((looking-at proof-shell-assumption-regexp)
+    (cons 'hyp (match-string 1)))
+   (t nil)))
+
+
+(defun lego-state-preserving-p (cmd)
+  (not (string-match lego-undoable-commands-regexp cmd)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Commands specific to lego                                      ;;
@@ -427,8 +439,9 @@
   (setq proof-comment-start "(*")
   (setq proof-comment-end "*)")
 
-  (setq proof-retract-target-fn 'lego-retract-target)
-  (setq proof-goal-hyp-fn 'lego-goal-hyp)
+  (setq proof-retract-target-fn 'lego-retract-target
+        proof-goal-hyp-fn 'lego-goal-hyp
+	proof-state-preserving-p 'lego-state-preserving-p)
 
   (setq	proof-save-command-regexp lego-save-command-regexp
 	proof-save-with-hole-regexp lego-save-with-hole-regexp
@@ -504,6 +517,7 @@
         proof-shell-abort-goal-regexp lego-shell-abort-goal-regexp
         proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp
         proof-shell-error-regexp lego-error-regexp
+	proof-shell-interrupt-regexp lego-interrupt-regexp
         proof-shell-noise-regexp "Discharge\\.\\. "
         proof-shell-assumption-regexp lego-id
         proof-shell-goal-regexp lego-goal-regexp
diff --git a/proof-dependencies.el b/proof-dependencies.el
new file mode 100644
index 00000000..d3dcddb3
--- /dev/null
+++ b/proof-dependencies.el
@@ -0,0 +1,157 @@
+; This file is an attempt to abstract away from the differences between
+; XEmacs and FSF Emacs. Everything that is done differently between one
+; or other version should be appropriately wrapped in here.
+
+
+(defvar proof-locked-hwm nil
+  "Upper limit of the locked region")
+
+(defvar proof-queue-loose-end nil
+  "Limit of the queue region that is not equal to proof-locked-hwm.")
+
+
+(defsubst make-span (start end)
+  (make-extent start end))
+
+(defsubst set-span-endpoints (span start end)
+  (set-extent-endpoints span start end))
+
+(defsubst set-span-start (span value)
+  (set-extent-endpoints span value (extent-end-position span)))
+
+(defsubst set-span-end (span value)
+  (set-extent-endpoints span (extent-start-position span) value))
+
+(defsubst span-property (span name)
+  (extent-property span name))
+
+(defsubst set-span-property (span name value)
+  (set-extent-property span name value))
+
+(defsubst delete-span (span)
+  (delete-extent span))
+
+(defsubst delete-spans (start end prop)
+  (mapcar-extents 'delete-extent nil (current-buffer) start end  nil prop))
+
+(defsubst span-at (pt prop)
+  (extent-at pt nil prop))
+
+(defsubst span-at-before (pt prop)
+  (extent-at pt nil prop nil 'before))
+  
+(defsubst span-start (span)
+  (extent-start-position span))
+
+(defsubst span-end (span)
+  (extent-end-position span))
+
+(defsubst prev-span (span prop)
+  (extent-at (extent-start-position span) nil prop nil 'before))
+
+(defsubst next-span (span prop)
+  (extent-at (extent-end-position span) nil prop nil 'after))
+
+(defvar proof-locked-ext nil
+  "Upper limit of the locked region")
+
+(defvar proof-queue-ext nil
+  "Upper limit of the locked region")
+
+(defun proof-init-segmentation ()
+  (setq proof-queue-loose-end nil)
+  (setq proof-queue-ext (make-extent nil nil (current-buffer)))
+  (set-extent-property proof-queue-ext 'start-closed t)
+  (set-extent-property proof-queue-ext 'end-open t)
+  (set-extent-property proof-queue-ext 'read-only t)
+  (make-face 'proof-queue-face)
+  (if (eq (device-class (frame-device)) 'color)
+	     (set-face-background 'proof-queue-face "mistyrose")
+    (set-face-background 'proof-queue-face "Black")
+    (set-face-foreground 'proof-queue-face "White"))
+  (set-extent-property proof-queue-ext 'face 'proof-queue-face)
+  
+  (setq proof-locked-hwm nil)
+  (setq proof-locked-ext (make-extent nil nil (current-buffer)))
+  (set-extent-property proof-locked-ext 'start-closed t)
+  (set-extent-property proof-locked-ext 'end-open t)
+  (set-extent-property proof-locked-ext 'read-only t)
+  (if (eq (device-class (frame-device)) 'color)
+      (progn (make-face 'proof-locked-face)
+	     (set-face-background 'proof-locked-face "lavender")
+	     (set-extent-property proof-locked-ext 'face 'proof-locked-face))
+    (set-extent-property proof-locked-ext 'face 'underline)))
+
+(defsubst proof-lock-unlocked ()
+  (set-extent-property proof-locked-ext 'read-only t))
+
+(defsubst proof-unlock-locked ()
+  (set-extent-property proof-locked-ext 'read-only nil))
+
+(defsubst proof-detach-queue ()
+  (detach-extent proof-queue-ext))
+
+(defsubst proof-set-queue-endpoints (start end)
+  (set-extent-endpoints proof-queue-ext start end))
+
+(defsubst proof-set-queue-start (start)
+  (set-extent-endpoints proof-queue-ext start 
+			(extent-end-position proof-queue-ext)))
+
+(defsubst proof-set-queue-end (end)
+  (set-extent-endpoints proof-queue-ext (extent-start-position proof-queue-ext)
+			end)) 
+
+(defsubst proof-detach-segments ()
+  (detach-extent proof-queue-ext)
+  (detach-extent proof-locked-ext))
+
+(defsubst proof-set-locked-end (end)
+  (set-extent-endpoints proof-locked-ext (point-min) end))
+
+(defsubst proof-locked-end ()
+  (or (and proof-locked-ext (extent-end-position proof-locked-ext))
+      (point-min)))
+
+(defsubst proof-end-of-queue ()
+  (extent-end-position proof-queue-ext))
+
+;(defsubst proof-have-color ()
+;  (eq (device-class) 'color))
+
+(defun proof-dont-show-annotations ()
+  (let ((disp (make-display-table))
+	(i 128))
+	(while (< i 256)
+	  (aset disp i "")
+	  (incf i))
+	(add-spec-to-specifier current-display-table disp (current-buffer))))
+
+;; in case Emacs is not aware of read-shell-command-map
+(defvar read-shell-command-map
+  (let ((map (make-sparse-keymap)))
+    (if (not (fboundp 'set-keymap-parents))
+        (setq map (append minibuffer-local-map map))
+      (set-keymap-parents map minibuffer-local-map)
+      (set-keymap-name map 'read-shell-command-map))
+    (define-key map "\t" 'comint-dynamic-complete)
+    (define-key map "\M-\t" 'comint-dynamic-complete)
+    (define-key map "\M-?" 'comint-dynamic-list-completions)
+    map)
+  "Minibuffer keymap used by shell-command and related commands.")
+v
+
+;; in case Emacs is not aware of the function read-shell-command
+(or (fboundp 'read-shell-command)
+    ;; from minibuf.el distributed with XEmacs 19.11
+    (defun read-shell-command (prompt &optional initial-input history)
+      "Just like read-string, but uses read-shell-command-map:
+\\{read-shell-command-map}"
+      (let ((minibuffer-completion-table nil))
+        (read-from-minibuffer prompt initial-input read-shell-command-map
+                              nil (or history
+                              'shell-command-history)))))
+
+
+
+(provide 'proof-dependencies)
diff --git a/proof-fontlock.el b/proof-fontlock.el
index ff2c4630..11920a32 100644
--- a/proof-fontlock.el
+++ b/proof-fontlock.el
@@ -4,6 +4,11 @@
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 
 ;; $Log$
+;; Revision 1.3  1997/11/17 17:11:19  djs
+;; Added some magic commands: proof-frob-locked-end, proof-try-command,
+;; proof-interrupt-process. Added moving nested lemmas above goal for coq.
+;; Changed the key mapping for assert-until-point to C-c RET.
+;;
 ;; Revision 1.2  1997/10/13 17:13:50  tms
 ;; *** empty log message ***
 ;;
@@ -35,25 +40,27 @@
 ;; font lock faces: declarations, errors, tacticals                 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+(defun proof-have-color ()
+ ())
+
 (defvar font-lock-declaration-name-face 
 (progn 
-  (cond ((eq (device-class) 'color)
-	 ;notice that device-class does not exist in Emacs 19.30
+  (cond 
+   ((proof-have-color)
+    (copy-face 'bold 'font-lock-declaration-name-face)
 
-	 (copy-face 'bold 'font-lock-declaration-name-face)
+    ;; Emacs 19.28 compiles this down to
+    ;; internal-set-face-1. This is not compatible with XEmacs
+    (set-face-foreground
+     'font-lock-declaration-name-face "chocolate"))
+    (t (copy-face 'bold-italic 'font-lock-declaration-name-face)))))
 
-	 ;; Emacs 19.28 compiles this down to
-	 ;; internal-set-face-1. This is not compatible with XEmacs
-	   (set-face-foreground
-	    'font-lock-declaration-name-face "chocolate"))
-	(t (copy-face 'bold-italic 'font-lock-declaration-name-face)))
 ;;  (if running-emacs19
 ;;      (setq font-lock-declaration-name-face
-;;	    (face-name 'font-lock-declaration-name-face)))
-  ))
+;;	    (face-name 'font-lock-declaration-name-face))
 
 (defvar font-lock-tacticals-name-face
-(if (eq (device-class) 'color)
+(if (proof-have-color)
     (let ((face (make-face 'font-lock-tacticals-name-face)))
       (dont-compile
 	(set-face-foreground face
@@ -62,7 +69,7 @@
   (copy-face 'bold 'font-lock-tacticals-name-face)))
 
 (defvar font-lock-error-face
-(if (eq (device-class) 'color)
+(if (proof-have-color)
     (let ((face (make-face 'font-lock-error-face)))
       (dont-compile
 	(set-face-foreground face
diff --git a/proof.el b/proof.el
index b9e70740..d4952721 100644
--- a/proof.el
+++ b/proof.el
@@ -8,17 +8,12 @@
 
 
 
-;; TO DO:
-
-;; o Need to think about fixing up errors caused by pbp-generated commands
-
-;; o undo support needs to consider Discharge; perhaps unrol to the
-;;   beginning of the module? 
-
-;; o pbp code is horribly inefficient and doesn't accord with the tech
-;;   report
-
 ;; $Log$
+;; Revision 1.25  1997/11/17 17:11:21  djs
+;; Added some magic commands: proof-frob-locked-end, proof-try-command,
+;; proof-interrupt-process. Added moving nested lemmas above goal for coq.
+;; Changed the key mapping for assert-until-point to C-c RET.
+;;
 ;; Revision 1.24  1997/11/13 10:23:49  hhg
 ;; Includes commented code for Coq version of extent protocol
 ;;
@@ -27,7 +22,8 @@
 ;;
 ;; Revision 1.22  1997/11/10 15:51:09  djs
 ;; Put in a workaround for a strange bug in comint which was finding a bunch
-;; of ^G's from comint-get-old-input for some inexplicable reason.
+;; of ^G's from comint-get-old-input for some inexplicable reason. THIS IS
+;; STILL BROKEN AND A BUG REPORT HAS BEEN SUBMITTED TO XEMACS.ORG
 ;;
 ;; Revision 1.21  1997/11/06 16:56:59  hhg
 ;; Parameterize by proof-goal-hyp-fn in pbp-make-top-span, to handle
@@ -110,6 +106,7 @@
 (require 'compile)
 (require 'comint)
 (require 'etags)
+(require 'proof-dependencies)
 (require 'proof-fontlock)
 
 (autoload 'w3-fetch "w3" nil t)
@@ -152,6 +149,9 @@
 (defvar proof-goal-hyp-fn nil "Is point at goal or hypothesis")
 (defvar proof-kill-goal-command nil "How to kill a goal.")
 
+(defvar proof-state-preserving-p nil
+  "whether a command preserves the proof state")
+
 (defvar pbp-change-goal nil
   "*Command to change to the goal %s")
 
@@ -190,6 +190,10 @@
   "A regular expression indicating that the PROOF process has
   identified an error.") 
 
+(defvar proof-shell-interrupt-regexp nil
+  "A regular expression indicating that the PROOF process has
+  responded to an interrupt.") 
+
 (defvar proof-shell-proof-completed-regexp nil
   "*Regular expression indicating that the proof has been completed.")
 
@@ -224,12 +228,6 @@
 (defvar proof-re-term-or-comment nil 
   "You are not authorised for this information.")
 
-(defvar proof-locked-hwm nil
-  "Upper limit of the locked region")
-
-(defvar proof-queue-loose-end nil
-  "Limit of the queue region that is not equal to proof-locked-hwm.")
-
 (defvar proof-marker nil 
   "You are not authorised for this information.")
 
@@ -253,6 +251,7 @@
 (defvar proof-included-files-list nil 
   "Files currently included in proof process")
 
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;               Bridging the emacs19/xemacs gulf                   ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -271,131 +270,6 @@
       (and (= emacs-major-version major) (>= emacs-minor-version minor)))
 )
 
-(defvar extended-shell-command-on-region
-  (emacs-version-at-least 19 29)
-  "Does `shell-command-on-region' optionally offer to output in an other buffer?")
-
-;; in case Emacs is not aware of read-shell-command-map
-(defvar read-shell-command-map
-  (let ((map (make-sparse-keymap)))
-    (if (not (fboundp 'set-keymap-parents))
-        (setq map (append minibuffer-local-map map))
-      (set-keymap-parents map minibuffer-local-map)
-      (set-keymap-name map 'read-shell-command-map))
-    (define-key map "\t" 'comint-dynamic-complete)
-    (define-key map "\M-\t" 'comint-dynamic-complete)
-    (define-key map "\M-?" 'comint-dynamic-list-completions)
-    map)
-  "Minibuffer keymap used by shell-command and related commands.")
-
-
-;; in case Emacs is not aware of the function read-shell-command
-(or (fboundp 'read-shell-command)
-    ;; from minibuf.el distributed with XEmacs 19.11
-    (defun read-shell-command (prompt &optional initial-input history)
-      "Just like read-string, but uses read-shell-command-map:
-\\{read-shell-command-map}"
-      (let ((minibuffer-completion-table nil))
-        (read-from-minibuffer prompt initial-input read-shell-command-map
-                              nil (or history
-                              'shell-command-history)))))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  Spans and segments                                              ;;
-;;  Because one day we might wish to port to emacs19                ;;
-;;  Note that we need to go back to using marks too                 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defsubst make-span (start end)
-  (make-extent start end))
-
-(defsubst set-span-endpoints (span start end)
-  (set-extent-endpoints span start end))
-
-(defsubst set-span-start (span value)
-  (set-extent-endpoints span value (extent-end-position span)))
-
-(defsubst set-span-end (span value)
-  (set-extent-endpoints span (extent-start-position span) value))
-
-(defsubst span-property (span name)
-  (extent-property span name))
-
-(defsubst set-span-property (span name value)
-  (set-extent-property span name value))
-
-(defsubst delete-span (span)
-  (delete-extent span))
-
-(defsubst delete-spans (start end prop)
-  (mapcar-extents 'delete-extent nil (current-buffer) start end  nil prop))
-
-(defsubst span-at (pt prop)
-  (extent-at pt nil prop))
-
-(defsubst span-at-before (pt prop)
-  (extent-at pt nil prop nil 'before))
-  
-(defsubst span-start (span)
-  (extent-start-position span))
-
-(defsubst span-end (span)
-  (extent-end-position span))
-
-(defsubst prev-span (span prop)
-  (extent-at (extent-start-position span) nil prop nil 'before))
-
-(defsubst next-span (span prop)
-  (extent-at (extent-end-position span) nil prop nil 'after))
-
-(defvar proof-locked-ext nil
-  "Upper limit of the locked region")
-
-(defvar proof-queue-ext nil
-  "Upper limit of the locked region")
-
-(defun proof-init-segmentation ()
-  (setq proof-queue-loose-end nil)
-  (setq proof-queue-ext (make-extent nil nil (current-buffer)))
-  (set-extent-property proof-queue-ext 'start-closed t)
-  (set-extent-property proof-queue-ext 'end-open t)
-  (set-extent-property proof-queue-ext 'read-only t)
-  (make-face 'proof-queue-face)
-  (if (eq (device-class (frame-device)) 'color)
-	     (set-face-background 'proof-queue-face "mistyrose")
-    (set-face-background 'proof-queue-face "Black")
-    (set-face-foreground 'proof-queue-face "White"))
-  (set-extent-property proof-queue-ext 'face 'proof-queue-face)
-  
-  (setq proof-locked-hwm nil)
-  (setq proof-locked-ext (make-extent nil nil (current-buffer)))
-  (set-extent-property proof-locked-ext 'start-closed t)
-  (set-extent-property proof-locked-ext 'end-open t)
-  (set-extent-property proof-locked-ext 'read-only t)
-  (if (eq (device-class (frame-device)) 'color)
-      (progn (make-face 'proof-locked-face)
-	     (set-face-background 'proof-locked-face "lavender")
-	     (set-extent-property proof-locked-ext 'face 'proof-locked-face))
-    (set-extent-property proof-locked-ext 'face 'underline)))
-
-(defun proof-segment-buffer (eol eoq)
-   (setq proof-locked-hwm eol
-         proof-queue-loose-end eoq)
-   (if (and (null eoq) (null eol))
-       (progn (detach-extent proof-locked-ext)
-	      (detach-extent proof-queue-ext))
-     (if (eq eol (point-min))
-	 (detach-extent proof-locked-ext)
-       (set-extent-endpoints proof-locked-ext (point-min) eol 
-			     (current-buffer)))
-     (if (eq eol eoq)
-	 (progn
-	   (detach-extent proof-queue-ext)
-	   (setq proof-queue-loose-end nil))
-       (set-extent-endpoints proof-queue-ext eol eoq (current-buffer)))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; A couple of small utilities ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -420,15 +294,10 @@
   (concat (substring address 0 (match-end 0))
           (file-name-directory (substring address (match-end 0)))))
 
-(defun proof-end-of-locked ()
-  "Jump to the end of the locked region."
-  (interactive)
-  (or proof-locked-hwm (point-min)))
-
 (defun proof-goto-end-of-locked ()
   "Jump to the end of the locked region."
   (interactive)
-  (goto-char (proof-end-of-locked)))
+  (goto-char (proof-locked-end)))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -470,7 +339,6 @@
 
       (save-excursion
 	(set-buffer proof-shell-buffer)
-	(setq comint-get-old-input (function (lambda () "")))
 	(funcall proof-mode-for-shell)
 	(set-buffer proof-pbp-buffer)
 	(funcall proof-mode-for-pbp))
@@ -495,7 +363,7 @@
 	      (comint-send-eof)
 	      (save-excursion
 		(set-buffer proof-script-buffer)
-		(proof-segment-buffer nil nil))
+		(proof-detach-segments))
 	      (kill-buffer))
 	    (run-hooks 'proof-shell-exit-hook)
 
@@ -627,14 +495,14 @@
 	 ((= c proof-shell-field-char)
 	  (setq ext (make-span (car stack) op))
 	  (set-span-property ext 'mouse-face 'highlight)
-	  (set-span-property ext 'proof (cadr stack))
+	  (set-span-property ext 'proof (car (cdr stack)))
 					; Pop annotation off stack, for Coq
 ;	  (setq ap 0)
-;	  (while (< ap (length (cadr stack)))
-;	    (aset ann ap (aref (cadr stack) ap))
+;	  (while (< ap (length (car (cdr stack))))
+;	    (aset ann ap (aref (car (cdr stack) ap)))
 ;	    (incf ap))
 					; Finish popping annotations
-	  (setq stack (cddr stack)))
+	  (setq stack (cdr (cdr stack))))
 	 (t (incf op)))
 	(incf ip))
       (setq topl (reverse (cons (point-max) topl)))
@@ -665,10 +533,24 @@
     (insert-string string)
     (beep))
   (set-buffer proof-script-buffer)
-  (proof-segment-buffer proof-locked-hwm proof-locked-hwm)
-  (delete-spans (proof-end-of-locked) (point-max) 'type)
+  (proof-detach-queue)
+  (delete-spans (proof-locked-end) (point-max) 'type)
   (proof-release-lock))
 
+(defun proof-shell-handle-interrupt ()
+  (save-excursion 
+    (display-buffer (set-buffer proof-pbp-buffer))
+    (goto-char (point-max))
+    (newline 2)
+    (insert-string 
+     "Interrupt: Script Management may be in an inconsistent state\n")
+    (beep))
+  (set-buffer proof-script-buffer)
+  (if proof-shell-busy
+      (progn (proof-detach-queue)
+	     (delete-spans (proof-locked-end) (point-max) 'type)
+	     (proof-release-lock))))
+
 (defvar proof-shell-delayed-output nil
   "The last interesting output the proof process output, and what to do
    with it.")
@@ -682,6 +564,7 @@
        ((eq ins 'insert)
 	(setq str (proof-shell-strip-annotations str))
 	(set-buffer proof-pbp-buffer)
+	(erase-buffer)
 	(insert str))
        ((eq ins 'analyse)
 	(proof-shell-analyse-structure str))
@@ -696,6 +579,9 @@
     (cons 'error (proof-shell-strip-annotations 
 		  (substring string (match-beginning 0)))))
 
+   ((string-match proof-shell-interrupt-regexp string)
+    'interrupt)
+
    ((string-match proof-shell-abort-goal-regexp string)
     (setq proof-shell-delayed-output (cons 'insert "\n\nAborted"))
     ())
@@ -774,20 +660,20 @@
 ; Pass start and end as nil if the cmd isn't in the buffer.
 
 (defun proof-start-queue (start end alist)
-  (if start 
-      (if (eq (proof-end-of-locked) start) 
-	  (proof-segment-buffer start end)
-	(proof-segment-buffer end start)))
-  (while (and alist (string= (cadar alist) "COMMENT"))
-    (funcall (caddar alist) (caar alist))
+  (if start
+      (proof-set-queue-endpoints start end))
+  (let (item)
+    (while (and alist (string= 
+		       (nth 1 (setq item (car alist))) 
+		       "COMMENT"))
+    (funcall (nth 2 item) (car item))
     (setq alist (cdr alist)))
   (if alist
       (progn
 	(proof-grab-lock) 
-	(erase-buffer proof-pbp-buffer)
 	(setq proof-shell-delayed-output (cons 'insert "Done."))
 	(setq proof-action-list alist)
-	(proof-send (cadar alist)))))
+	(proof-send (nth 1 item))))))
 
 ; returns t if it's run out of input
 
@@ -795,18 +681,21 @@
   (save-excursion
     (set-buffer proof-script-buffer)
     (if (null proof-action-list) (error "Non Sequitur"))
-    (funcall (caddar proof-action-list) (caar proof-action-list))
-    (setq proof-action-list (cdr proof-action-list))
-    (while (and proof-action-list
-		(string= (cadar proof-action-list) "COMMENT"))
-      (funcall (caddar proof-action-list) (caar proof-action-list))
-      (setq proof-action-list (cdr proof-action-list)))
-    (if (null proof-action-list)
-	(progn (proof-release-lock)
-	       (proof-segment-buffer proof-locked-hwm proof-locked-hwm)
-	       t)
-      (proof-send (cadar proof-action-list))
-      nil)))
+    (let ((item (car proof-action-list)))
+      (funcall (nth 2 item) (car item))
+      (setq proof-action-list (cdr proof-action-list))
+      (while (and proof-action-list
+		(string= 
+		 (nth 1 (setq item (car proof-action-list))) 
+		 "COMMENT"))
+	(funcall (nth 2 item) (car item))
+	(setq proof-action-list (cdr proof-action-list)))
+      (if (null proof-action-list)
+	  (progn (proof-release-lock)
+		 (proof-detach-queue)
+		 t)
+	(proof-send (nth 1 item))
+	nil))))
 
 (defun proof-shell-insert-loopback-cmd  (cmd)
   "Insert command sequence triggered by the proof process
@@ -817,10 +706,10 @@ at the end of locked region (after inserting a newline)."
       (proof-goto-end-of-locked)
       (newline)
       (insert cmd)
-      (setq ext (make-span (proof-end-of-locked) (point)))
+      (setq ext (make-span (proof-locked-end) (point)))
       (set-span-property ext 'type 'pbp)
       (set-span-property ext 'cmd cmd)
-      (proof-segment-buffer (proof-end-of-locked) (point))
+      (proof-set-queue-endpoints (proof-locked-end) (point))
       (setq proof-action-list 
 	    (cons (car proof-action-list) 
 		  (cons (list ext cmd 'proof-done-advancing)
@@ -828,13 +717,14 @@ at the end of locked region (after inserting a newline)."
 
 (defun proof-shell-popup-eager-annotation ()
   (let (mrk str file module)
-    (save-excursion ;; BROKEN - MAY BE MULTI
+    (save-excursion ;; BROKEN - THERE MAY BE MULTIPLE EAGER ANNOTATIONS
       (goto-char (point-max))
       (search-backward proof-shell-eager-annotation-start)
       (setq mrk (+ 1 (point)))
       (search-forward proof-shell-eager-annotation-end)
       (setq str (buffer-substring mrk (- (point) 1)))
       (display-buffer (set-buffer proof-pbp-buffer))
+      (goto-char (point-max))
       (insert str "\n"))
     (if (string-match "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]" str)
 	(progn
@@ -859,27 +749,30 @@ at the end of locked region (after inserting a newline)."
 	    (backward-delete-char 1)
 	    (set-marker proof-marker (point)))
 	(let (string res cmd)	
-	    (re-search-forward proof-shell-annotated-prompt-regexp nil t)
-	    (backward-char (- (match-end 0) (match-beginning 0)))
-	    (setq string (buffer-substring (marker-position proof-marker)
-					   (point)))
-	    (goto-char (point-max))
-	    (backward-delete-char 1)
-	    (setq cmd (cadar proof-action-list))
-	    (save-excursion
-	      (setq res (proof-shell-process-output cmd string))
-	      (cond
-	       ((and (consp res) (eq (car res) 'error))
-		(proof-shell-handle-error cmd (cdr res)))
-	       ((and (consp res) (eq (car res) 'loopback))
-		(proof-shell-insert-loopback-cmd (cdr res))
-		(proof-shell-exec-loop))
-	       (t (if (proof-shell-exec-loop)
-		      (proof-shell-handle-delayed-output)))))))))
+	  (goto-char (marker-position proof-marker))
+	  (re-search-forward proof-shell-annotated-prompt-regexp nil t)
+	  (backward-char (- (match-end 0) (match-beginning 0)))
+	  (setq string (buffer-substring (marker-position proof-marker)
+					 (point)))
+	  (goto-char (point-max))
+	  (backward-delete-char 1)
+	  (setq cmd (nth 1 (car proof-action-list)))
+	  (save-excursion
+	    (setq res (proof-shell-process-output cmd string))
+	    (cond
+	     ((and (consp res) (eq (car res) 'error))
+	      (proof-shell-handle-error cmd (cdr res)))
+	     ((eq res 'interrupt)
+	      (proof-shell-handle-interrupt))
+	     ((and (consp res) (eq (car res) 'loopback))
+	      (proof-shell-insert-loopback-cmd (cdr res))
+	      (proof-shell-exec-loop))
+	     (t (if (proof-shell-exec-loop)
+		    (proof-shell-handle-delayed-output)))))))))
 
 (defun proof-last-goal-or-goalsave ()
   (save-excursion
-    (let ((ext (span-at-before (proof-end-of-locked) 'type)))
+    (let ((ext (span-at-before (proof-locked-end) 'type)))
     (while (and ext 
 		(not (eq (span-property ext 'type) 'goalsave))
 		(or (eq (span-property ext 'type) 'comment)
@@ -906,7 +799,7 @@ at the end of locked region (after inserting a newline)."
     (let ((flist proof-included-files-list) 
 	  (file (expand-file-name (buffer-file-name))) ext cmd)
       (if (string-match "\\(.*\\)\\.." file) (setq file (match-string 1 file)))
-      (while (and flist (not (string= file (cdar flist))))
+      (while (and flist (not (string= file (cdr (car flist)))))
 	(setq flist (cdr flist)))
       (if (null flist) 
 	  (if (not (y-or-n-p "Steal script management? " )) (error "Aborted"))
@@ -916,14 +809,14 @@ at the end of locked region (after inserting a newline)."
 	(setq ext (proof-last-goal-or-goalsave))
 	(setq cmd (if (and ext (not (eq (span-property ext 'type) 'goalsave)))
 		      proof-kill-goal-command ""))
-	(proof-segment-buffer nil nil)
+	(proof-detach-segments)
 	(delete-spans (point-min) (point-max) 'type))      
       (setq proof-script-buffer (current-buffer))
-      (proof-segment-buffer nil nil)
+      (proof-detach-segments)
 
       (cond 
        (flist
-	 (list nil (concat cmd "ForgetMark " (caar flist) ";")
+	 (list nil (concat cmd "ForgetMark " (car (car flist)) ";")
 	       `(lambda (ext) (setq proof-included-files-list 
 				    (quote ,(cdr flist))))))
 	((not (string= cmd ""))
@@ -969,15 +862,16 @@ at the end of locked region (after inserting a newline)."
   (let (ext)
     (proof-goto-end-of-locked)
     (insert cmd)
-    (setq ext (make-span (proof-end-of-locked) (point)))
+    (setq ext (make-span (proof-locked-end) (point)))
     (set-span-property ext 'type 'pbp)
     (set-span-property ext 'cmd cmd)
-    (proof-start-queue (proof-end-of-locked) (point) 
+    (proof-start-queue (proof-locked-end) (point) 
 		       (list (list ext cmd 'proof-done-advancing)))))
 
 (defun proof-done-advancing (ext)
-  (let ((end (span-end ext)) nam gext next cmd)
-    (proof-segment-buffer end proof-queue-loose-end)
+  (let ((end (span-end ext)) nam gext next cmd str start)
+    (proof-set-locked-end end)
+    (proof-set-queue-start end)
     (setq cmd (span-property ext 'cmd))
     (cond
      ((or (eq (span-property ext 'type) 'comment)
@@ -998,10 +892,30 @@ at the end of locked region (after inserting a newline)."
 			      (span-property gext 'cmd))
 		(setq nam (match-string 2 cmd))
 	      (error "Oops... can't find Goal name!!!")))
-	(set-span-end gext end)
-	(set-span-property gext 'highlight 'mouse-face)
-	(set-span-property gext 'type 'goalsave)
-	(set-span-property gext 'name nam)))))
+
+;; This code's for nested goals in Coq, and shouldn't affect things in LEGO
+
+      (setq next (prev-span gext 'type))
+      (while (and next 
+		  (not (string-match proof-goal-command-regexp 
+				     (span-property next 'cmd))))
+	(setq next (prev-span next 'type)))
+	
+      (if next (progn
+		 (proof-unlock-locked)
+		 (setq str (buffer-substring (span-start gext) end))
+		 (delete-region (span-start gext) end)
+		 (goto-char (span-start next))
+		 (setq start (point))
+		 (insert str "\n\n")
+		 (setq end (point))
+		 (proof-lock-unlocked))
+	(setq start (span-start gext)))
+
+      (set-span-endpoints gext start end)  
+      (set-span-property gext 'highlight 'mouse-face)
+      (set-span-property gext 'type 'goalsave)
+      (set-span-property gext 'name nam)))))
   
 ; Create a list of (type,int,string) pairs from the end of the locked
 ; region to pos, denoting the command and the position of its
@@ -1014,7 +928,7 @@ at the end of locked region (after inserting a newline)."
 
 (defun proof-segment-up-to (pos)
   (save-excursion
-    (let ((str (make-string (- (buffer-size) (proof-end-of-locked) -10) ?x))
+    (let ((str (make-string (- (buffer-size) (proof-locked-end) -10) ?x))
 	  (i 0) (depth 0) (quote-parity t) done alist c)
      (proof-goto-end-of-locked)
      (while (not done)
@@ -1049,23 +963,24 @@ at the end of locked region (after inserting a newline)."
 	       (if (>= (point) pos) (setq done t) (setq i 0)))))))
      alist)))
 
-(defun proof-semis-to-vanillas (semis)
-  (let ((ct (proof-end-of-locked)) ext alist)
+(defun proof-semis-to-vanillas (semis &optional callback-fn)
+  (let ((ct (proof-locked-end)) ext alist semi)
     (while (not (null semis))
-      (setq ext (make-span ct (caddar semis))
-	    ct (caddar semis))
-      (if (eq (caar semis) 'cmd)
+      (setq semi (car semis)
+            ext (make-span ct (nth 2 semi))
+	    ct (nth 2 semi))
+      (if (eq (car (car semis)) 'cmd)
 	  (progn
 	    (set-span-property ext 'type 'vanilla)
-	    (set-span-property ext 'cmd (cadar semis))
-	    (setq alist (cons (list ext (cadar semis) 'proof-done-advancing)
+	    (set-span-property ext 'cmd (nth 1 semi))
+	    (setq alist (cons (list ext (nth 1 semi) 
+				    (or callback-fn 'proof-done-advancing))
 			      alist)))
 	(set-span-property ext 'type 'comment)
 	(setq alist (cons (list ext "COMMENT" 'proof-done-advancing) alist)))
 	(setq semis (cdr semis)))
     (nreverse alist)))
 
-; 
 
 (defun proof-assert-until-point
   (&optional unclosed-comment-fun ignore-proof-process-p)
@@ -1078,7 +993,7 @@ at the end of locked region (after inserting a newline)."
   (let ((pt  (point)) semis crowbar)
     (setq crowbar (proof-steal-process))
     (save-excursion
-      (if (not (re-search-backward "\\S-" (proof-end-of-locked) t))
+      (if (not (re-search-backward "\\S-" (proof-locked-end) t))
 	  (progn (goto-char pt)
 		 (error "Nothing to do!")))
       (setq semis (proof-segment-up-to (point))))
@@ -1087,11 +1002,58 @@ at the end of locked region (after inserting a newline)."
       (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis)))
       (if (and (not ignore-proof-process-p) (not crowbar) (null semis))
 	  (error "Nothing to do!"))
-      (goto-char (caddar semis))
+      (goto-char (nth 2 (car semis)))
       (and (not ignore-proof-process-p)
 	   (let ((vanillas (proof-semis-to-vanillas (nreverse semis))))
 	     (if crowbar (setq vanillas (cons crowbar vanillas)))
-	     (proof-start-queue (proof-end-of-locked) (point) vanillas))))))
+	     (proof-start-queue (proof-locked-end) (point) vanillas))))))
+
+(defun proof-done-trying (ext)
+  (proof-detach-queue))
+			
+(defun proof-try-command
+  (&optional unclosed-comment-fun) 
+
+  "Process the command at point,
+   but don't add it to the locked region. This will only happen if
+   the command passes proof-state-preserving-p.
+
+   Default action if inside a comment is just to go until the start of
+   the comment. If you want something different, put it inside
+   unclosed-comment-fun."
+  (interactive)
+  (let ((pt  (point)) semis crowbar test)
+    (setq crowbar (proof-steal-process))
+    (save-excursion
+      (if (not (re-search-backward "\\S-" (proof-locked-end) t))
+	  (progn (goto-char pt)
+		 (error "Nothing to do!")))
+      (setq semis (proof-segment-up-to (point))))
+    (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis)))
+	(funcall unclosed-comment-fun)
+      (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis)))
+      (if (and (not crowbar) (null semis)) (error "Nothing to do!"))
+      (setq test (car semis))
+      (if (not (funcall proof-state-preserving-p (nth 1 test)))
+	  (error "Command is not state preserving"))
+      (goto-char (nth 2 test))
+      (let ((vanillas (proof-semis-to-vanillas (list test)
+					       'proof-done-trying)))
+	(if crowbar (setq vanillas (cons crowbar vanillas)))
+	(proof-start-queue (proof-locked-end) (point) vanillas)))))
+
+(defun proof-interrupt-process ()
+  (interactive)
+  (if (not (proof-shell-live-buffer))
+      (error "Proof Process Not Started!"))
+  (if (not (eq proof-script-buffer (current-buffer)))
+      (error "Don't own process!"))
+  (if (not proof-shell-busy)
+      (error "Proof Process Not Active!"))
+  (save-excursion
+    (set-buffer proof-shell-buffer)
+    (comint-interrupt-subjob)))
+  
     
 (defun proof-find-next-terminator ()
   "Set point after next `proof-terminal-char'."
@@ -1106,10 +1068,11 @@ deletes the region corresponding to the proof sequence."
   (let ((start (span-start ext))
         (end (span-end ext))
 	(kill (span-property ext 'delete-me)))
-    (proof-segment-buffer start proof-queue-loose-end)
+    (proof-set-locked-end start)
+    (proof-set-queue-end start)
     (delete-spans start end 'type)
     (delete-span ext)
-    (and kill (delete-region start end))))
+    (if kill (delete-region start end))))
 
 (defun proof-setup-retract-action (start end proof-command delete-region)
   (let ((span (make-span start end)))
@@ -1126,7 +1089,7 @@ deletes the region corresponding to the proof sequence."
   (interactive)
   (proof-check-process-available)
   (let ((sext (span-at (point) 'type)))
-    (if (null (proof-end-of-locked)) (error "No locked region"))
+    (if (null (proof-locked-end)) (error "No locked region"))
     (if (null sext) (error "Outside locked region"))
     (funcall proof-retract-target-fn sext delete-region)))
 
@@ -1136,7 +1099,7 @@ deletes the region corresponding to the proof sequence."
    proof script and in the proof process. In particular, it deletes
    the corresponding part of the proof script."
   (interactive)
-  (goto-char (span-start (span-at-before (proof-end-of-locked) 'type)))
+  (goto-char (span-start (span-at-before (proof-locked-end) 'type)))
   (proof-retract-until-point t))
 
 (defun proof-restart-script ()
@@ -1146,7 +1109,7 @@ deletes the region corresponding to the proof sequence."
 	(progn
 	  (set-buffer proof-script-buffer)
 	  (delete-spans (point-min) (point-max) 'type)
-	  (proof-segment-buffer nil nil)))
+	  (proof-detach-segments)))
     (setq proof-shell-busy nil
 	  proof-script-buffer nil)
     (if (buffer-live-p proof-shell-buffer) 
@@ -1154,6 +1117,16 @@ deletes the region corresponding to the proof sequence."
     (if (buffer-live-p proof-pbp-buffer)
 	(kill-buffer proof-pbp-buffer))))
 
+(defun proof-frob-locked-end ()
+  (interactive)
+  "Move the end of the locked region backwards. 
+   Only for use by consenting adults."
+  (if (> (point) (proof-locked-end))
+      (error "Can only move backwards")
+    (proof-set-locked-end (point))
+    (delete-spans (proof-locked-end) (point-max) 'type)))
+
+
 	  
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;          Active terminator minor mode                            ;;
@@ -1197,7 +1170,7 @@ current command."
   "Insert the terminator in an intelligent way and assert until the new terminator."
   (let ((mrk (point)) ins)
     (if (looking-at "\\s-\\|\\'\\|\\w") 
-	(if (not (re-search-backward "\\S-" (proof-end-of-locked) t))
+	(if (not (re-search-backward "\\S-" (proof-locked-end) t))
 	    (error "Nothing to do!")))
     (if (not (= (char-after (point)) proof-terminal-char))
 	(progn (forward-char) (insert proof-terminal-string) (setq ins t)))
@@ -1250,13 +1223,13 @@ current command."
 
   (define-key proof-mode-map [(control c) (control e)]
     'proof-find-next-terminator)
-
+  (define-key proof-mode-map [(control c) (control c)] 'proof-interrupt-process)
   (define-key proof-mode-map proof-terminal-char 'proof-active-terminator)
-  (define-key proof-mode-map [(control c) (control a)]    'proof-assert-until-point)
-  (define-key proof-mode-map [(control c) u]    'proof-retract-until-point)
+  (define-key proof-mode-map [(control c) (return)] 'proof-assert-until-point)
+  (define-key proof-mode-map [(control c) (control t)] 'proof-try-command)
+  (define-key proof-mode-map [(control c) u] 'proof-retract-until-point)
   (define-key proof-mode-map [(control c) (control u)] 'proof-undo-last-successful-command)
-  (define-key proof-mode-map [(control c) ?']
-  'proof-goto-end-of-locked)
+  (define-key proof-mode-map [(control c) ?'] 'proof-goto-end-of-locked)
 
   ;; For fontlock
   (remove-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer t)
@@ -1275,18 +1248,8 @@ current command."
   (setq proof-shell-delayed-output (cons 'insert "done"))
   (setq comint-prompt-regexp proof-shell-prompt-pattern)
   (add-hook 'comint-output-filter-functions 'proof-shell-filter nil t)
-;  (add-hook 'comint-output-filter-functions 'comint-truncate-buffer nil t)
-;  (setq comint-buffer-maximum-size 10000)
-;
-
-  (let ((disp (make-display-table))
-	(i 128))
-	(while (< i 256)
-	  (aset disp i "")
-	  (incf i))
-	(add-spec-to-specifier current-display-table disp (current-buffer)))
-		  
-  (setq comint-append-old-input nil)
+  (setq comint-get-old-input (function (lambda () "")))
+  (proof-dont-show-annotations)
   (setq proof-marker (make-marker)))
 
 (defun proof-shell-config-done ()
diff --git a/todo b/todo
new file mode 100644
index 00000000..4d1a73b1
--- /dev/null
+++ b/todo
@@ -0,0 +1,27 @@
+This is a list of things which need doing to the lego mode.
+
+* Fixing up errors caused by pbp-generated commands.
+
+* undo support for LEGO needs to consider Discharge; perhaps unrol to
+  the beginning of the module?
+
+* pbp code doesn't quite accord with the tech report; in particular it
+  decodes annotations eagerly. Lazily would be faster, and it's what
+  the tech report claims
+
+* It would be nice to have a version ported to emacs19 (or
+  20). Unfortunately, it's currently impossible to port the pbp code,
+  since emacs19 doesn't properly handle highlighting of nested
+  overlays. The bulk of the stuff dependent on which version of emacs
+  is running has been moved to proof-dependencies.el, but there are
+  doubtless differences in font-locking and menu code which will
+  require some work.
+
+* Indentation - LEGO should indent only with brackets; Coq for Inductive
+  definitions and 'case' constructs also.
+
+* file handling could be more robust
+
+* For Coq:
+   Fill in proof-shell-interrupt-regexp
+   Fill in proof-state-preserving-p