Renamed for new subdirectory structure

1 files changed, 0 insertions, 1838 deletions

diff --git a/proof.el b/proof.el
deleted file mode 100644
index c37f863b..00000000
--- a/proof.el
+++ /dev/null
@@ -1,1838 +0,0 @@
-;; proof.el Major mode for proof assistants
-;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
-;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
-;;          Thomas Kleymann and Dilip Sequeira
-
-;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
-;; Thanks to Robert Boyer, Rod Burstall,
-;;           James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens  
-
-
-(require 'cl)
-(require 'compile)
-(require 'comint)
-(require 'etags)
-(cond ((fboundp 'make-extent) (require 'span-extent))
-      ((fboundp 'make-overlay) (require 'span-overlay))
-      (t nil))
-(require 'proof-syntax)
-(require 'proof-indent)
-(require 'easymenu)
-(require 'tl-list)
-
-(autoload 'w3-fetch "w3" nil t)
-
-(defmacro deflocal (var value docstring)
- (list 'progn
-   (list 'defvar var 'nil docstring)
-   (list 'make-variable-buffer-local (list 'quote var))
-   (list 'setq var value)))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Generic config for proof assistant				    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defvar proof-assistant ""
-  "Name of the proof assistant")
-
-(defvar proof-www-home-page ""
-  "Web address for information on proof assistant")
-
-(defvar proof-shell-cd nil
-  "*Command of the inferior process to change the directory.")
-
-(defvar proof-shell-process-output-system-specific nil
-  "*Errors, start of proofs, abortions of proofs and completions of
-  proofs are recognised in the function `proof-shell-process-output'.
-  All other output from the proof engine is simply reported to the
-  user in the RESPONSE buffer.
-
-  To catch further special cases, set this variable to a tuple of
-  functions '(condf . actf). Both are given (cmd string) as arguments.
-  `cmd' is a string containing the currently processed command.
-  `string' is the response from the proof system. To change the
-  behaviour of `proof-shell-process-output', (condf cmd string) must
-  return a non-nil value. Then (actf cmd string) is invoked. See the
-  documentation of `proof-shell-process-output' for the required
-  output format.")
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Proof mode variables                                           ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defconst proof-mode-version-string
-  "PROOF-MODE. ALPHA Version 2 (August 1998) LEGO Team <lego@dcs.ed.ac.uk>")
-
-(defconst proof-info-dir "/usr/local/share/info"
-  "Directory to search for Info documents on Script Management.")
-
-(defconst proof-universal-keys
-  (list (cons '[(control c) (control c)] 'proof-interrupt-process)
-	(cons '[(control c) (control v)]
-	      'proof-execute-minibuffer-cmd)
-	(cons '[(meta tab)] 'tag-complete-symbol))
-  "List of keybindings which are valid in both in the script and the
-  response buffer. Elements of the list are tuples (k . f) 
-  where `k' is a keybinding (vector) and `f' the designated function.")
-
-(defvar proof-prog-name-ask-p nil
-  "*If t, you will be asked which program to run when the inferior
- process starts up.")
-
-
- 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  Other buffer-local variables used by proof mode                 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; These should be set before proof-config-done is called
-
-(defvar proof-terminal-char nil "terminator character")
-
-(defvar proof-comment-start nil "Comment start")
-(defvar proof-comment-end nil   "Comment end")
-
-(defvar proof-save-command-regexp nil "Matches a save command")
-(defvar proof-save-with-hole-regexp nil "Matches a named save command")
-(defvar proof-goal-with-hole-regexp nil "Matches a saved goal command")
-
-(defvar proof-goal-command-p nil "Is this a goal")
-(defvar proof-count-undos-fn nil "Compute number of undos in a target segment")
-(defvar proof-find-and-forget-fn nil "Compute command to forget up to point")
-
-(defvar proof-goal-hyp-fn nil
-  "A function which returns cons cell if point is at a goal/hypothesis.
-First element of cell is a symbol, 'goal' or 'hyp'.  The second
-element is a string: the goal or hypothesis itself.  This is used
-when parsing the proofstate output")
-
-(defvar proof-kill-goal-command nil "How to kill a goal.")
-(defvar proof-global-p nil
-  "Is this a global declaration")
-
-(defvar proof-state-preserving-p nil
-  "A predicate, non-nil if its argument preserves the proof state")
-
-(defvar pbp-change-goal nil
-  "*Command to change to the goal %s")
-
-;; these should be set in proof-pre-shell-start-hook
-
-(defvar proof-prog-name nil "program name for proof shell")
-(defvar proof-mode-for-shell nil "mode for proof shell")
-(defvar proof-mode-for-pbp nil "The actual mode for Proof-by-Pointing.")
-(defvar proof-shell-insert-hook nil 
-  "Function to config proof-system to interface")
-
-(defvar proof-pre-shell-start-hook)
-(defvar proof-post-shell-exit-hook)
-
-(defvar proof-shell-prompt-pattern nil 
-   "comint-prompt-pattern for proof shell")
-
-(defvar proof-shell-init-cmd nil
-   "The command for initially configuring the proof process")
-
-(defvar proof-shell-handle-delayed-output-hook
-  '(proof-pbp-focus-on-first-goal)
-  "*This hook is called after output from the PROOF process has been
-  displayed in the RESPONSE buffer.")
-
-(defvar proof-shell-handle-error-hook
-  '(proof-goto-end-of-locked-if-pos-not-visible-in-window)
-  "*This hook is called after an error has been reported in the
-  RESPONSE buffer.")  
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  Generic config for script management                            ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defvar proof-shell-wakeup-char nil
-  "A character terminating the prompt in annotation mode")
-
-(defvar proof-shell-annotated-prompt-regexp ""
-  "Annotated prompt pattern")
-
-(defvar proof-shell-abort-goal-regexp nil
-  "*Regular expression indicating that the proof of the current goal
-  has been abandoned.")
-
-(defvar proof-shell-error-regexp nil
-  "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.")
-
-(defvar proof-shell-result-start ""
-  "String indicating the start of an output from the prover following
-  a `pbp-goal-command' or a `pbp-hyp-command'.")
-
-(defvar proof-shell-result-end ""
-  "String indicating the end of an output from the prover following a
-  `pbp-goal-command' or a `pbp-hyp-command'.") 
-
-(defvar proof-shell-start-goals-regexp ""
-  "String indicating the start of the proof state.")
-
-(defvar proof-shell-end-goals-regexp ""
-  "String indicating the end of the proof state.")
-
-(defvar pbp-error-regexp nil
-  "A regular expression indicating that the PROOF process has
-  identified an error.") 
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  Internal variables used by scripting and pbp                    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defvar proof-mode-name "Proof")
-
-(defvar proof-shell-echo-input t
-  "If nil, input to the proof shell will not be echoed")
-
-(defvar proof-terminal-string nil 
-  "End-of-line string for proof process.")
-
-(defvar proof-re-end-of-cmd nil 
-  "You are not authorised for this information.")
-
-(defvar proof-re-term-or-comment nil 
-  "You are not authorised for this information.")
-
-(defvar proof-marker nil 
-  "You are not authorised for this information.")
-
-(defvar proof-shell-buffer nil
-  "You are not authorised for this information.")
-
-(defvar proof-script-buffer nil
-  "You are not authorised for this information.")
-
-(defvar proof-pbp-buffer nil
-  "You are not authorised for this information.")
-
-(defvar proof-shell-busy nil 
-  "You are not authorised for this information.")
-
-(deflocal proof-buffer-type nil 
-  "You are not authorised for this information.")
-
-(defvar proof-action-list nil "action list")
-
-(defvar proof-included-files-list nil 
-  "Files currently included in proof process")
-
-(deflocal proof-active-buffer-fake-minor-mode nil
-  "An indication in the modeline that this is the *active* buffer")
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; A couple of small utilities                                      ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun proof-define-keys (map kbl)
-  "Adds keybindings `kbl' in `map'. The argument `kbl' is a list of
-  tuples (k . f) where `k' is a keybinding (vector) and `f' the
-  designated function."
-  (mapcar
-   (lambda (kbl)
-     (let ((k (car kbl)) (f (cdr kbl)))
-         (define-key map k f)))
-   kbl))
-
-(defun proof-string-to-list (s separator) 
-  "converts strings `s' separated by the character `separator' to a
-  list of words" 
-  (let ((end-of-word-occurence (string-match (concat separator "+") s)))
-    (if (not end-of-word-occurence)
-        (if (string= s "") 
-            nil
-          (list s))
-      (cons (substring s 0 end-of-word-occurence) 
-            (proof-string-to-list 
-             (substring s
-                        (string-match (concat "[^" separator "]")
-                                      s end-of-word-occurence)) separator)))))
-
-;; FIXME: this doesn't belong here  (and shouldn't be called w3-* !!)
-(defun w3-remove-file-name (address)
-  "remove the file name in a World Wide Web address"
-  (string-match "://[^/]+/" address)
-  (concat (substring address 0 (match-end 0))
-          (file-name-directory (substring address (match-end 0)))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Basic code for the locked region and the queue region            ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(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-locked-span nil
-  "Upper limit of the locked region")
-
-(defvar proof-queue-span nil
-  "Upper limit of the locked region")
-
-(make-variable-buffer-local 'proof-locked-span)
-(make-variable-buffer-local 'proof-queue-span)
-
-(defun proof-init-segmentation ()
-  (setq proof-queue-loose-end nil)
-  (if (not proof-queue-span)
-      (setq proof-queue-span (make-span 1 1)))
-  (set-span-property proof-queue-span 'start-closed t)
-  (set-span-property proof-queue-span 'end-open t)
-  (span-read-only proof-queue-span)
-
-  (make-face 'proof-queue-face)
-  ;; Whether display has color or not
-  (cond ((and (fboundp 'device-class)
-	      (eq (device-class (frame-device)) 'color))
-	 (set-face-background 'proof-queue-face "mistyrose"))
-	((and (fboundp 'x-display-color-p) (x-display-color-p))
-	 (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)
-  
-  (setq proof-locked-hwm nil)
-  (if (not proof-locked-span)
-      (setq proof-locked-span (make-span 1 1)))
-  (set-span-property proof-locked-span 'start-closed t)
-  (set-span-property proof-locked-span 'end-open t)
-  (span-read-only proof-locked-span)
-
-  (make-face 'proof-locked-face)
-  ;; Whether display has color or not
-  (cond ((and (fboundp 'device-class)
-	      (eq (device-class (frame-device)) 'color))
-	 (set-face-background 'proof-locked-face "lavender"))
-	((and (fboundp 'x-display-color-p) (x-display-color-p))
-	 (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))
-
-(defsubst proof-lock-unlocked ()
-  (span-read-only proof-locked-span))
-
-(defsubst proof-unlock-locked ()
-  (span-read-write proof-locked-span))
-
-(defsubst proof-set-queue-endpoints (start end)
-  (set-span-endpoints proof-queue-span start end))
-
-(defsubst proof-set-locked-endpoints (start end)
-  (set-span-endpoints proof-locked-span start end))
-
-(defsubst proof-detach-queue ()
-  (and proof-queue-span (detach-span proof-queue-span)))
-
-(defsubst proof-detach-locked ()
-  (and proof-locked-span (detach-span proof-locked-span)))
-
-(defsubst proof-set-queue-start (start)
-  (set-span-endpoints proof-queue-span start (span-end proof-queue-span)))
-
-(defsubst proof-set-queue-end (end)
-  (set-span-endpoints proof-queue-span (span-start proof-queue-span) end))
-
-(defun proof-detach-segments ()
-  (proof-detach-queue)
-  (proof-detach-locked))
-
-(defsubst proof-set-locked-end (end)
-  (if (>= (point-min) end)
-      (proof-detach-locked)
-    (set-span-endpoints proof-locked-span (point-min) end)))
-
-(defun proof-unprocessed-begin ()
-  "proof-unprocessed-begin returns end of locked region in script
-  buffer and point-min otherwise."
-  (or 
-   (and (eq proof-script-buffer (current-buffer))
-	proof-locked-span (span-end proof-locked-span))
-   (point-min)))
-
-(defun proof-locked-end ()
-  "proof-locked-end returns the end of the locked region.  It should
-  only be called if we're in the scripting buffer."
-  (if (eq proof-script-buffer (current-buffer))
-      (proof-unprocessed-begin)
-    (error "bug: proof-locked-end called from wrong buffer")))
-
-(defsubst proof-end-of-queue ()
-  (and proof-queue-span (span-end proof-queue-span)))
-
-(defun proof-dont-show-annotations ()
-  "This sets the display values of the annotations used to
-   communicate with the proof assistant so that they don't show up on
-   the screen."
-  (let ((disp (make-display-table))
-	(i 128))
-	(while (< i 256)
-	  (aset disp i [])
-	  (incf i))
-	(cond ((fboundp 'add-spec-to-specifier)
-	       (add-spec-to-specifier current-display-table disp
-				      (current-buffer)))
-	      ((boundp 'buffer-display-table)
-	       (setq buffer-display-table disp)))))
-
-;;; 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)))))
-
-;; The package fume-func provides a function with the same name and
-;; specification. However, fume-func's version is incorrect.
-(and (fboundp 'fume-match-find-next-function-name)
-(defun fume-match-find-next-function-name (buffer)
-  "General next function name in BUFFER finder using match.
-  The regexp is assumed to be a two item list the car of which is the regexp
-  to use, and the cdr of which is the match position of the function name"
-  (set-buffer buffer)
-  (let ((r (car fume-function-name-regexp))
-        (p (cdr fume-function-name-regexp)))
-    (and (re-search-forward r nil t)
-	 (cons (buffer-substring (setq p (match-beginning p)) (point)) p)))))
-
-(defun proof-goto-end-of-locked-interactive ()
-  "Jump to the end of the locked region."
-  (interactive)
-  (switch-to-buffer proof-script-buffer)
-  (goto-char (proof-locked-end)))
-
-(defun proof-goto-end-of-locked ()
-  "Jump to the end of the locked region."
-  (goto-char (proof-locked-end)))
-
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window ()
-  "If the end of the locked region is not visible, jump to the end of
-  the locked region."
-  (interactive)
-  (let ((pos (save-excursion
-	       (set-buffer proof-script-buffer)
-	       (proof-locked-end))))
-    (or (pos-visible-in-window-p pos (get-buffer-window
-				      proof-script-buffer t))
-        (proof-goto-end-of-locked-interactive))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  Starting and stopping the proof-system shell                    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun proof-shell-live-buffer () 
-  (and proof-shell-buffer
-       (comint-check-proc proof-shell-buffer)
-       proof-shell-buffer))
-
-(defun proof-start-shell ()
-  (if (proof-shell-live-buffer)
-      ()
-    (run-hooks 'proof-pre-shell-start-hook)
-    (setq proof-included-files-list nil)
-    (if proof-prog-name-ask-p
-	(save-excursion
-	  (setq proof-prog-name (read-shell-command "Run process: "
-						    proof-prog-name))))
-    (let ((proc
-	   (concat "Inferior "
-		   (substring proof-prog-name
-			      (string-match "[^/]*$" proof-prog-name)))))
-      (while (get-buffer (concat "*" proc "*"))
-	(if (string= (substring proc -1) ">")
-	    (aset proc (- (length proc) 2) 
-		  (+ 1 (aref proc (- (length proc) 2))))
-	  (setq proc (concat proc "<2>"))))
-
-      (message (format "Starting %s process..." proc))
-
-      ;; Starting the inferior process (asynchronous)
-      (let ((prog-name-list (proof-string-to-list proof-prog-name " ")))
-	(apply 'make-comint  (append (list proc (car prog-name-list) nil)
-				     (cdr prog-name-list))))
-      ;; To send any initialisation commands to the inferior process,
-      ;; consult proof-shell-config-done...
-
-      (setq proof-shell-buffer (get-buffer (concat "*" proc "*")))
-      (setq proof-pbp-buffer (get-buffer-create (concat "*" proc "-goals*")))
-
-      (save-excursion
-	(set-buffer proof-shell-buffer)
-	(funcall proof-mode-for-shell)
-	(set-buffer proof-pbp-buffer)
-	(funcall proof-mode-for-pbp))
-
-      (setq proof-script-buffer (current-buffer))
-      (proof-init-segmentation)
-      (setq proof-active-buffer-fake-minor-mode t)
-
-      (if (fboundp 'redraw-modeline)
-	  (redraw-modeline)
-	(force-mode-line-update))
-
-      (or (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist)
-	  (setq minor-mode-alist
-		(append minor-mode-alist
-			(list '(proof-active-buffer-fake-minor-mode 
-				" Scripting")))))
-
-      (message 
-       (format "Starting %s process... done." proc)))))
-  
-
-(defun proof-stop-shell ()
-  "Exit the PROOF process
-
-  Runs proof-shell-exit-hook if non nil"
-
-  (interactive)
-  (save-excursion
-    (let ((buffer (proof-shell-live-buffer)) (proc))
-      (if buffer
-	  (progn
-	    (save-excursion
-	      (set-buffer buffer)
-	      (setq proc (process-name (get-buffer-process)))
-	      (comint-send-eof)
-	      (save-excursion
-		(set-buffer proof-script-buffer)
-		(proof-detach-segments))
-	      (kill-buffer))
-	    (run-hooks 'proof-shell-exit-hook)
-
-             ;;it is important that the hooks are
-	     ;;run after the buffer has been killed. In the reverse
-	     ;;order e.g., intall-shell-fonts causes problems and it
-	     ;;is impossible to restart the PROOF shell
-
-	    (message (format "%s process terminated." proc)))))))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;          Proof by pointing                                       ;;
-;;          All very lego-specific at present                       ;;
-;;          To make sense of this code, you should read the         ;;
-;;          relevant LFCS tech report by tms, yb, and djs           ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-
-(defvar pbp-goal-command nil
-  "Command informing the prover that `pbp-button-action' has been
-  requested on a goal.")
-
-(defvar pbp-hyp-command nil
-  "Command informing the prover that `pbp-button-action' has been
-  requested on an assumption.")
-
-(defun pbp-button-action (event)
-   (interactive "e")
-   (mouse-set-point event)
-   (pbp-construct-command))
-
-; Using the spans in a mouse behavior is quite simple: from the
-; mouse position, find the relevant span, then get its annotation
-; and produce a piece of text that will be inserted in the right
-; buffer.  
-
-(defun proof-expand-path (string)
-  (let ((a 0) (l (length string)) ls)
-    (while (< a l) 
-      (setq ls (cons (int-to-string (aref string a)) 
-		     (cons " " ls)))
-      (incf a))
-    (apply 'concat (nreverse ls))))
-
-(defun proof-send-span (event)
-  (interactive "e")
-  (let* ((span (span-at (mouse-set-point event) 'type))
-	 (str (span-property span 'cmd)))
-    (cond ((and (eq proof-script-buffer (current-buffer)) (not (null span)))
-	   (proof-goto-end-of-locked)
-	   (cond ((eq (span-property span 'type) 'vanilla)
-		  (insert str)))))))
-
-(defun pbp-construct-command ()
-  (let* ((span (span-at (point) 'proof))
-	 (top-span (span-at (point) 'proof-top-element))
-	 top-info)
-    (if (null top-span) ()
-      (setq top-info (span-property top-span 'proof-top-element))
-      (pop-to-buffer proof-script-buffer)
-      (cond
-       (span
-	(proof-invisible-command 
-	 (format (if (eq 'hyp (car top-info)) pbp-hyp-command 
-		                              pbp-goal-command)
-		 (concat (cdr top-info) (proof-expand-path 
-					 (span-property span 'proof))))))
-       ((eq (car top-info) 'hyp)
-	(proof-invisible-command (format pbp-hyp-command (cdr top-info))))
-       (t
-	 (proof-insert-pbp-command (format pbp-change-goal (cdr top-info))))))
-    ))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;          Turning annotated output into pbp goal set              ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defvar proof-shell-first-special-char nil "where the specials start")
-(defvar proof-shell-goal-char nil "goal mark")
-(defvar proof-shell-start-char nil "annotation start")
-(defvar proof-shell-end-char nil "annotation end")
-(defvar proof-shell-field-char nil "annotated field end")
-(defvar proof-shell-eager-annotation-start nil "eager ann. field start")
-(defvar proof-shell-eager-annotation-end nil "eager ann. field end")
-
-(defvar proof-shell-assumption-regexp nil
-  "A regular expression matching the name of assumptions.")
-
-;; FIXME: da: where is this variable used?  
-;;	      dropped in favour of goal-char?
-(defvar proof-shell-goal-regexp nil
-  "A regular expressin matching the identifier of a goal.")
-
-(defvar proof-shell-noise-regexp nil
-  "Unwanted information output from the proof process within
-  `proof-start-goals-regexp' and `proof-end-goals-regexp'.")
-
-(defun pbp-make-top-span (start end)
-  (let (span name)
-    (goto-char start)
-    ;; FIXME: why name?  This is a character function
-    (setq name (funcall proof-goal-hyp-fn))
-    (beginning-of-line)
-    (setq start (point))
-    (goto-char end)
-    (beginning-of-line)
-    (backward-char)
-    (setq span (make-span start (point)))
-    (set-span-property span 'mouse-face 'highlight)
-    (set-span-property span 'proof-top-element name)))
-
-
-;; Need this for processing error strings and so forth
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   The filter. First some functions that handle those few         ;;
-;;   occasions when the glorious illusion that is script-management ;;
-;;   is temporarily suspended                                       ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;;   Output from the proof process is handled lazily, so that only  
-;;   the output from the last of multiple commands is actually      
-;;   processed (assuming they're all successful)                    
-
-(defvar proof-shell-delayed-output nil
-  "The last interesting output the proof process output, and what to do
-   with it.")
-
-(defvar proof-analyse-using-stack nil
-  "Are annotations sent by proof assistant local or global")
-
-;; FIXME: da: what's magical value 128 below? should be in defconst?
-(defun proof-shell-analyse-structure (string)
-  (save-excursion
-    (let* ((ip 0) (op 0) ap (l (length string)) 
-	   (ann (make-string (length string) ?x))
-           (stack ()) (topl ()) 
-	   (out (make-string l ?x)) c span)
-      (while (< ip l)	
-	(if (< (setq c (aref string ip)) 128)
-	    (progn (aset out op c)
-		   (incf op)))
-	(incf ip))
-      (display-buffer (set-buffer proof-pbp-buffer))
-      (erase-buffer)
-      (insert (substring out 0 op))
-
-      (setq ip 0
-	    op 1)
-      (while (< ip l)
-	(setq c (aref string ip))
-	(cond
-	 ((= c proof-shell-goal-char)
-	  (setq topl (cons op topl))
-	  (setq ap 0))
-	 ((= c proof-shell-start-char)
-	  (if proof-analyse-using-stack
-	      (setq ap (- ap (- (aref string (incf ip)) 128)))
-	    (setq ap (- (aref string (incf ip)) 128)))
-	  (incf ip)
-	  (while (not (= (setq c (aref string ip)) proof-shell-end-char))
-	    (aset ann ap (- c 128))
-	    (incf ap)
-	    (incf ip))
-	  (setq stack (cons op (cons (substring ann 0 ap) stack))))
-	 ((= c proof-shell-field-char)
-	  (setq span (make-span (car stack) op))
-	  (set-span-property span 'mouse-face 'highlight)
-	  (set-span-property span 'proof (car (cdr stack)))
-	  ;; Pop annotation off stack
-	  (and proof-analyse-using-stack
-	       (progn
-		 (setq ap 0)
-		 (while (< ap (length (cadr stack)))
-		   (aset ann ap (aref (cadr stack) ap))
-		   (incf ap))))
-	  ;; Finish popping annotations
-	  (setq stack (cdr (cdr stack))))
-	 (t (incf op)))
-	(incf ip))
-      (setq topl (reverse (cons (point-max) topl)))
-      ;; If we want Coq pbp: (setq coq-current-goal 1)
-      (while (setq ip (car topl) 
-		   topl (cdr topl))
-	(pbp-make-top-span ip (car topl))))))
-
-(defun proof-shell-strip-annotations (string)
-  (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x )))
-    (while (< ip l)
-      (if (>= (aref string ip) proof-shell-first-special-char)
-	  (if (char-equal (aref string ip) proof-shell-start-char)
-	      (progn (incf ip)
-		     (while (< (aref string ip) proof-shell-first-special-char)
-		       (incf ip))))
-	(aset out op (aref string ip))
-	(incf op))
-      (incf ip))
-    (substring out 0 op)))
-
-(defun proof-shell-handle-delayed-output ()
-  (let ((ins (car proof-shell-delayed-output))
-	(str (cdr proof-shell-delayed-output)))
-    (display-buffer proof-pbp-buffer)
-    (save-excursion
-      (cond 
-       ((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))
-       (t (set-buffer proof-pbp-buffer)
-	  (insert "\n\nbug???")))))
-  (run-hooks 'proof-shell-handle-delayed-output-hook)
-  (setq proof-shell-delayed-output (cons 'insert "done")))
-
-(defun proof-shell-handle-error (cmd string)
-  (save-excursion
-    (display-buffer (set-buffer proof-pbp-buffer))
-    (if (not (eq proof-shell-delayed-output (cons 'insert "done")))
-	(progn
-	  (set-buffer proof-pbp-buffer)
-	  (erase-buffer)
-	  (insert (proof-shell-strip-annotations 
-		   (cdr proof-shell-delayed-output)))))
-    (goto-char (point-max))
-    (if (re-search-backward pbp-error-regexp nil t) 
-	(delete-region (- (point) 2) (point-max)))
-    (newline 2)
-    (insert-string string)
-    (beep))
-  (set-buffer proof-script-buffer)
-  (proof-detach-queue)
-  (delete-spans (proof-locked-end) (point-max) 'type)
-  (proof-release-lock)
-  (run-hooks 'proof-shell-handle-error-hook))
-
-(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))))
-
-
-(defun proof-goals-pos (span maparg)
-  "Given a span, this function returns the start of it if corresponds
-  to a goal and nil otherwise."
- (and (eq 'goal (car (span-property span 'proof-top-element)))
-		(span-start span)))
-
-(defun proof-pbp-focus-on-first-goal ()
-  "If the `proof-pbp-buffer' contains goals, the first one is brought
-  into view."
-  (and (fboundp 'map-extents)
-       (let
-	   ((pos (map-extents 'proof-goals-pos proof-pbp-buffer
-			      nil nil nil nil 'proof-top-element)))
-	 (and pos (set-window-point
-		   (get-buffer-window proof-pbp-buffer t) pos)))))
-
-           
-
-(defun proof-shell-process-output (cmd string)
-  "Deals with errors, start of proofs, abortions of proofs and
-  completions of proofs. All other output from the proof engine is
-  simply reported to the user in the RESPONSE buffer. To extend this
-  function, set `proof-shell-process-output-system-specific'.
-
-  The basic output processing function - it can return one of 4  
-  things: 'error, 'interrupt, 'loopback, or nil. 'loopback means this
-  was output from pbp, and should be inserted into the script buffer
-  and sent back to the proof assistant."
-  (cond 
-   ((string-match proof-shell-error-regexp string)
-    (cons 'error (proof-shell-strip-annotations 
-		  (substring string (match-beginning 0)))))
-
-   ((string-match proof-shell-interrupt-regexp string)
-    'interrupt)
-
-   ((and proof-shell-abort-goal-regexp
-	 (string-match proof-shell-abort-goal-regexp string))
-    (setq proof-shell-delayed-output (cons 'insert "\n\nAborted"))
-    ())
-	 
-   ((string-match proof-shell-proof-completed-regexp string)
-    (setq proof-shell-delayed-output
-	  (cons 'insert (concat "\n" (match-string 0 string)))))
-
-   ((string-match proof-shell-start-goals-regexp string)
-    (let (start end)
-      (while (progn (setq start (match-end 0))
-		    (string-match proof-shell-start-goals-regexp 
-				  string start)))
-      (setq end (string-match proof-shell-end-goals-regexp string start))
-      (setq proof-shell-delayed-output 
-	    (cons 'analyse (substring string start end)))))
-       
-   ((string-match proof-shell-result-start string)
-    (let (start end)
-      (setq start (+ 1 (match-end 0)))
-      (string-match proof-shell-result-end string)
-      (setq end (- (match-beginning 0) 1))
-      (cons 'loopback (substring string start end))))
-   
-   ;; hook to tailor proof-shell-process-output to a specific proof
-   ;; system  
-   ((and proof-shell-process-output-system-specific
-	 (funcall (car proof-shell-process-output-system-specific)
-		  cmd string))
-    (funcall (cdr proof-shell-process-output-system-specific)
-	     cmd string))
-
-   (t (setq proof-shell-delayed-output (cons 'insert string)))))
-         
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Low-level commands for shell communication                     ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun proof-shell-insert (string)
-  (set-buffer proof-shell-buffer)
-  (goto-char (point-max))
-
-  (run-hooks 'proof-shell-insert-hook)
-  (insert string)
-
-  ;; xemacs and emacs19 have different semantics for what happens when
-  ;; shell input is sent next to a marker
-  ;; the following code accommodates both definitions
-  (if (marker-position proof-marker)
-      (let ((inserted (point)))
-	(comint-send-input)
-	(set-marker proof-marker inserted))
-    (comint-send-input)))
-
-(defun proof-send (string)
-  (let ((l (length string)) (i 0))
-    (while (< i l)
-      (if (= (aref string i) ?\n) (aset string i ?\ ))
-      (incf i)))
-  (save-excursion (proof-shell-insert string)))
-
-;; Note that this is not really intended for anything complicated -
-;; just to stop the user accidentally sending a command while the
-;; queue is running.
-(defun proof-check-process-available (&optional relaxed)
-  "Checks
-     (1) Is a proof process running?
-     (2) Is the proof process idle?
-     (3) Does the current buffer own the proof process?
-     (4) Is the current buffer a proof script?
-    and signals an error if at least one of the conditions is not
-    fulfilled. If relaxed is set, only (1) and (2) are tested."
-  (if (proof-shell-live-buffer)
-      (cond
-       (proof-shell-busy (error "Proof Process Busy!"))
-       (relaxed ())			;exit cond
-       ((not (eq proof-script-buffer (current-buffer)))
-	(error "Don't own proof process"))))
-  (if (not (or relaxed (eq proof-buffer-type 'script)))
-      (error "Must be running in a script buffer")))
-
-(defun proof-grab-lock (&optional relaxed)
-  (proof-start-shell)
-  (proof-check-process-available relaxed)
-  (setq proof-shell-busy t))
-
-(defun proof-release-lock ()
-  (if (proof-shell-live-buffer)
-      (progn
-	(if (not proof-shell-busy)
-	    (error "Bug: Proof process not busy"))
-	(if (not (eq proof-script-buffer (current-buffer)))
-	    (error "Bug: Don't own process"))
-	(setq proof-shell-busy nil))))
-
-; Pass start and end as nil if the cmd isn't in the buffer.
-
-(defun proof-start-queue (start end alist &optional relaxed)
-  (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 relaxed) 
-	(setq proof-shell-delayed-output (cons 'insert "Done."))
-	(setq proof-action-list alist)
-	(proof-send (nth 1 item))))))
-
-; returns t if it's run out of input
-
-(defun proof-shell-exec-loop ()
-  (save-excursion
-    (set-buffer proof-script-buffer)
-    (if (null proof-action-list) (error "Non Sequitur"))
-    (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
-at the end of locked region (after inserting a newline and indenting)."
-  (save-excursion
-    (set-buffer proof-script-buffer)
-    (let (span)
-      (proof-goto-end-of-locked)
-      (newline-and-indent)
-      (insert cmd)
-      (setq span (make-span (proof-locked-end) (point)))
-      (set-span-property span 'type 'pbp)
-      (set-span-property span 'cmd cmd)
-      (proof-set-queue-endpoints (proof-locked-end) (point))
-      (setq proof-action-list 
-	    (cons (car proof-action-list) 
-		  (cons (list span cmd 'proof-done-advancing)
-			(cdr proof-action-list)))))))
-
-;; ******** NB **********
-;;  While we're using pty communication, this code is OK, since all
-;; eager annotations are one line long, and we get input a line at a
-;; time. If we go over to piped communication, it will break.
-
-(defun proof-shell-popup-eager-annotation ()
-  "Eager annotations are annotations which the proof system produces
-while it's doing something (e.g. loading libraries) to say how much
-progress it's made. Obviously we need to display these as soon as they
-arrive."
-  (let (mrk str file module)
-    (save-excursion 
-      (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
-	  (setq file (match-string 2 str)
-		module (match-string 1 str))
-	  (if (string= file "") 
-	      (setq file (buffer-file-name proof-script-buffer)))
-	  (setq file (expand-file-name file))
-	  (if (string-match "\\(.*\\)\\.." file)
-	      (setq file (match-string 1 file)))
-	  (setq proof-included-files-list (cons (cons module file)
-						proof-included-files-list))))))
-
-(defun proof-shell-filter (str) 
-  "The filter for the shell-process. We sleep until we get a
-  wakeup-char in the input, then run proof-shell-process-output, and
-  set proof-marker to keep track of how far we've got."
-  (if (string-match proof-shell-eager-annotation-end str)
-      (proof-shell-popup-eager-annotation))
-  (if (or
-       ;; Some proof systems can be hacked to have annotated prompts;
-       ;; for these we set proof-shell-wakeup-char to the annotation special.  
-       (and proof-shell-wakeup-char
-	   (string-match (char-to-string proof-shell-wakeup-char) str))
-       ;; Others rely on a standard top-level (e.g. SML) whose prompt can't
-       ;; be hacked.  For those we use the prompt regexp.
-       (string-match proof-shell-annotated-prompt-regexp str))
-      (if (null (marker-position proof-marker))
-	  ;; Set marker to first prompt in output buffer, and sleep again.
-	  (progn
-	    (goto-char (point-min))
-	    (re-search-forward proof-shell-annotated-prompt-regexp)
-	    ;; FIXME: da: why is this next line here?  to delete the 
-	    ;;        possibly several character prompt? why?
-	    ;;        TMS: Its purpose is to remove the wakeup
-	    ;;        character associated with the prompt. This
-	    ;;        should not be necessary anymore, because the wakeup
-	    ;;        character isn't displayed anyway; see
-	    ;;        `proof-dont-show-annotations'. Watch this space!
-	    (backward-delete-char 1)
-	    (set-marker proof-marker (point)))
-	;; We've matched against a second prompt in str now.  Search
-	;; the output buffer for the second prompt after the one previously
-	;; marked.
-	(let (string res cmd)	
-	  (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))	; da: assumed to be after a prompt?
-	  (backward-delete-char 1)	; da: WHY? nasty assumption.
-	  (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 ((span (span-at-before (proof-locked-end) 'type)))
-    (while (and span 
-		(not (eq (span-property span 'type) 'goalsave))
-		(or (eq (span-property span 'type) 'comment)
-		    (not (funcall proof-goal-command-p
-				       (span-property span 'cmd)))))
-      (setq span (prev-span span 'type)))
-    span)))
-    
-;; This needs some work to make it generic, since most of the code
-;; doesn't apply to Coq at all.
-(defun proof-steal-process ()
-  "This allows us to steal the process if we want to change the buffer
-   in which script management is running."
-  (proof-start-shell)
-  (if proof-shell-busy (error "Proof Process Busy!"))
-  (if (not (eq proof-buffer-type 'script))
-      (error "Must be running in a script buffer"))
-  (cond
-   ((eq proof-script-buffer (current-buffer))
-    nil)
-   (t
-    (let ((flist proof-included-files-list) 
-	  (file (expand-file-name (buffer-file-name))) span (cmd ""))
-      (if (string-match "\\(.*\\)\\.." file) (setq file (match-string 1 file)))
-      (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"))
-	(if (not (y-or-n-p "Reprocess this file? " )) (error "Aborted")))
-      (if (not (buffer-name proof-script-buffer))
-	  (message "Warning: Proof script buffer deleted: proof state may be inconsistent")
-	(save-excursion
-	  (set-buffer proof-script-buffer)
-	  (setq proof-active-buffer-fake-minor-mode nil)
-	  (setq span (proof-last-goal-or-goalsave))
-	  ;; This won't work for Coq if we have recursive goals in progress
-	  (if (and span (not (eq (span-property span 'type) 'goalsave)))
-	      (setq cmd proof-kill-goal-command))
-	  (proof-detach-segments)
-	  (delete-spans (point-min) (point-max) 'type)))
-
-      (setq proof-script-buffer (current-buffer))
-      (proof-init-segmentation)
-      (setq proof-active-buffer-fake-minor-mode t)
-
-      (cond 
-       (flist
-	(list nil (concat cmd "ForgetMark " (car (car flist)) ";")
-	      `(lambda (span) (setq proof-included-files-list 
-				    (quote ,(cdr flist))))))
-       ((not (string= cmd ""))
-	(list nil cmd 'proof-done-invisible))
-       (t nil))))))
-
-(defun proof-done-invisible (span) ())
-
-(defun proof-invisible-command (cmd &optional relaxed)
-  "Send cmd to the proof process without responding to the user."
-  (proof-check-process-available relaxed)
-  (if (not (string-match proof-re-end-of-cmd cmd))
-      (setq cmd (concat cmd proof-terminal-string)))
-  (proof-start-queue nil nil (list (list nil cmd
-  'proof-done-invisible)) relaxed))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;          User Commands                                           ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-	
-; Script management uses two major segments: Locked, which marks text
-; which has been sent to the proof assistant and cannot be altered
-; without being retracted, and Queue, which contains stuff being
-; queued for processing.  proof-action-list contains a list of
-; (span,command,action) triples. The loop looks like: Execute the
-; command, and if it's successful, do action on span.  If the
-; command's not successful, we bounce the rest of the queue and do
-; some error processing.
-;
-; when a span has been processed, we classify it as follows:
-; 'goalsave - denoting a 'goalsave pair in the locked region
-;    a 'goalsave region has a 'name property which is the name of the goal
-; 'comment - denoting a comment
-; 'pbp - denoting a span created by pbp
-; 'vanilla - denoting any other span.
-;   'pbp & 'vanilla spans have a property 'cmd, which says what
-;   command they contain. 
-
-; We don't allow commands while the queue has anything in it.  So we
-; do configuration by concatenating the config command on the front in
-; proof-send
-
-;;         proof-assert-until-point, and various gunk for its       ;;
-;;         setup and callback                                       ;;
-
-;; This code is for nested goals in Coq, and shouldn't affect things
-;; in LEGO.  It lifts "local" lemmas from inside goals out to top
-;; level.
-
-(defun proof-lift-global (glob-span)
-  (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)))))
-
-;; This is the actual callback for assert-until-point.
-
-(defun proof-done-advancing (span)
-  (let ((end (span-end span)) nam gspan next cmd)
-    (proof-set-locked-end end)
-    (proof-set-queue-start end)
-    (setq cmd (span-property span 'cmd))
-    (cond
-     ((eq (span-property span 'type) 'comment)
-      (set-span-property span 'mouse-face 'highlight))
-     ((string-match proof-save-command-regexp cmd)
-      ;; In coq, we have the invariant that if we've done a save and
-      ;; there's a top-level declaration then it must be the
-      ;; associated goal.  (Notice that because it's a callback it
-      ;; must have been approved by the theorem prover.)
-      (if (string-match proof-save-with-hole-regexp cmd)
-	  (setq nam (match-string 2 cmd)))
-      (setq gspan span)
-      (while (or (eq (span-property gspan 'type) 'comment)
-		 (not (funcall proof-goal-command-p 
-				    (setq cmd (span-property gspan 'cmd)))))
-	(setq next (prev-span gspan 'type))
-	(delete-span gspan)
-	(setq gspan next))
-
-      (if (null nam)
-	  (if (string-match proof-goal-with-hole-regexp
-			    (span-property gspan 'cmd))
-	      (setq nam (match-string 2 (span-property gspan 'cmd)))
-	    ;; This only works for Coq, but LEGO raises an error if
-	    ;; there's no name.
-	    ;; FIXME: a nonsense for Isabelle.
-	    (setq nam "Unnamed_thm")))
-
-      (set-span-end gspan end)
-      (set-span-property gspan 'mouse-face 'highlight)
-      (set-span-property gspan 'type 'goalsave)
-      (set-span-property gspan 'name nam)
-
-      (proof-lift-global gspan))
-     (t
-      (set-span-property span 'mouse-face 'highlight)
-      (if (funcall proof-global-p cmd)
-	  (proof-lift-global span))))))
-
-; depth marks number of nested comments. quote-parity is false if
-; we're inside ""'s.  Only one of (depth > 0) and (not quote-parity)
-; should be true at once. -- hhg
-
-(defun proof-segment-up-to (pos)
-  "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
-terminator. type is one of comment, or cmd. 'unclosed-comment may be
-consed onto the start if the segment finishes with an unclosed
-comment."
-  (save-excursion
-    (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)
-       (cond 
-	((and (= (point) pos) (> depth 0))
-	 (setq done t alist (cons 'unclosed-comment alist)))
-	((= (point) (point-max))
-	 (if (not quote-parity)
-	     (message "Warning: unclosed quote"))
-	 (setq done t))
-	((and (looking-at "\\*)") quote-parity)
-	 (if (= depth 0) 
-	     (progn (message "Warning: extraneous comment end") (setq done t))
-	   (setq depth (- depth 1)) (forward-char 2)
-	   (if (eq i 0) 
-	       (setq alist (cons (list 'comment "" (point)) alist))
-	     (aset str i ?\ ) (incf i))))
-	((and (looking-at "(\\*") quote-parity)
-	 (setq depth (+ depth 1)) (forward-char 2))
-	((> depth 0) (forward-char))
-	(t
-	 (setq c (char-after (point)))
-	 (if (or (> i 0) (not (= (char-syntax c) ?\ )))
-	     (progn (aset str i c) (incf i)))
-	 (if (looking-at "\"")
-	     (setq quote-parity (not quote-parity)))
-	 (forward-char)
-	 (if (and (= c proof-terminal-char) quote-parity)
-	     (progn 
-	       (setq alist 
-		     (cons (list 'cmd (substring str 0 i) (point)) alist))
-	       (if (>= (point) pos) (setq done t) (setq i 0)))))))
-     alist)))
-
-(defun proof-semis-to-vanillas (semis &optional callback-fn)
-  "Convert a sequence of semicolon positions (returned by the above
-function) to a set of vanilla extents."
-  (let ((ct (proof-locked-end)) span alist semi)
-    (while (not (null semis))
-      (setq semi (car semis)
-            span (make-span ct (nth 2 semi))
-	    ct (nth 2 semi))
-      (if (eq (car (car semis)) 'cmd)
-	  (progn
-	    (set-span-property span 'type 'vanilla)
-	    (set-span-property span 'cmd (nth 1 semi))
-	    (setq alist (cons (list span (nth 1 semi) 
-				    (or callback-fn 'proof-done-advancing))
-			      alist)))
-	(set-span-property span 'type 'comment)
-	(setq alist (cons (list span "COMMENT" 'proof-done-advancing) alist)))
-	(setq semis (cdr semis)))
-    (nreverse alist)))
-
-; Assert until point - We actually use this to implement the 
-; assert-until-point, active terminator keypress, and find-next-terminator. 
-; In different cases we want different things, but usually the information
-; (i.e. are we inside a comment) isn't available until we've actually run
-; proof-segment-up-to (point), hence all the different options when we've
-; done so.
-
-(defun proof-assert-until-point
-  (&optional unclosed-comment-fun ignore-proof-process-p)
-  "Process the region from the end of the locked-region until point.
-   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. If ignore-proof-process-p is set, no commands
-   will be added to the queue."
-  (interactive)
-  (let ((pt (point))
-	(crowbar (or ignore-proof-process-p (proof-steal-process)))
-	semis)
-    (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 ignore-proof-process-p) (not crowbar) (null semis))
-	  (error "Nothing to do!"))
-      (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-locked-end) (point) vanillas))))))
-
-;;         insert-pbp-command - an advancing command, for use when  ;;
-;;         PbpHyp or Pbp has executed in LEGO, and returned a       ;;
-;;         command for us to run                                    ;;
-
-(defun proof-insert-pbp-command (cmd)
-  (proof-check-process-available)
-  (let (span)
-    (proof-goto-end-of-locked)
-    (insert cmd)
-    (setq span (make-span (proof-locked-end) (point)))
-    (set-span-property span 'type 'pbp)
-    (set-span-property span 'cmd cmd)
-    (proof-start-queue (proof-locked-end) (point) 
-		       (list (list span cmd 'proof-done-advancing)))))
-
-
-;;         proof-retract-until-point and associated gunk            ;;
-;;         most of the hard work (i.e computing the commands to do  ;;
-;;         the retraction) is implemented in the customisation      ;;
-;;         module (lego.el or coq.el) which is why this looks so    ;;
-;;         straightforward                                          ;;
-
-
-(defun proof-done-retracting (span)
-  "Updates display after proof process has reset its state. See also
-the documentation for `proof-retract-until-point'. It optionally
-deletes the region corresponding to the proof sequence."
-  (let ((start (span-start span))
-        (end (span-end span))
-	(kill (span-property span 'delete-me)))
-    (proof-set-locked-end start)
-    (proof-set-queue-end start)
-    (delete-spans start end 'type)
-    (delete-span span)
-    (if kill (delete-region start end))))
-
-(defun proof-setup-retract-action (start end proof-command delete-region)
-  (let ((span (make-span start end)))
-    (set-span-property span 'delete-me delete-region)
-    (list (list span proof-command 'proof-done-retracting))))
-
-(defun proof-retract-target (target delete-region)
-  (let ((end (proof-locked-end))
-	(start (span-start target))
-	(span (proof-last-goal-or-goalsave))
-	actions)
-    
-    (if (and span (not (eq (span-property span 'type) 'goalsave)))
-	(if (< (span-end span) (span-end target))
-	    (progn
-	      (setq span target)
-	      (while (and span (eq (span-property span 'type) 'comment))
-		(setq span (next-span span 'type)))
-	      (setq actions (proof-setup-retract-action
-			     start end 
-			     (if (null span) "COMMENT"
-			       (funcall proof-count-undos-fn span))
-			     delete-region)
-		    end start))
-	  
-	  (setq actions (proof-setup-retract-action (span-start span) end
-						    proof-kill-goal-command
-						    delete-region)
-		end (span-start span))))
-    
-    (if (> end start) 
-	(setq actions
-	      (nconc actions (proof-setup-retract-action 
-			      start end
-			      (funcall proof-find-and-forget-fn target)
-			      delete-region))))
-      
-    (proof-start-queue (min start end) (proof-locked-end) actions)))
-
-(defun proof-retract-until-point (&optional delete-region)
-  "Sets up the proof process for retracting until point. In
-   particular, it sets a flag for the filter process to call
-   `proof-done-retracting' after the proof process has actually
-   successfully reset its state. It optionally deletes the region in
-   the proof script corresponding to the proof command sequence. If
-   this function is invoked outside a locked region, the last
-   successfully processed command is undone."
-  (interactive)
-  (proof-check-process-available)
-  (let ((span (span-at (point) 'type)))
-    (if (null (proof-locked-end)) (error "No locked region"))
-    (and (null span)
-	 (progn (proof-goto-end-of-locked) (backward-char)
-		(setq span (span-at (point) 'type))))
-    (proof-retract-target span delete-region)))
-
-;;         proof-try-command                                        ;;
-;;         this isn't really in the spirit of script management,    ;;
-;;         but sometimes the user wants to just try an expression   ;;
-;;         without having to undo it in order to try something      ;;
-;;         different. Of course you can easily lose sync by doing   ;;
-;;         something here which changes the proof state             ;;
-
-(defun proof-done-trying (span)
-  (delete-span span)
-  (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 satisfies 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)))))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;         misc other user functions                                ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-
-(defun proof-undo-last-successful-command ()
-  "Undo last successful command, both in the buffer recording the
-   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-locked-end) 'type)))
-  (proof-retract-until-point t))
-
-(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'."
-  (interactive)
-  (let ((cmd (span-at (point) 'type)))
-    (if cmd (goto-char (span-end cmd))
-      (and (re-search-forward "\\S-" nil t)
-	   (proof-assert-until-point nil 'ignore-proof-process)))))
-
-(defun proof-process-buffer ()
-  "Process the current buffer and set point at the end of the buffer."
-  (interactive)
-  (end-of-buffer)
-  (proof-assert-until-point))
-
-;; For when things go horribly wrong
-
-(defun proof-restart-script ()
-  (interactive)
-  (save-excursion
-    (if (buffer-live-p proof-script-buffer)
-	(progn
-	  (set-buffer proof-script-buffer)
-	  (setq proof-active-buffer-fake-minor-mode nil)
-	  (delete-spans (point-min) (point-max) 'type)
-	  (proof-detach-segments)))
-    (setq proof-shell-busy nil
-	  proof-script-buffer nil)
-    (if (buffer-live-p proof-shell-buffer) 
-	(kill-buffer proof-shell-buffer))
-    (if (buffer-live-p proof-pbp-buffer)
-	(kill-buffer proof-pbp-buffer))))
-
-;; A command for making things go horribly wrong - it moves the
-;; end-of-locked-region marker backwards, so user had better move it
-;; correctly to sync with the proof state, or things will go all
-;; pear-shaped.
-
-(defun proof-frob-locked-end ()
-  (interactive)
-  "Move the end of the locked region backwards. 
-   Only for use by consenting adults."
-  (cond
-   ((not (eq proof-script-buffer (current-buffer)))
-    (error "Not in proof buffer"))
-   ((> (point) (proof-locked-end))
-    (error "Can only move backwards"))
-   (t (proof-set-locked-end (point))
-      (delete-spans (proof-locked-end) (point-max) 'type))))
-
-(defvar proof-minibuffer-history nil
-  "The last command read from the minibuffer")
-
-(defun proof-execute-minibuffer-cmd ()
-  (interactive)
-  (let (cmd)
-    (proof-check-process-available 'relaxed)
-    (setq cmd (read-string "Command: " nil 'proof-minibuffer-history))
-    (proof-invisible-command cmd 'relaxed)))
-	  
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;; Popup and Pulldown Menu ;;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;;; Menu commands for the underlying proof assistant
-(defvar proof-ctxt-string ""
-  "Command to display context in proof assistant")
-
-(defvar proof-help-string ""
-  "Command to ask for help in proof assistant")
-
-(defvar proof-prf-string ""
-  "Command to display proof state in proof assistant")
-
-(defun proof-ctxt ()
-  "List context."
-  (interactive) 
-  (proof-invisible-command (concat proof-ctxt-string proof-terminal-string)))
-
-(defun proof-help ()
-  "Print help message giving syntax."
-  (interactive)
-  (proof-invisible-command (concat proof-help-string proof-terminal-string)))
-
-(defun proof-prf ()
-  "List proof state."
-  (interactive)
-  (proof-invisible-command (concat proof-prf-string proof-terminal-string)))
-
-;;; To be called from menu
-(defun proof-info-mode ()
-  "Info mode on proof mode."
-  (interactive)
-  (info "script-management"))
-
-(defun proof-exit ()
-  "Exit Proof-assistant."
-  (interactive)
-  (proof-restart-script))
-
-(defvar proof-help-menu
-  '("Help"
-	     ["Proof assistant web page"
-	      (w3-fetch proof-www-home-page) t]
-	     ["Help on Emacs proof-mode" proof-info-mode t]
-	     )
-  "The Help Menu in Script Management.")
-
-(defvar proof-shared-menu
-  (append-element '(
-            ["Display context" proof-ctxt
-	      :active (proof-shell-live-buffer)]
-            ["Display proof state" proof-prf
-	      :active (proof-shell-live-buffer)]
-	    ["Exit proof assistant" proof-exit
-	      :active (proof-shell-live-buffer)]
-	    "----"
-	    ["Find definition/declaration" find-tag-other-window t]
-	    )
-	  proof-help-menu))
-
-(defvar proof-menu  
-  (append '("Commands"
-            ["Toggle active terminator" proof-active-terminator-minor-mode
-	     :active t
-	     :style toggle
-             :selected proof-active-terminator-minor-mode]
-            "----")
-          (list (if (string-match "XEmacs 19.1[2-9]" emacs-version)
-		    "--:doubleLine" "----"))
-          proof-shared-menu
-          )
-  "*The menu for the proof assistant.")
-
-(defvar proof-shell-menu proof-shared-menu
-  "The menu for the Proof-assistant shell")
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;          Active terminator minor mode                            ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(deflocal proof-active-terminator-minor-mode nil 
-  "active terminator minor mode flag")
-
-(defun proof-active-terminator-minor-mode (&optional arg)
-  "Toggle PROOF's Active Terminator minor mode.
-With arg, turn on the Active Terminator minor mode if and only if arg
-is positive.
-
-If Active terminator mode is enabled, a terminator will process the
-current command."
-
- (interactive "P")
- 
-;; has this minor mode been registered as such?
-  (or (assq 'proof-active-terminator-minor-mode minor-mode-alist)
-      (setq minor-mode-alist
-            (append minor-mode-alist
-                    (list '(proof-active-terminator-minor-mode
-			    (concat " " proof-terminal-string))))))
-
-  (setq proof-active-terminator-minor-mode
-        (if (null arg) (not proof-active-terminator-minor-mode)
-          (> (prefix-numeric-value arg) 0)))
-  (if (fboundp 'redraw-modeline)
-      (redraw-modeline)
-    (force-mode-line-update)))
-
-(defun proof-process-active-terminator ()
-  "Insert the terminator in an intelligent way and assert until the
-  new terminator.  Fire up proof process if necessary."
-  (let ((mrk (point)) ins)
-    (if (looking-at "\\s-\\|\\'\\|\\w") 
-	(if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t))
-	    (error "Nothing to do!")))
-    (if (not (= (char-after (point)) proof-terminal-char))
-	(progn (forward-char) (insert proof-terminal-string) (setq ins t)))
-    (proof-assert-until-point
-     (function (lambda ()
-		 (if ins (backward-delete-char 1))
-		 (goto-char mrk) (insert proof-terminal-string))))))
-
-(defun proof-active-terminator ()
-  (interactive)
-  (if proof-active-terminator-minor-mode 
-      (proof-process-active-terminator)
-    (self-insert-command 1)))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Proof mode configuration                                         ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-
-(define-derived-mode proof-mode fundamental-mode 
-  proof-mode-name "Proof mode - not standalone"
-  ;; define-derived-mode proof-mode initialises proof-mode-map
-  (setq proof-buffer-type 'script))
-
-;; This has to come after proof-mode is defined
-
-(define-derived-mode proof-shell-mode comint-mode 
-  "proof-shell" "Proof shell mode - not standalone"
-  (setq proof-buffer-type 'shell)
-  (setq proof-shell-busy nil)
-  (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)
-  (setq comint-get-old-input (function (lambda () "")))
-  (proof-dont-show-annotations)
-  (setq proof-marker (make-marker)))
-
-(easy-menu-define proof-shell-menu
-		  proof-shell-mode-map
-		  "Menu used in the proof assistant shell."
-		  (cons proof-mode-name (cdr proof-shell-menu)))
-
-(easy-menu-define proof-mode-menu  
-		  proof-mode-map
-		  "Menu used in proof mode."
-		  (cons proof-mode-name (cdr proof-menu)))
-
-;; the following callback is an irritating hack - there should be some
-;; elegant mechanism for computing constants after the child has
-;; configured.
-
-(defun proof-config-done () 
-
-;; calculate some strings and regexps for searching
-
-  (setq proof-terminal-string (char-to-string proof-terminal-char))
-
-  (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string))
-  (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string))
-
-  (make-local-variable 'comment-start)
-  (setq comment-start (concat proof-comment-start " "))
-  (make-local-variable 'comment-end)
-  (setq comment-end (concat " " proof-comment-end))
-  (make-local-variable 'comment-start-skip)
-  (setq comment-start-skip 
-    (concat (regexp-quote proof-comment-start) "+\\s_?"))
-
-  (setq proof-re-end-of-cmd (concat "\\s_*" proof-terminal-string "\\s_*\\\'"))
-  (setq proof-re-term-or-comment 
-	(concat proof-terminal-string "\\|" (regexp-quote proof-comment-start)
-		"\\|" (regexp-quote proof-comment-end)))
-
-;; func-menu --- Jump to a goal within a buffer
-  (and (boundp 'fume-function-name-regexp-alist)
-       (defvar fume-function-name-regexp-proof
-	 (cons proof-goal-with-hole-regexp 2))
-       (push (cons major-mode 'fume-function-name-regexp-proof)
-	     fume-function-name-regexp-alist))
-  (and (boundp 'fume-find-function-name-method-alist)
-       (push (cons major-mode 'fume-match-find-next-function-name)
-	     fume-find-function-name-method-alist))
-
-;; Info
-  (or (memq proof-info-dir Info-default-directory-list)
-      (setq Info-default-directory-list
-	    (cons proof-info-dir Info-default-directory-list)))
-
-;; keymaps and menus
-  (easy-menu-add proof-mode-menu proof-mode-map)
-
-  (proof-define-keys proof-mode-map proof-universal-keys)
-
-  (define-key proof-mode-map
-    (vconcat [(control c)] (vector proof-terminal-char))
-    'proof-active-terminator-minor-mode)
-
-  (define-key proof-mode-map [(control c) (control e)]
-    'proof-find-next-terminator)
-
-  (define-key proof-mode-map (vector proof-terminal-char)
-    'proof-active-terminator)
-  (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-interactive)
-  (define-key proof-mode-map [(control button1)] 'proof-send-span)
-  (define-key proof-mode-map [(control c) (control b)] 'proof-process-buffer)
-  (define-key proof-mode-map [(control c) (control z)] 'proof-frob-locked-end)
-
-  (define-key proof-mode-map [tab]      'proof-indent-line)
-  (make-local-variable 'indent-line-function)
-  (setq indent-line-function 'proof-indent-line)
-
-  (define-key (current-local-map) [(control c) (control p)] 'proof-prf)
-  (define-key (current-local-map) [(control c) ?c] 'proof-ctxt)
-  (define-key (current-local-map) [(control c) ?h] 'proof-help)
-
-;; For fontlock
-  (remove-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer t)
-  (add-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer nil t)
-  (remove-hook 'font-lock-mode-hook 'proof-unfontify-separator t)
-  (add-hook 'font-lock-mode-hook 'proof-unfontify-separator nil t)
-
-;; if we don't have the following, zap-commas fails to work.
-
-  (and (boundp 'font-lock-always-fontify-immediately)
-       (setq font-lock-always-fontify-immediately t))
-
-  (run-hooks 'proof-mode-hook))
-
-(defun proof-shell-config-done ()
-  (accept-process-output (get-buffer-process (current-buffer)))
-
-  ;; If the proof process in invoked on a different machine e.g.,
-  ;; for proof-prog-name="rsh fastmachine proofprocess", one needs
-  ;; to adjust the directory:
-  (and proof-shell-cd
-       (proof-shell-insert (format proof-shell-cd
-       ;; under Emacs 19.34 default-directory contains "~" which causes
-       ;; problems with LEGO's internal Cd command
-				   (expand-file-name default-directory))))
-
-  (if proof-shell-init-cmd
-       (proof-shell-insert proof-shell-init-cmd))
-
-;; Note that proof-marker actually gets set in proof-shell-filter.
-;; This is manifestly a hack, but finding somewhere more convenient
-;; to do the setup is tricky.
-
-  (while (null (marker-position proof-marker))
-    (if (accept-process-output (get-buffer-process (current-buffer)) 15)
-	()
-      (error "Failed to initialise proof process"))))
-
-(define-derived-mode pbp-mode fundamental-mode 
-  proof-mode-name "Proof by Pointing"
-  ;; defined-derived-mode pbp-mode initialises pbp-mode-map
-  (setq proof-buffer-type 'pbp)
-  (suppress-keymap pbp-mode-map 'all)
-;  (define-key pbp-mode-map [(button2)] 'pbp-button-action)
-  (proof-define-keys pbp-mode-map proof-universal-keys)
-  (erase-buffer))
-
-
-(provide 'proof)