Split proof.el into proof-config.el, proof-script.el, proof-shell.el

4 files changed, 2905 insertions, 2801 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
new file mode 100644
index 00000000..f5fb761d
--- /dev/null
+++ b/generic/proof-config.el
@@ -0,0 +1,483 @@
+;; proof-config.el  Proof General configuration for proof assistant.
+;;
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
+;;          Thomas Kleymann and Dilip Sequeira
+;;
+;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;;
+;; $Id$
+;;
+;; 
+;; This file declares all prover-specific configuration variables.
+;; These are used variously by the proof script mode and the proof
+;; shell mode.
+;; 
+;; To customize Proof General for a new proof assistant, you
+;; should read this file carefully! 
+;;
+;;  0. Major modes
+;;  1. Menus, user-level commands.
+;;  2. Script mode configuration 
+;;  3. Shell mode configuration
+;;     3a. commands
+;;     3b. regexps
+;;     3c. hooks
+;;
+
+
+(defgroup prover-config nil
+  "Configuration of Proof General for the prover in use."
+  :group 'proof-internal)
+
+;; The variables in the "prover-config" (NB: not "proof config"!!)
+;; customize group are those which are intended to be set by the
+;; prover specific elisp, i.e. constants set on a per-prover basis.
+
+;; Putting these in a customize group is useful for documenting
+;; this type of variable, and for developing a new instantiation
+;; of Proof General.
+;; But it is *not* useful for final user-level customization!
+;; The reason is that saving these customizations across a session is
+;; not liable to work, because the prover specific elisp usually
+;; overrides with a series of setq's in <assistant>-mode-config type
+;; functions.  This is why prover-config appears under the
+;; proof-internal group.
+
+;; Note: The XEmacs customization menus would be nicer if the
+;; variables in prover-config group were uniformly renamed
+;; prover-config-* (and similarly for other variables/groups).  
+;; But it's somewhat of a horror in the code!
+
+
+(defcustom proof-assistant ""
+  "Name of the proof assistant Proof General is using.
+This is set automatically by the mode stub defined in proof-site,
+from the name given in proof-internal-assistant-table."
+  :type 'string
+  :group 'prover-config)
+
+
+
+
+;;
+;; 0. The major modes used by Proof General.
+;;
+
+(defcustom proof-mode-for-shell nil
+  "Mode for proof shell buffers.
+Suggestion: this can be set in proof-pre-shell-start-hook."
+  :type 'function
+  :group 'prover-config)
+
+(defcustom proof-mode-for-pbp nil
+  "Mode for proof state display buffers.
+Suggestion: this can be set in proof-pre-shell-start-hook."
+  :type 'function
+  :group 'prover-config)
+
+(defcustom proof-mode-for-script nil
+  "Major mode for proof script buffers."
+  :type 'function
+  :group 'prover-config)
+
+
+
+
+
+;;
+;; 1. Configuration for menus, user-level commands, etc.
+;;
+
+(defcustom proof-www-home-page ""
+  "Web address for information on proof assistant"
+  :type 'string
+  :group 'prover-config)
+
+(defcustom proof-ctxt-string ""
+  "*Command to display the context in proof assistant."
+  :type 'string
+  :group 'proof)
+
+(defcustom proof-help-string ""
+  "*Command to ask for help in proof assistant."
+  :type 'string
+  :group 'proof)
+
+(defcustom proof-prf-string ""
+  "Command to display proof state in proof assistant."
+  :type 'string
+  :group 'prover-)
+
+(defcustom proof-goal-command nil
+  "Command to set a goal in the proof assistant.  String or fn.
+If a string, the format character %s will be replaced by the
+goal string. If a function, should return a command string to
+insert when called interactively."
+  :type '(choice string function)
+  :group 'prover-config)
+
+(defcustom proof-save-command nil
+  "Command to save a proved theorem in the proof assistant.  String or fn.
+If a string, the format character %s will be replaced by the
+theorem name. If a function, should return a command string to
+insert when called interactively."
+  :type '(choice string function)
+  :group 'prover-config)
+
+
+;; FIXME: allow this to be set in the mode fn instead.
+(defcustom proof-tags-support t
+  "If non-nil, include tags functions in menus.
+This variable should be set before requiring proof.el"
+  :type 'boolean
+  :group 'prover-config)
+
+
+
+;;
+;; 2. Configuration for proof script mode
+;;
+
+;;
+;; The following variables should be set before proof-config-done
+;; is called.  These configure the mode for the script buffer,
+;; including highlighting, etc.
+;;
+
+(defgroup proof-script nil
+  "Proof General configuration of scripting buffer mode."
+  :group 'prover-config)
+
+
+(defcustom proof-terminal-char nil
+  "Character which terminates a proof command in a script buffer."
+  :type 'character
+  :group 'proof-script)
+
+(defcustom proof-comment-start ""
+  "String which starts a comment in the proof assistant command language.
+The script buffer's comment-start is set to this string plus a space."
+  :type 'string
+  :group 'proof-script)
+
+(defcustom proof-comment-end ""
+  "String which starts a comment in the proof assistant command language.
+The script buffer's comment-end is set to this string plus a space."
+  :type 'string
+  :group 'proof-script)
+
+(defcustom proof-save-command-regexp nil 
+  "Matches a save command"
+  :type 'regexp
+  :group 'prover-config)
+
+(defcustom proof-save-with-hole-regexp nil 
+  "Matches a named save command"
+  :type 'regexp
+  :group 'proof-script)
+
+(defcustom proof-goal-with-hole-regexp nil 
+  "Matches a saved goal command"
+  :type 'regexp
+  :group 'proof-script)
+
+(defcustom proof-goal-command-p nil 
+  "Is this a goal"
+  :type 'function
+  :group 'proof-script)
+
+(defcustom proof-lift-global nil
+  "This function lifts local lemmas from inside goals out to top level.
+This function takes the local goalsave span as an argument. Set this
+to `nil' of the proof assistant does not support nested goals."
+  :type '(choice nil function)
+  :group 'proof-script)
+
+(defcustom proof-count-undos-fn nil 
+  "Compute number of undos in a target segment"
+  :type 'function
+  :group 'proof-script)
+
+(defcustom proof-atomic-sequence-lists nil
+  "list of instructions for setting up atomic sequences of commands (ACS).
+
+Each instruction is
+a list of the form `(END START &optional FORGET-COMMAND)'. END is a
+regular expression to recognise the last command in an ACS. START
+is a function. Its input is the last command of an ACS. Its output
+is a regular exression to recognise the first command of the ACS.
+It is evaluated once and the output is successively matched agains
+previously processed commands until a match occurs (or the
+beginning of the current buffer is reached). The region determined
+by (START,END) is locked as an ACS. Optionally, the ACS is
+annotated with the actual command to retract the ACS. This is
+computed by applying FORGET-COMMAND to the first and last command
+of the ACS."
+  :type '(repeat (cons regexp function (choice (const nil) function)))
+  :group 'proof-shell)
+
+
+(defconst proof-no-command "COMMENT"
+  "String used as a nullary action (send no command to the proof assistant).
+Only relevant for proof-find-and-forget-fn.")
+
+(defcustom proof-find-and-forget-fn nil
+  "Function returning a command string to forget back to before its argument span.
+The special string proof-no-command means there is nothing to do."
+  :type 'function
+  :group 'proof-script)
+
+(defcustom 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"
+  :type 'function
+  :group 'proof-script)
+
+(defcustom proof-kill-goal-command ""
+  "Command to kill a goal."
+  :type 'string
+  :group 'proof-script)
+
+(defcustom proof-global-p nil
+  "Whether a command is a global declaration.  Predicate on strings or nil.
+This is used to handle nested goals allowed by some provers."
+  :type 'function
+  :group 'proof-script)
+
+(defcustom proof-state-preserving-p nil
+  "A predicate, non-nil if its argument preserves the proof state."
+  :type 'function
+  :group 'proof-script)
+
+(defcustom pbp-change-goal nil
+  "Command to change to the goal %s"
+  :type 'string
+  :group 'prover-config)
+
+(defcustom proof-shell-process-output-system-specific nil
+  "Set this variable to handle system specific output.
+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 pair 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."
+  :type '(cons (function function))
+  :group 'prover-config)
+
+(defcustom proof-activate-scripting-hook nil
+  "Hook run when a buffer is switched into scripting mode.
+The current buffer will be the newly active scripting buffer.
+
+This hook may be useful for synchronizing with the proof
+assistant, for example, to switch to a new theory."
+  :type '(repeat function)
+  :group 'prover-config)
+
+
+
+
+
+;;
+;;  3. Configuration for proof shell	                            
+;;
+;; The variables in this section concern the proof shell mode.
+;; The first group of variables are hooks invoked at various points.
+;; The second group of variables are concerned with matching the output
+;; from the proof assistant.
+;;
+;; Variables here are put into the customize group 'proof-shell'.
+;;
+;; These should be set in the shell mode configuration, again,
+;; before proof-shell-config-done is called.
+;;
+
+(defgroup proof-shell nil
+  "Settings for output from the proof assistant in the proof shell."
+  :group 'prover-config)
+
+
+;; 
+;; 3a. commands
+;;
+
+(defcustom proof-prog-name nil
+  "System command to run program name in proof shell.
+Suggestion: this can be set in proof-pre-shell-start-hook."
+  :type 'string
+  :group 'proof-shell)
+
+(defcustom proof-shell-init-cmd ""
+   "The command for initially configuring the proof process."
+   :type '(choice string (const nil))
+   :group 'proof-shell)
+
+(defcustom proof-shell-cd nil
+  "Command to the proof assistant to change the working directory."
+  :type 'string
+  :group 'proof-shell)
+
+
+;;
+;; 3b. Regexp variables for matching output from proof process.
+;;
+
+(defcustom proof-shell-prompt-pattern nil 
+   "Proof shell's value for comint-prompt-pattern, which see."
+   :type 'regexp
+   :group 'proof-shell)
+
+;; FIXME da: replace this with wakeup-regexp or prompt-regexp?
+;; May not need next variable.
+(defcustom proof-shell-wakeup-char nil
+  "A special character which terminates an annotated prompt.
+Set to nil if proof assistant does not support annotated prompts."
+  :type '(choice character (const nil))
+  :group 'proof-shell)
+
+(defcustom proof-shell-annotated-prompt-regexp ""
+  "Regexp matching a (possibly annotated) prompt pattern.
+Output is grabbed between pairs of lines matching this regexp.
+To help matching you may be able to annotate the proof assistant
+prompt with a special character not appearing in ordinary output.
+The special character should appear in this regexp, should
+be the value of proof-shell-wakeup-char."
+  :type 'regexp
+  :group 'proof-shell)
+
+(defcustom proof-shell-abort-goal-regexp nil
+  "Regexp matching output from an aborted proof."
+  :type 'regexp
+  :group 'proof-shell)
+
+(defcustom proof-shell-error-regexp nil
+  "Regexp matching an error report from the proof assistant.
+We assume that an error message corresponds to a failure
+in the last proof command executed.  (So don't match
+mere warning messages with this regexp)."
+  :type 'regexp
+  :group 'proof-shell) 
+
+(defcustom proof-shell-interrupt-regexp nil
+  "Regexp matching output indicating the assistant was interrupted."
+  :type 'regexp
+  :group 'proof-shell) 
+
+(defcustom proof-shell-proof-completed-regexp nil
+  "Regexp matching output indicating a finished proof."
+  :type 'regexp
+  :group 'proof-shell)
+
+(defcustom proof-shell-result-start ""
+  "Regexp matching start of an output from the prover after pbp commands.
+In particular, after a `pbp-goal-command' or a `pbp-hyp-command'."
+  :type 'regexp
+  :group 'proof-shell)
+
+(defcustom proof-shell-result-end ""
+  "Regexp matching end of output from the prover after pbp commands.
+In particular, after a `pbp-goal-command' or a `pbp-hyp-command'."
+  :type 'regexp
+  :group 'proof-shell)
+
+(defcustom proof-shell-start-goals-regexp ""
+  "Regexp matching the start of the proof state output."
+  :type 'regexp
+  :group 'proof-shell)
+
+(defcustom proof-shell-end-goals-regexp ""
+  "Regexp matching the end of the proof state output."
+  :type 'regexp
+  :group 'proof-shell)
+
+(defcustom pbp-error-regexp nil
+  "Regexp indicating that the proof process has identified an error."
+  :type 'regexp
+  :group 'proof-shell)
+
+;;
+;; 3c. hooks 
+;;
+
+(defcustom proof-shell-insert-hook nil 
+  "Hooks run by proof-shell-insert before inserting a command.
+Can be used to configure the proof assistant to the interface in
+various ways (for example, setting the line width of output).
+Any text inserted by these hooks will be sent to the proof process
+before every command issued by Proof General."
+  :type '(repeat function)
+  :group 'proof-shell)
+
+(defcustom proof-pre-shell-start-hook nil
+  "Hooks run before proof shell is started.
+Usually this is set to a function which configures the proof shell
+variables."
+  :type '(repeat function)
+  :group 'proof-shell)
+
+(defcustom proof-shell-handle-delayed-output-hook
+  '(proof-pbp-focus-on-first-goal)
+  "Hooks run after new output has been displayed in the RESPONSE buffer."
+  :type '(repeat function)
+  :group 'proof-shell)
+
+(defcustom proof-shell-handle-error-hook
+  '(proof-goto-end-of-locked-if-pos-not-visible-in-window)
+  "Hooks run after an error has been reported in the RESPONSE buffer."
+  :type '(repeat function)
+  :group 'proof-shell)
+
+(defcustom proof-shell-process-file nil
+  "A tuple of the form (regexp . function) to match a processed file name.
+
+If REGEXP matches output, then the function FUNCTION is invoked on the
+output string chunk. It must return a script file name (with complete
+path) the system is currently processing. In practice, FUNCTION is
+likely to inspect the match data.  If it returns the empty string,
+the file name of the scripting buffer is used instead.  If it
+returns nil, no action is taken.
+
+Care has to be taken in case the prover only reports on compiled
+versions of files it is processing. In this case, FUNCTION needs to
+reconstruct the corresponding script file name. The new (true) file
+name is added to the front of `proof-included-files-list'."
+  :type '(choice (cons regexp function) (const nil))
+  :group 'proof-shell)
+
+(defcustom proof-shell-retract-files-regexp nil
+  "A REGEXP to match that the prover has retracted across file boundaries.
+
+At this stage, Proof General's view of the processed files is out of
+date and needs to be updated with the help of the function
+`proof-shell-compute-new-files-list'."
+  :type '(choice regexp (const nil))
+  :group 'proof-shell)
+
+(defcustom proof-shell-compute-new-files-list nil
+  "Function to update `proof-included-files list'.
+
+It needs to return an up to date list of all processed files. Its
+output is stored in `proof-included-files-list'. Its input is the
+string of which `proof-shell-retract-files-regexp' matched a
+substring. In practice, this function is likely to inspect the
+previous (global) variable `proof-included-files-list' and the match
+data triggered by `proof-shell-retract-files-regexp'."
+  :type '(choice function (const nil))
+  :group 'proof-shell)
+
+
+
+
+
+;; End of proof-config.el
+(provide 'proof-config)
diff --git a/generic/proof-script.el b/generic/proof-script.el
new file mode 100644
index 00000000..453b18db
--- /dev/null
+++ b/generic/proof-script.el
@@ -0,0 +1,1423 @@
+;; proof-script.el  Major mode for proof assistant script files.
+;;
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
+;;          Thomas Kleymann and Dilip Sequeira
+;;
+;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;;
+;; $Id$
+;;
+
+;;
+;;  Internal variables used by script mode
+;;
+
+;; FIXME da: remove proof-terminal-string.  At the moment some
+;; commands need to have the terminal string, some don't.
+;; We should assume commands are terminated properly at the
+;; specific level.
+(defvar proof-terminal-string nil 
+  "End-of-line string for proof process.")
+
+(defvar proof-re-end-of-cmd nil 
+  "Regexp matching end of command.  Based on proof-terminal-string.
+Set in proof-config-done.")
+
+(defvar proof-re-term-or-comment nil 
+  "Regexp matching terminator, comment start, or comment end.
+Set in proof-config-done.")
+
+(defvar proof-marker nil 
+  "Marker in proof shell buffer pointing to previous command input.")
+
+(defvar proof-shell-buffer nil
+  "Process buffer where the proof assistant is run.")
+
+(defvar proof-script-buffer-list nil
+  "Scripting buffers with locked regions.
+The first element is current and in scripting minor mode.
+The cdr of the list of corresponding file names is a subset of
+`proof-included-files-list'.")
+
+(defvar proof-pbp-buffer nil
+  "The goals buffer (also known as the pbp buffer).")
+
+(defvar proof-response-buffer nil
+  "The response buffer.")
+
+(defvar proof-shell-busy nil 
+  "A lock indicating that the proof shell is processing.
+When this is non-nil, proof-check-process-available will give
+an error.")
+
+(deflocal proof-buffer-type nil 
+  "Symbol indicating the type of this buffer: 'script, 'shell, or 'pbp.")
+
+(defvar proof-action-list nil "action list")
+
+(defvar proof-included-files-list nil 
+  "List of files currently included in proof process.
+Whenever a new file is being processed, it gets added to the front of
+the list. When the prover retracts across file boundaries, this list
+is resynchronised. It contains files in canonical truename format")
+
+(deflocal proof-active-buffer-fake-minor-mode nil
+  "An indication in the modeline that this is the *active* script buffer")
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; A few small utilities					    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun proof-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. Moves point after the match.
+
+The package fume-func provides the function
+`fume-match-find-next-function-name' with the same specification.
+However, fume-func's version is incorrec"
+  ;; DO NOT USE save-excursion; we need to move point!
+  ;; save-excursion is called at a higher level in the func-menu
+  ;; package 
+    (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-message (str)
+  "Output STR in minibuffer."
+  (message (concat "[" proof-assistant "] " str)))
+
+;; append-element in tl-list
+(defun proof-append-element (ls elt)
+  "Append ELT to last of LS if ELT is not nil. [proof.el]
+This function coincides with `append-element' in the package
+[tl-list.el.]"
+  (if elt
+      (append ls (list elt))
+    ls))
+
+(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) 
+  "Return the list of words in S separated by SEPARATOR."
+  (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)))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Basic code for the locked region and the queue region            ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; FIXME: da: doc below needs fixing.
+(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)
+
+(defface proof-queue-face
+  '((((type x) (class color) (background light))
+     (:background "mistyrose"))
+    (((type x) (class color) (background dark))
+     (:background "mediumvioletred"))
+    (t				
+     (:foreground "white" :background "black")))
+  "Face for commands in proof script waiting to be processed."
+  :group 'proof)
+
+(defface proof-locked-face
+  '((((type x) (class color) (background light))   
+     (:background "lavender"))
+    (((type x) (class color) (background dark))   
+     (:background "navy"))
+    (t				
+     (:underline t)))
+  "Face for locked region of proof script (processed commands)."
+  :group 'proof)
+
+(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)
+
+  (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)
+
+  (set-span-property proof-locked-span 'face 'proof-locked-face)
+
+  (detach-span proof-locked-span))
+
+(defsubst proof-lock-unlocked ()
+  "Make the locked region read only."
+  (span-read-only proof-locked-span))
+
+(defsubst proof-unlock-locked ()
+  "Make the locked region read-write."
+  (span-read-write proof-locked-span))
+
+(defsubst proof-set-queue-endpoints (start end)
+  "Set the queue span to be START, END."
+  (set-span-endpoints proof-queue-span start end))
+
+(defsubst proof-set-locked-endpoints (start end)
+  "Set the locked span to be START, END."
+  (set-span-endpoints proof-locked-span start end))
+
+(defsubst proof-detach-queue ()
+  "Remove the span for the queue region."
+  (and proof-queue-span (detach-span proof-queue-span)))
+
+(defsubst proof-detach-locked ()
+  "Remove the span for the locked region."
+  (and proof-locked-span (detach-span proof-locked-span)))
+
+(defsubst proof-set-queue-start (start)
+  "Set the queue span to begin at START."
+  (set-span-start proof-queue-span start))
+
+(defsubst proof-set-queue-end (end)
+  "Set the queue span to end at END."
+  (set-span-end proof-queue-span end))
+
+(defun proof-detach-segments (&optional buffer)
+  "Remove locked and queue region from BUFFER.
+Defaults to current buffer when BUFFER is nil."
+  (let ((buffer (or buffer (current-buffer))))
+    (save-excursion
+      (proof-detach-queue)
+      (proof-detach-locked))))
+
+(defsubst proof-set-locked-end (end)
+  "Set the end of the locked region to be END, sort of? FIXME.
+If END is past the end of the buffer, remove the locked region.
+Otherwise set the locked region to be from the start of the
+buffer to END."
+  (if (>= (point-min) end)
+      (proof-detach-locked)
+    (set-span-endpoints proof-locked-span (point-min) end)))
+
+(defun proof-unprocessed-begin ()
+  "Return end of locked region in current buffer or (point-min) otherwise."
+  (or 
+   (and (member (current-buffer) proof-script-buffer-list)
+	proof-locked-span (span-end proof-locked-span))
+   (point-min)))
+
+(defun proof-locked-end ()
+  "Return end of the locked region of the current buffer.
+Only call this from a scripting buffer."
+  (if (member (current-buffer) proof-script-buffer-list)
+      (proof-unprocessed-begin)
+    (error "bug: proof-locked-end called from wrong buffer")))
+
+(defsubst proof-end-of-queue ()
+  "Return the end of the queue region, or nil if none."
+  (and proof-queue-span (span-end proof-queue-span)))
+
+(defun proof-dont-show-annotations ()
+  "Set display values of annotations (characters 128-255) to be invisible."
+  (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)))))
+
+(defun proof-mark-buffer-atomic (buffer)
+  "Mark BUFFER as having been processed in a single step.
+
+If buffer already contains a locked region, only the remainder of the
+buffer is closed off atomically." 
+  (save-excursion
+    (set-buffer buffer)
+    (let ((span (make-span (proof-unprocessed-begin) (point-max)))
+	  cmd)
+      ;; compute first command of buffer
+      (goto-char (point-min))
+      (proof-find-next-terminator)
+      (let ((cmd-list (member-if
+		       (lambda (entry) (equal (car entry) 'cmd))
+		       (proof-segment-up-to (point)))))
+	(proof-init-segmentation)
+	(if cmd-list 
+	    (progn
+	      (setq cmd (second (car cmd-list)))
+	      (set-span-property span 'type 'vanilla)
+	      (set-span-property span 'cmd cmd))
+	  ;; If there was no command in the buffer, atomic
+	  ;; span becomes a comment.
+	  (set-span-property span 'type 'comment)))
+      (proof-set-locked-end (point-max))
+      (or (member buffer proof-script-buffer-list)
+	  (setq proof-script-buffer-list
+		(append proof-script-buffer-list (list buffer)))))))
+
+(defun proof-file-truename (filename)
+  "Returns the true name of the file FILENAME or nil."
+  (and filename (file-exists-p filename) (file-truename filename)))
+
+(defun proof-register-possibly-new-processed-file (file)
+  "Register a possibly new FILE as having been processed by the prover."
+  (let* ((cfile (file-truename file))
+	 (buffer (proof-file-to-buffer cfile)))
+    (if (not (member cfile proof-included-files-list))
+	(progn
+	  (setq proof-included-files-list
+		(cons cfile proof-included-files-list))
+	  (or (equal cfile
+		     (file-truename (buffer-file-name
+				     (car proof-script-buffer-list))))
+	      (not buffer)
+	      (proof-mark-buffer-atomic buffer))))))
+
+
+
+
+;;; begin messy COMPATIBILITY HACKING for FSFmacs.
+;;; 
+;;; In case Emacs is not aware of the function read-shell-command,
+;;; and read-shell-command-map, we duplicate some code adjusted from
+;;; minibuf.el distributed with XEmacs 20.4.
+;;;
+;;; This code is still required as of FSF Emacs 20.2.
+;;;
+;;; I think bothering with this just to give completion for
+;;; when proof-prog-name-ask-p=t is a big overkill!   - da.
+;;;	
+(defvar read-shell-command-map
+  (let ((map (make-sparse-keymap 'read-shell-command-map)))
+    (if (not (fboundp 'set-keymap-parents))
+        (if (fboundp 'set-keymap-parent)
+	    ;; FSF Emacs 20.2
+	    (set-keymap-parent map minibuffer-local-map)
+	  ;; Earlier FSF Emacs
+	  (setq map (append minibuffer-local-map map))
+	  ;; XEmacs versions?
+	  (set-keymap-parents map minibuffer-local-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.")
+
+(or (fboundp 'read-shell-command)
+    (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)))))
+
+
+;;; end messy COMPATIBILITY HACKING
+
+
+;;
+;; Misc movement functions
+;;
+
+;; FIXME da: these next two functions slightly different, why?
+;; (unprocessed-begin vs proof-locked-end)
+(defun proof-goto-end-of-locked-interactive ()
+  "Jump to the end of the locked region."
+  (interactive)
+  (switch-to-buffer (car proof-script-buffer-list))
+  (goto-char (proof-locked-end)))
+
+(defun proof-goto-end-of-locked ()
+  "Jump to the end of the locked region."
+  (goto-char (proof-unprocessed-begin)))
+
+(defun proof-in-locked-region-p ()
+  "Non-nil if point is in locked region.  Assumes proof script buffer current."
+  (< (point) (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 it."
+  (interactive)
+  (let* ((proof-script-buffer (car proof-script-buffer-list))
+	 (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))))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;          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                                       ;;
+
+
+(defun proof-check-atomic-sequents-lists (span cmd end)
+  "Check if CMD is the final command in an ACS.
+
+If CMD is matched by the end regexp in `proof-atomic-sequents-list',
+the ACS is marked in the current buffer. If CMD does not match any,
+`nil' is returned, otherwise non-nil."
+  ;;FIXME tms: needs implementation
+  nil)
+
+(defun proof-done-advancing (span)
+  "The callback function for assert-until-point."
+  (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))
+     ((proof-check-atomic-sequents-lists span cmd end))
+     ((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)
+
+      (and proof-lift-global
+	   (funcall proof-lift-global gspan)))
+     (t
+      (set-span-property span 'mouse-face 'highlight)
+      (and proof-global-p 
+	   (funcall proof-global-p cmd)
+	   proof-lift-global
+	   (funcall proof-lift-global span))))))
+
+
+
+;; FIXME da: Below it would probably be faster to use the primitive
+;; skip-chars-forward rather than scanning character-by-character 
+;; with a lisp loop over the whole region. Also I'm not convinced that
+;; Emacs should be better at skipping whitespace and comments than the
+;; proof process itself!
+
+(defun proof-segment-up-to (pos &optional next-command-end)
+  "Create a list of (type,int,string) tuples from end of locked region to POS.
+Each tuple denotes 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.
+If optional NEXT-COMMAND-END is non-nil, we contine past POS until
+the next command end."
+  (save-excursion
+      ;; 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
+    (let ((str (make-string (- (buffer-size)
+			       (proof-unprocessed-begin) -10) ?x))
+	  (i 0) (depth 0) (quote-parity t) done alist c)
+     (proof-goto-end-of-locked)
+     (while (not done)
+       (cond
+	;; Case 1. We've reached POS, not allowed to go past it,
+	;; and are inside a comment
+	((and (not next-command-end) (= (point) pos) (> depth 0))
+	 (setq done t alist (cons 'unclosed-comment alist)))
+	;; Case 2. We've reached the end of the buffer while
+	;; scanning inside a comment or string
+	((= (point) (point-max))
+	 (cond
+	  ((not quote-parity)
+	   (message "Warning: unclosed quote"))
+	  ((> depth 0)
+	   (setq done t alist (cons 'unclosed-comment alist))))
+	 (setq done t))
+	;; Case 3. Found a comment end, not inside a string
+	((and (looking-at (regexp-quote proof-comment-end)) quote-parity)
+	 (if (= depth 0) 
+	     (progn
+	       (message "Warning: extraneous comment end")
+	       (setq done t))
+	   (setq depth (- depth 1))
+	   (forward-char (length proof-comment-end))
+	   (if (eq i 0) 
+	       (setq alist (cons (list 'comment "" (point)) alist))
+	     (aset str i ?\ )
+	     (incf i))))
+	;; Case 4. Found a comment start, not inside a string
+	((and (looking-at (regexp-quote proof-comment-start)) quote-parity)
+	 (setq depth (+ depth 1))
+	 (forward-char (length proof-comment-start)))
+	;; Case 5. Inside a comment. 
+	((> depth 0)
+	 (forward-char))
+	;; Case 6. Anything else
+	(t
+	 ;; Skip whitespace before the start of a command, otherwise
+	 ;; other characters in the accumulator string str
+	 (setq c (char-after (point)))
+	 (if (or (> i 0) (not (= (char-syntax c) ?\ )))
+	     (progn
+	       (aset str i c)
+	       (incf i)))
+	 
+	 (if (looking-at "\"")	; FIXME da: should this be more generic?
+	     (setq quote-parity (not quote-parity)))
+	 
+	 (forward-char)
+
+	 ;; Found the end of a command
+	 (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-unprocessed-begin)) 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 proof-no-command 'proof-done-advancing) alist)))
+	(setq semis (cdr semis)))
+    (nreverse alist)))
+
+;;
+;; Two commands for moving forwards in proof scripts.
+;; Moving forward for a "new" command may insert spaces
+;; or new lines.  Moving forward for the "next" command
+;; does not.
+;;
+
+(defun proof-script-new-command-advance ()
+  "Move point to a nice position for a new command.
+Assumes that point is at the end of a command."
+  (interactive)
+  (if proof-one-command-per-line
+      ;; One command per line: move to next new line,
+      ;; creating one if at end of buffer or at the
+      ;; start of a blank line.  (This has the pleasing
+      ;; effect that blank regions of the buffer are
+      ;; automatically extended when inserting new commands).
+      (cond
+       ((eq (forward-line) 1)
+	(newline))
+       ((eolp)
+        (newline)
+	(forward-line -1)))
+    ;; Multiple commands per line: skip spaces at point,
+    ;; and insert the same number of spaces that were
+    ;; skipped in front of point (at least one).
+    ;; This has the pleasing effect that the spacing
+    ;; policy of the current line is copied: e.g.
+    ;;   <command>;  <command>;
+    ;; Tab columns don't work properly, however.
+    ;; Instead of proof-one-command-per-line we could
+    ;; introduce a "proof-command-separator" to improve
+    ;; this.
+    (let ((newspace (max (skip-chars-forward " \t") 1))
+	  (p (point)))
+	(insert-char ?\ newspace)
+	(goto-char p))))
+
+(defun proof-script-next-command-advance ()
+  "Move point to the beginning of the next command if it's nearby.
+Assumes that point is at the end of a command."
+  (interactive)
+  ;; skip whitespace on this line
+  (skip-chars-forward " \t")		
+  (if (and proof-one-command-per-line (eolp))
+      ;; go to the next line if we have one command per line
+      (forward-line)))
+
+
+
+; 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.
+
+;; FIXME da: this command doesn't behave as the doc string says when
+;; inside comments.  Also is unhelpful at the start of commands, and
+;; in the locked region.  I prefer the new version below.
+
+(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-check-process-available)))
+	semis)
+    (save-excursion
+      (if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t))
+	  (progn (goto-char pt)
+		 (error "I don't know what I should be doing in this buffer!")))
+      (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 "I don't know what I should be doing in this buffer!"))
+      (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-unprocessed-begin) (point) vanillas))))))
+
+
+;; da: This is my alternative version of the above.
+;; It works from the locked region too.
+;; I find it more convenient to assert up to the current command (command
+;; point is inside), and move to the next command.
+;; This means proofs can be easily replayed with point at the start
+;; of lines.  Above function gives stupid "nothing to do error." when
+;; point is on the start of line or in the locked region.
+
+;; FIXME: behaviour inside comments may be odd at the moment.  (it
+;; doesn't behave as docstring suggests, same prob as
+;; proof-assert-until-point)
+;; FIXME: polish the undo behaviour and quit behaviour of this
+;; command (should inhibit quit somewhere or other).
+
+(defun proof-assert-next-command
+  (&optional unclosed-comment-fun ignore-proof-process-p
+	     dont-move-forward for-new-command)
+  "Process until the end of the next unprocessed command after point.
+If inside a comment, just to go 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.
+Afterwards, move forward to near the next command afterwards, unless
+DONT-MOVE-FORWARD is non-nil.  If FOR-NEW-COMMAND is non-nil,
+a space or newline will be inserted automatically."
+  (interactive)
+  (let ((pt (point))
+	(crowbar (or ignore-proof-process-p (proof-check-process-available)))
+	semis)
+    (save-excursion
+      ;; CHANGE from old proof-assert-until-point: don't bother check
+      ;; for non-whitespace between locked region and point.
+      ;; CHANGE: ask proof-segment-up-to to scan until command end
+      ;; (which it used to do anyway, except in the case of a comment)
+      (setq semis (proof-segment-up-to (point) t)))
+    ;; old code:
+    ;;(if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t))
+    ;;	  (progn (goto-char pt)
+    ;;       (error "I don't know what I should be doing in this buffer!")))
+    ;; (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))
+	  ;; CHANGE: if inside a comment, do as the documentation
+	  ;; suggests.
+	  (setq semis nil))
+      (if (and (not ignore-proof-process-p) (not crowbar) (null semis))
+	  (error "I don't know what I should be doing in this buffer!"))
+      (goto-char (nth 2 (car semis)))
+      (if (not ignore-proof-process-p)
+	   (let ((vanillas (proof-semis-to-vanillas (nreverse semis))))
+;	     (if crowbar (setq vanillas (cons crowbar vanillas)))
+	     (proof-start-queue (proof-unprocessed-begin) (point) vanillas)))
+      ;; This is done after the queuing to be polite: it means the
+      ;; spacing policy enforced here is not put into the locked
+      ;; region so the user can re-edit.
+      (if (not dont-move-forward)
+	   (if for-new-command
+	       (proof-script-new-command-advance)
+	     (proof-script-next-command-advance))))))
+
+;;         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-unprocessed-begin) (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) proof-no-command
+			       (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)))
+
+;; FIXME da:  I would rather that this function moved point to
+;; the start of the region retracted?
+
+(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-check-process-available))
+    (save-excursion
+      (if (not (re-search-backward "\\S-" (proof-locked-end) t))
+	  (progn (goto-char pt)
+		 (error "I don't know what I should be doing in this buffer!")))
+      (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 "I don't know what I should be doing in this buffer!"))
+      (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-unprocessed-begin) (point) vanillas)))))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;         misc other user functions                                ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+(defun proof-undo-last-successful-command (&optional no-delete)
+  "Undo last successful command at end of locked region.
+Unless optional NO-DELETE is set, the text is also deleted from
+the proof script."
+  (interactive "p")
+  (let ((lastspan (span-at-before (proof-locked-end) 'type)))
+    (if lastspan
+	(progn
+	  (goto-char (span-start lastspan))
+	  (proof-retract-until-point (not no-delete)))
+      (error "Nothing to undo!"))))
+
+(defun proof-interrupt-process ()
+  (interactive)
+  (if (not (proof-shell-live-buffer))
+      (error "Proof Process Not Started!"))
+  (if (not (member (current-buffer) proof-script-buffer-list))
+      (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-goto-command-start ()
+  "Move point to start of current command."
+  (interactive)
+  (let ((cmd (span-at (point) 'type)))
+    (if cmd (goto-char (span-start cmd)) ; BUG: only works for unclosed proofs.
+      (let ((semis (proof-segment-up-to (point) t)))
+	(if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis)))
+	(if (and semis (car semis) (car (car semis)))
+	    (progn
+	      (goto-char (nth 2 (car (car semis))))
+	      (skip-chars-forward " \t\n")))))))
+
+(defun proof-process-buffer ()
+  "Process the current buffer and set point at the end of the buffer."
+  (interactive)
+  (goto-char (point-max))
+  (proof-assert-until-point))
+
+(defun proof-restart-buffer (buffer)
+  "Remove all extents in BUFFER and update `proof-script-buffer-list'."
+  (save-excursion
+    (if (buffer-live-p buffer)
+	(progn
+	  (set-buffer buffer)
+	  (setq proof-active-buffer-fake-minor-mode nil)
+	  (delete-spans (point-min) (point-max) 'type)
+	  (proof-detach-segments)))
+    (setq proof-script-buffer-list
+	  (remove buffer proof-script-buffer-list))))
+
+(defun proof-restart-buffers (bufferlist)
+  "Remove all extents in BUFFERLIST and update `proof-script-buffer-list'."
+  (mapcar 'proof-restart-buffer bufferlist))
+  
+;; For when things go horribly wrong
+;; FIXME: this needs to politely stop the process by sending
+;; an EOF or customizable command.  (maybe timeout waiting for
+;; it to die before killing the buffer)
+;; maybe better:
+;;  Put a funciton to remove all extents in buffers into
+;; the kill-buffer-hook for the proof shell.  Then this
+;; function just stops the shell nicely (see proof-stop-shell).
+(defun proof-restart-script ()
+  "Restart Proof General.
+Kill off the proof assistant process and remove all markings in the
+script buffers."
+  (interactive)
+  (proof-restart-buffers proof-script-buffer-list)
+  ;; { (equal proof-script-buffer-list nil) }
+   (setq proof-shell-busy nil
+	 proof-included-files-list nil
+	 proof-shell-proof-completed 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))
+   (and (buffer-live-p proof-response-buffer)
+	(kill-buffer proof-response-buffer)))
+
+;; For when things go not-quite-so-horribly wrong
+;; FIXME: this may need work, and maybe isn't needed at
+;; all (proof-retract-file when it appears may be enough).
+(defun proof-restart-script-same-process ()
+  (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)))))
+
+;; 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 (member (current-buffer) proof-script-buffer-list))
+    (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
+  "History of proof commands 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)))
+
+;; da: below functions for input history simulation are quick hacks.
+;; Could certainly be made more efficient.
+
+(defvar proof-command-history nil
+  "History used by proof-previous-matching-command and friends.")
+
+(defun proof-build-command-history ()
+  "Construct proof-command-history from script buffer.
+Based on position of point."
+  ;; let
+  )
+
+(defun proof-previous-matching-command (arg)
+  "Search through previous commands for new command matching current input."
+  (interactive))
+  ;;(if (not (memq last-command '(proof-previous-matching-command
+  ;; proof-next-matching-command)))
+      ;; Start a new search
+      
+  
+
+(defun proof-next-matching-command (arg)
+  "Search through following commands for new command matching current input."
+  (interactive "p")
+  (proof-previous-matching-command (- arg)))
+	  
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; Popup and Pulldown Menu ;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;;; Menu commands for the underlying proof assistant
+
+;;; These are defcustom'd so that users may re-configure
+;;; the system to their liking.
+;;; Functions using the above 
+
+(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)))
+
+
+
+;; FIXME: da: add more general function for inserting into the
+;; script buffer and the proof process together, and using
+;; a choice of minibuffer prompting (hated by power users, perfect
+;; for novices).
+;; Add named goals.
+;; TODO:
+;;   Add named goals.
+;;   Coherent policy for movement here and elsewhere based on
+;;    proof-one-command-per-line user option.
+;;   Coherent policy for sending to process after writing into
+;;    script buffer.  Could have one without the other.
+;;    For example, may be more easy to edit complex goal string
+;;    first in the script buffer.  Ditto for tactics, etc.
+
+(defvar proof-issue-goal-history nil
+  "History of goals for proof-issue-goal.")
+
+(defun proof-issue-goal (goal-cmd)
+  "Insert a goal command into the script buffer, issue it to prover."
+  (interactive
+   (if proof-goal-command 
+       (if (stringp proof-goal-command)
+	   (list (format proof-goal-command
+			 (read-string "Goal: " ""
+				      proof-issue-goal-history)))
+	 (proof-goal-command))
+     (error
+      "Proof General not configured for goals: set proof-goal-command.")))
+  (let ((proof-one-command-per-line t))   ; Goals always start at a new line
+    (proof-issue-new-command goal-cmd)))
+
+(defvar proof-issue-save-history nil
+  "History of theorem names for proof-issue-save.")
+
+(defun proof-issue-save (thmsave-cmd)
+  "Insert a save theorem command into the script buffer, issue it."
+  (interactive
+   (if proof-save-command
+       (if (stringp proof-save-command)
+	   (list (format proof-save-command
+			 (read-string "Save as: " ""
+				      proof-issue-save-history)))
+	 (proof-save-command))
+     (error
+      "Proof General not configured for save theorem: set proof-save-command.")))
+  (let ((proof-one-command-per-line t))   ; Goals always start at a new line
+    (proof-issue-new-command thmsave-cmd)))
+
+(defun proof-issue-new-command (cmd)
+  "Insert CMD into the script buffer and issue it to the proof assistant.
+If point is in the locked region, move to the end of it first.
+Start up the proof assistant if necessary."
+  ;; FIXME: da: I think we need a (proof-script-switch-to-buffer)
+  ;; function (so there is some control over display).
+  ;; (switch-to-buffer proof-script-buffer)
+  (if (proof-shell-live-buffer)
+      (if (proof-in-locked-region-p)
+	  (proof-goto-end-of-locked-interactive)))
+  (proof-script-new-command-advance)
+  ;; FIXME: fixup behaviour of undo here.  Really want
+  ;; to temporarily disable undo for insertion.
+  ;; (buffer-disable-undo) this trashes whole undo list!
+  (insert cmd)
+  ;; FIXME: could do proof-indent-line here, but let's
+  ;; wait until indentation is fixed.
+  (proof-assert-until-point))
+
+
+
+
+;;; To be called from menu
+(defun proof-info-mode ()
+  "Call info on Proof General."
+  (interactive)
+  (info "ProofGeneral"))
+
+(defun proof-exit ()
+  "Exit Proof-assistant."
+  (interactive)
+  (proof-restart-script))
+
+(defvar proof-help-menu
+  `("Help"
+    [,(concat proof-assistant " web page")
+     (browse-url proof-www-home-page) t]
+    ["Proof General home page"
+     (browse-url proof-general-home-page) t]
+    ["Proof General Info" proof-info-mode t]
+    )
+  "The Help Menu in Script Management.")
+
+(defvar proof-shared-menu
+  (proof-append-element
+   (append
+    (list
+     ["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)])
+    (if proof-tags-support
+	(list
+	 "----"
+	 ["Find definition/declaration" find-tag-other-window t])
+      nil))
+    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 proof command terminator, and assert up to it.
+Fire up proof process if necessary."
+  (let ((mrk (point)) ins incomment)
+    (if (looking-at "\\s-\\|\\'\\|\\w") 
+	(if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t))
+	    (error "I don't know what I should be doing in this buffer!")))
+    (if (not (= (char-after (point)) proof-terminal-char))
+	(progn (forward-char) (insert proof-terminal-string) (setq ins t)))
+    (proof-assert-until-point
+     (function (lambda ()
+		 (setq incomment t)
+		 (if ins (backward-delete-char 1))
+		 (goto-char mrk)
+		 (insert proof-terminal-string))))
+    (or incomment
+	(proof-script-next-command-advance))))
+
+(defun proof-active-terminator ()
+  "Insert the terminator, perhaps sending the command to the assistant.
+If proof-active-terminator-minor-mode is non-nil, the command will be
+sent to the assistant."
+  (interactive)
+  (if proof-active-terminator-minor-mode 
+      (proof-process-active-terminator)
+    (self-insert-command 1)))
+
+
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Proof General scripting mode definition			    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+;; da: this isn't so nice if a scripting buffer should inherit
+;; from another mode: e.g. for Isabelle, we would like to use
+;; sml-mode.
+;; FIXME: add more doc to the mode below, to give hints on
+;; configuring for new assistants.
+(define-derived-mode proof-mode fundamental-mode 
+  proof-mode-name
+  "Proof General major mode for proof scripts.
+\\{proof-mode-map}
+"
+  (setq proof-buffer-type 'script)
+
+  ;; Has buffer already been processed?
+  (and (member buffer-file-truename proof-included-files-list)
+       (proof-mark-buffer-atomic (current-buffer)))
+
+  (make-local-variable 'kill-buffer-hook)
+  (add-hook 'kill-buffer-hook
+	    (lambda ()
+	      (setq proof-script-buffer-list
+		    (remove (current-buffer) proof-script-buffer-list)))))
+
+;; FIXME: da: could we put these into another keymap already?
+;; FIXME: da: it's offensive to experience users to rebind global stuff
+;;        like meta-tab, this should be removed.
+(defconst proof-universal-keys
+  (append
+   '(([(control c) (control c)] . proof-interrupt-process)
+    ([(control c) (control v)] . proof-execute-minibuffer-cmd))
+   (if proof-tags-support
+       '(([(meta tab)]	       . tag-complete-symbol))
+     nil))
+"List of keybindings which for the script and response buffer. 
+Elements of the list are tuples (k . f) 
+where `k' is a keybinding (vector) and `f' the designated function.")
+
+;; Fixed definitions in proof-mode-map, which don't depend on
+;; prover configuration.
+;;; INDENT HACK: font-lock only recognizes define-key at start of line
+(let ((map proof-mode-map))
+(define-key map [(control c) (control e)] 'proof-find-next-terminator)
+(define-key map [(control c) (control a)] 'proof-goto-command-start)
+(define-key map [(control c) (control n)] 'proof-assert-next-command)
+(define-key map [(control c) (return)]	  'proof-assert-next-command)
+(define-key map [(control c) (control t)] 'proof-try-command)
+(define-key map [(control c) ?u]	  'proof-retract-until-point)
+(define-key map [(control c) (control u)] 'proof-undo-last-successful-command)
+(define-key map [(control c) ?\']	  'proof-goto-end-of-locked-interactive)
+(define-key map [(control button1)]	  'proof-send-span)
+(define-key map [(control c) (control b)] 'proof-process-buffer)
+(define-key map [(control c) (control z)] 'proof-frob-locked-end)
+(define-key map [(control c) (control p)] 'proof-prf)
+(define-key map [(control c) ?c]	  'proof-ctxt)
+(define-key map [(control c) ?h]	  'proof-help)
+(define-key map [(meta p)]		  'proof-previous-matching-command)
+(define-key map [(meta n)]		  'proof-next-matching-command)
+;; FIXME da: this shouldn't need setting, because it works
+;; via indent-line-function which is set below.  Check this.
+(define-key map [tab] 'proof-indent-line)
+(proof-define-keys map proof-universal-keys))
+
+
+
+;; 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 () 
+  "Finish setup of Proof General scripting mode.
+Call this function in the derived mode for the proof assistant to
+finish setup which depends on specific proof assistant configuration."
+  ;; calculate some strings and regexps for searching
+  (setq proof-terminal-string (char-to-string proof-terminal-char))
+
+  ;; FIXME: these are LEGO specific!
+  (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string))
+  (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string))
+
+  ;; FIXME da: I'm not sure we ought to add spaces here, but if
+  ;; we don't, there would be trouble overloading these settings
+  ;; to also use as regexps for finding comments.
+  ;; 
+  (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 'proof-match-find-next-function-name)
+	     fume-find-function-name-method-alist))
+
+  ;; Additional key definitions which depend on configuration for
+  ;; specific proof assistant.
+  (define-key proof-mode-map
+    (vconcat [(control c)] (vector proof-terminal-char))
+    'proof-active-terminator-minor-mode)
+
+  (define-key proof-mode-map (vector proof-terminal-char)
+    'proof-active-terminator)
+
+  (make-local-variable 'indent-line-function)
+  (setq indent-line-function 'proof-indent-line)
+
+  ;; Toolbar
+  (if (featurep 'proof-toolbar)
+      (proof-toolbar-setup))
+
+  ;; Menu
+  (easy-menu-define proof-mode-menu  
+		    proof-mode-map
+		    "Menu used in Proof General scripting mode."
+		    (cons proof-mode-name
+			  (append
+			   (cdr proof-menu)
+			   ;; begin UGLY COMPATIBILTY HACK
+			   ;; older/non-existent customize doesn't have 
+			   ;; this function.  
+			   (if (fboundp 'customize-menu-create)
+			       (list (customize-menu-create 'proof)
+				     (customize-menu-create 'proof-internal
+							    "Internals"))
+			     nil)
+			   ;; end UGLY COMPATIBILTY HACK
+			   )))
+  (easy-menu-add proof-mode-menu proof-mode-map)
+
+  ;; For fontlock
+
+  ;; setting font-lock-defaults explicitly is required by FSF Emacs
+  ;; 20.2's version of font-lock
+  (make-local-variable 'font-lock-defaults)
+  (setq font-lock-defaults '(font-lock-keywords))
+
+  ;; FIXME (da): zap commas support is too specific, should be enabled
+  ;; by each proof assistant as it likes.
+  (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.
+  ;; FIXME (da): setting this to t everywhere is too brutal.  Should
+  ;; probably make it local.
+  (and (boundp 'font-lock-always-fontify-immediately)
+       (setq font-lock-always-fontify-immediately t))
+
+  (run-hooks 'proof-mode-hook))
+
+
+
+(provide 'proof-script)
+;; proof-script.el ends here.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
new file mode 100644
index 00000000..1657b049
--- /dev/null
+++ b/generic/proof-shell.el
@@ -0,0 +1,951 @@
+;; proof-shell.el  Major mode for proof assistant script files.
+;;
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
+;;          Thomas Kleymann and Dilip Sequeira
+;;
+;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;;
+;; $Id$
+;;
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;  Starting and stopping the proof-system shell                    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun proof-shell-live-buffer ()
+  "Return buffer of active proof assistant, or nil if none running."
+  (and proof-shell-buffer
+       (comint-check-proc proof-shell-buffer)
+       proof-shell-buffer))
+
+(defun proof-start-shell ()
+  "Initialise a shell-like buffer for a proof assistant.
+
+Also generates goal and response buffers.
+Initialises current buffer for scripting.
+Does nothing if proof assistant is already running."
+  (if (proof-shell-live-buffer)
+      ()
+    (run-hooks 'proof-pre-shell-start-hook)
+    (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 "*"))
+	    proof-pbp-buffer (get-buffer-create (concat "*" proc "-goals*"))
+	    proof-response-buffer (get-buffer-create (concat "*" proc
+	    "-response*")))
+
+      (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-list (list (current-buffer)))
+      (proof-init-segmentation)
+      (setq proof-active-buffer-fake-minor-mode t)
+      (run-hooks 'proof-activate-scripting-hook)
+
+      (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)))))
+  
+
+;; Should this be the same as proof-restart-script?
+;; Perhaps this is redundant.
+(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)
+		(mapcar 'proof-detach-segments proof-script-buffer-list)
+	      (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 (member (current-buffer) proof-script-buffer-list) (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 (car proof-script-buffer-list))
+      (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 annotation field start.  A regular expression or nil.
+An eager annotation indicates to Emacs that some following output
+should be displayed immediately and not accumulated for parsing.
+Set to nil if the proof to disable this feature.")
+
+(defvar proof-shell-eager-annotation-end "$"
+  "Eager annotation field end.  A regular expression or nil.
+An eager annotation indicates to Emacs that some following output
+should be displayed immediately and not accumulated for parsing.
+Set to nil if the proof to disable this feature.
+
+The default value is \"$\" to match up to the end of the line.")
+
+(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?
+;; Answer: this is used in *specific* modes, see e.g.
+;; lego-goal-hyp.  This stuff needs making more generic.
+(defvar proof-shell-goal-regexp nil
+  "A regular expression 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 da: 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-shell-proof-completed nil
+  "Flag indicating that a completed proof has just been observed.")
+
+(defvar proof-analyse-using-stack nil
+  "Are annotations sent by proof assistant local or global")
+
+(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-output (start-regexp end-regexp append-face)
+  "Pretty print output in process buffer in specified region.
+The region begins with the match for START-REGEXP and is delimited by
+END-REGEXP. The match for END-REGEXP is not part of the specified region.
+Removes any annotations in the region.
+Fontifies the region.
+Appends APPEND-FACE to the text property of the region .
+Returns the string (with faces) in the specified region."
+  (let (start end string)
+    (save-excursion
+      (set-buffer proof-shell-buffer)
+      (goto-char (point-max))
+      (setq start (search-backward-regexp start-regexp))
+      (save-excursion (setq end (- (search-forward-regexp end-regexp)
+				   (length (match-string 0)))))
+      (setq string
+	    (proof-shell-strip-annotations (buffer-substring start end)))
+      (delete-region start end)
+      (insert string)
+      (setq end (+ start (length string)))
+      ;; This doesn't work with FSF Emacs 20.2's version of Font-lock
+      ;; because there are no known keywords in the process buffer
+      ;; Never mind. In a forthcoming version, the process buffer will
+      ;; not be tempered with. Fontification will take place in a
+      ;; separate response buffer.
+      ;; (font-lock-fontify-region start end)
+      (font-lock-append-text-property start end 'face append-face)
+      (buffer-substring start end))))
+
+(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")))
+
+
+;; Notes on markup in the scripting buffer. (da)
+;;
+;; The locked region is covered by a collection of non-overlaping
+;; spans (our abstraction of extents/overlays).
+;;
+;; For an unfinished proof, there is one extent for each command 
+;; or comment outside a command.   For a finished proof, there
+;; is one extent for the whole proof.
+;;
+;; Each command span has a 'type property, one of:
+;;
+;;     'vanilla      Initialised in proof-semis-to-vanillas, for
+;;     'goalsave 
+;;     'comment      A comment outside a command.
+;;
+;;  All spans except those of type 'comment have a 'cmd property,
+;;  which is set to a string of its command.  This is the
+;;  text in the buffer stripped of leading whitespace and any comments.
+;;
+;; 
+
+(defun proof-shell-handle-error (cmd string)
+  "React on an error message triggered by the prover.
+We display the process buffer, scroll to the end, beep and fontify the
+error message. At the end it calls `proof-shell-handle-error-hook'. "
+    ;; We extract all text between text matching
+    ;; `proof-shell-error-regexp' and the following prompt.
+    ;; Alternatively one could higlight all output between the
+    ;; previous and the current prompt.
+    ;; +/- of our approach
+    ;; + Previous not so relevent output is not highlighted
+    ;; - Proof systems have to conform to error messages whose start  can be
+    ;;   detected by a regular expression.
+  (proof-shell-handle-output
+   proof-shell-error-regexp proof-shell-annotated-prompt-regexp
+   'font-lock-error-face)
+  (save-excursion (display-buffer proof-shell-buffer)
+		  (beep)
+
+		  ;; unwind script buffer
+		  (set-buffer (car proof-script-buffer-list))
+		  (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 (car proof-script-buffer-list)))
+  (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)
+  "Process shell output by matching on STRING.
+This function 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'.
+
+This 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-proof-completed t)
+    (setq proof-shell-delayed-output
+	  (cons 'insert (concat "\n" (match-string 0 string)))))
+
+   ((string-match proof-shell-start-goals-regexp string)
+    (setq proof-shell-proof-completed nil)
+    (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)
+    (setq proof-shell-proof-completed nil)
+    (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                     ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; FIXME da: Should this kind of ordinary input go onto the queue of
+;; things to do?  Then errors during processing would prevent it being
+;; sent.  Also the proof shell lock would be set automatically, which
+;; might be nice?
+(defun proof-shell-insert (string)
+  (save-excursion
+    (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))))
+
+;; da: This function strips carriage returns from string, then
+;; sends it.  (Why strip CRs?)
+(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)))
+
+(defun proof-check-process-available (&optional relaxed)
+  "Adjust internal variables for scripting of current buffer.
+
+Signals an error if current buffer is not a proof script or if the
+proof process is not idle. If RELAXED is set, nothing more is done. No
+changes are necessary if the current buffer is already in Scripting
+minor mode. Otherwise, the current buffer will become the current
+scripting buffer provided the current scripting buffer has either no
+locked region or everything in it has been processed."
+  (proof-start-shell)
+  (cond
+   ((not (or relaxed (eq proof-buffer-type 'script)))
+    (error "Must be running in a script buffer"))
+   (proof-shell-busy (error "Proof Process Busy!"))
+   (relaxed ())			;exit cond
+
+   ;; No buffer is in Scripting minor mode.
+   ;; We assume the setup is done somewhere else
+   ;; so this should never happen
+   ((null proof-script-buffer-list) (assert nil))
+
+   ;; The current buffer is in Scripting minor mode
+   ;; so there's nothing to do
+   ((equal (current-buffer) (car proof-script-buffer-list)))
+
+   (t
+    (let ((script-buffer (car proof-script-buffer-list))
+	  (current-buffer (current-buffer)))
+      (save-excursion
+	(set-buffer script-buffer)
+	;; We only allow switching of the Scripting buffer if the
+	;; locked region is either empty or full for all buffers.
+	;; Here we check the current Scripting buffer's status.
+	(let
+	    ((locked-is-empty (eq (proof-unprocessed-begin) (point-min)))
+	     (locked-is-full  (progn
+				(goto-char (point-max))
+				(skip-chars-backward " \t\n")
+				(>= (proof-unprocessed-begin) (point)))))
+	  (if locked-is-full
+	      ;; We're switching from a buffer which has been
+	      ;; completely processed.  Make sure that it's
+	      ;; registered on the included files list, in
+	      ;; case it has been processed piecemeal.
+	      (if buffer-file-name
+		  (proof-register-possibly-new-processed-file 
+		   buffer-file-name)))
+
+	  (if (or locked-is-full locked-is-empty)
+	      ;; we are changing the scripting buffer
+	      (progn
+		(setq proof-active-buffer-fake-minor-mode nil)
+		(set-buffer current-buffer)
+
+		;; does the current buffer contain locked regions already?
+		(if (member current-buffer proof-script-buffer-list)
+		    (setq proof-script-buffer-list
+			  (remove current-buffer proof-script-buffer-list))
+		  (proof-init-segmentation))
+		(setq proof-script-buffer-list
+		      (cons current-buffer proof-script-buffer-list))
+		(setq proof-active-buffer-fake-minor-mode t)
+		(run-hooks 'proof-activate-scripting-hook))
+	    ;; Locked region covers only part of the buffer
+	    ;; FIXME da: ponder alternative of trying to complete rest
+	    ;; of current scripting buffer?
+	    (error "Cannot deal with two unfinished script buffers!"))))))))
+
+
+(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 in proof-release-lock: Proof process not busy")
+	    (message "Nag, nag, nag: proof-release-lock: Proof process not busy"))
+	(if (not (member (current-buffer) proof-script-buffer-list))
+	    (error "Bug in proof-release-lock: 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))) 
+		       proof-no-command))
+    (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
+
+
+;; 
+;; 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.
+
+(defun proof-shell-exec-loop () 
+"Process the proof-action-list.
+proof-action-list contains a list of (span,command,action) triples.
+This function is called with a non-empty proof-action-list, where the
+head of the list is the previously executed command which succeeded.
+We execute (action span) on the first item, then (action span) on
+following items which have proof-no-command as their cmd components.
+Return non-nil if the action list becomes empty; unlock the process
+and removes the queue region.  Otherwise send the next command to the
+proof process."
+  (save-excursion
+    (set-buffer (car proof-script-buffer-list))
+    ;; (if (null proof-action-list) 
+    ;;	(error "proof-shell-exec-loop: called with empty proof-action-list."))
+    ;; Be more relaxed about calls with empty action list
+    (if proof-action-list
+	(let ((item (car proof-action-list)))
+	  ;; Do (action span) on first item in list
+	  (funcall (nth 2 item) (car item))
+	  (setq proof-action-list (cdr proof-action-list))
+	  ;; Process following items in list with the form
+	  ;; ("COMMENT" cmd) by calling (cmd "COMMENT")
+	  (while (and proof-action-list
+		      (string= 
+		       (nth 1 (setq item (car proof-action-list))) 
+		       proof-no-command))
+	    ;; Do (action span) on comments
+	    (funcall (nth 2 item) (car item))
+	    (setq proof-action-list (cdr proof-action-list)))
+	  ;; If action list is empty now, release the process lock
+	  (if (null proof-action-list)
+	      (progn (proof-release-lock)
+		     (proof-detach-queue)
+		     ;; indicate finished
+		     t)
+	    ;; Send the next command to the process
+	    (proof-send (nth 1 item))
+	    ;; indicate not finished
+	    nil))
+      ;; Just indicate finished if called with empty proof-action-list.
+      t)))
+
+(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 (car proof-script-buffer-list))
+    (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.
+
+;; FIXME: highlight eager annotation-end : fix proof-shell-handle-output
+;; to highlight whole string.
+(defun proof-shell-popup-eager-annotation ()
+  "Process urgent messages.
+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 ((str (proof-shell-handle-output
+	      proof-shell-eager-annotation-start
+	      proof-shell-eager-annotation-end
+	      'font-lock-eager-annotation-face))
+	file module)
+    (proof-message str)))
+
+(defun proof-response-buffer-display (str face)
+  "Display STR with FACE in response buffer."
+  (let ((start))
+    (save-excursion
+      (set-buffer proof-response-buffer)
+      (setq start (goto-char (point-max)))
+      (insert str)
+      (font-lock-fontify-region start (point-max))
+      (font-lock-append-text-property start (point-max) 'face face)
+      (insert "\n"))))
+
+(defun proof-file-to-buffer (filename)
+  "Converts a FILENAME  into a buffer name"
+  (let* ((buffers (buffer-list))
+	 (pos
+	  (position (file-truename filename)
+		    (mapcar 'proof-file-truename
+			    (mapcar 'buffer-file-name
+				    buffers))
+		    :test 'equal)))
+    (and pos (nth pos buffers))))
+
+(defun proof-files-to-buffers (filenames)
+  "Converts a list of FILENAMES into a list of BUFFERS."
+  (if (null filenames) nil
+    (let* ((buffer (proof-file-to-buffer (car filenames)))
+	  (rest (proof-files-to-buffers (cdr filenames))))
+      (if buffer (cons buffer rest) rest))))
+	  
+		  
+(defun proof-shell-process-urgent-message (message)
+  "Display and analyse urgent MESSAGE for asserting or retracting files."
+  
+  ;; Is the prover processing a file?
+  (cond ((and proof-shell-process-file 
+	      (string-match (car proof-shell-process-file) message))
+	 (let
+	     ((file (funcall (cdr proof-shell-process-file) message)))
+	   (if (string= file "") 
+	       (setq file (buffer-file-name (car proof-script-buffer-list))))
+	   (if file
+	       (proof-register-possibly-new-processed-file file))))
+
+  ;; Is the prover retracting across files?
+	((and proof-shell-retract-files-regexp
+	      (string-match proof-shell-retract-files-regexp message))
+	 (let ((current-included proof-included-files-list))
+	   (setq proof-included-files-list
+		 (funcall proof-shell-compute-new-files-list message))
+	   (proof-restart-buffers
+	    (remove (car proof-script-buffer-list)
+		    (proof-files-to-buffers
+		     (set-difference current-included
+				     proof-included-files-list))))))
+	(t
+	 (proof-message message)
+	 (proof-response-buffer-display message
+					'font-lock-eager-annotation-face))))
+
+(defun proof-shell-process-urgent-messages (str)
+  "Scan the process output for urgent messages.
+Display them immediately in the Response buffer.
+Keep `proof-included-files-list' up to date.
+The input STR is the most recent chunk of output sent to the process
+filter. We assume that urgent messages are fully contained in STR."
+  (let ((start (string-match proof-shell-eager-annotation-start str))
+	end)
+    (and start
+	 (setq end
+	       (string-match proof-shell-eager-annotation-end str
+	       start))
+	 (progn
+	   (proof-shell-process-urgent-message
+	    (proof-shell-strip-annotations (substring str start end)))
+	   (proof-shell-process-urgent-messages (substring str end))))))
+
+(defun proof-shell-filter (str) 
+  "Filter for the proof assistant 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."
+  (and proof-shell-eager-annotation-start
+       (proof-shell-process-urgent-messages str)) 
+       
+  (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 annotated 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)
+	    (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?
+	  (setq cmd (nth 1 (car proof-action-list)))
+	  (save-excursion
+	    ;; 
+	    (setq res (proof-shell-process-output cmd string))
+	    ;; da: Added this next line to redisplay, for proof-toolbar
+	    ;; FIXME: should do this for all frames displaying the script
+	    ;; buffer!
+	    ;; ODDITY: has strange effect on highlighting, leave it.
+	    ;; (redisplay-frame (window-buffer  t)
+	    (cond
+	     ((eq (car-safe res) 'error)
+	      (proof-shell-handle-error cmd (cdr res)))
+	     ((eq res 'interrupt)
+	      (proof-shell-handle-interrupt))
+	     ((eq (car-safe 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)))
+    
+(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))
+
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Proof General shell mode definition				    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; 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 proof-shell-proof-completed nil)
+  (make-local-variable 'proof-shell-insert-hook)
+
+  ;; comint customisation. comint-prompt-regexp is used by
+  ;; comint-get-old-input, comint-skip-prompt, comint-bol, backward
+  ;; matching input, etc.  
+  (setq comint-prompt-regexp proof-shell-prompt-pattern)
+
+  ;; An article by Helen Lowe in UITP'96 suggests that the user should
+  ;; not see all output produced by the proof process. 
+  (remove-hook 'comint-output-filter-functions
+	       'comint-postoutput-scroll-to-bottom 'local)
+
+  (add-hook 'comint-output-filter-functions 'proof-shell-filter nil 'local)
+  (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 Proof General shell mode."
+		  (cons proof-mode-name (cdr proof-shell-menu)))
+
+(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-shell)
+;; proof-shell.el ends here.
\ No newline at end of file
diff --git a/generic/proof.el b/generic/proof.el
index 91036383..8a5b00f2 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -12,36 +12,46 @@
 ;;
 ;; $Id$
 ;;
-;; PENDING:
+
+(require 'proof-site)
+
+
 ;;
-;; da: I propose splitting this file as follows:
 ;;
-;;  proof.el         Controls loading.  Requires proof-script, proof-shell.
-;;		     Retains misc utils, user options, splash screen.
-;;  proof-script.el  Script management mode.
-;;  proof-shell.el   Proof shell mode.
+;; User options for proof mode
 ;;
-;; The shell mode and script mode are already fairly independent in
-;; this file.
+;; See proof-config.el for configuration variables.
 ;;
-
-(require 'proof-site)
-
 ;;
-;; Here is the first configuration variable, proof-assistant.
-;; Others follow below, along with notes about the prover-config
-;; customization group.
+;; The following variables are user options for Proof General.
+;; They appear in the 'proof' customize group and should
+;; not normally be touched by prover specific code.
 ;;
-(defgroup prover-config nil
-  "Configuration of Proof General for the prover in use."
-  :group 'proof-internal)
 
-(defcustom proof-assistant ""
-  "Name of the proof assistant Proof General is using.
-This is set automatically by the mode stub defined in proof-site,
-from the name given in proof-internal-assistant-table."
+(defcustom proof-prog-name-ask-p nil
+  "*If non-nil, query user which program to run for the inferior process."
+  :type 'boolean
+  :group 'proof)
+
+(defcustom proof-one-command-per-line nil
+  "*If non-nil, format for newlines after each proof command in a script."
+  :type 'boolean
+  :group 'proof)
+
+(defcustom proof-general-home-page
+  "http://www.dcs.ed.ac.uk/home/proofgen"
+  "*Web address for Proof General"
   :type 'string
-  :group 'proof-config)
+  :group 'proof-internal)
+
+;; configuration variables
+(require 'proof-config)			
+
+;; A global constant
+(defconst proof-mode-name "Proof-General"
+  "Root name for proof script mode.  
+Used internally and in menu titles.")
+
 
 
 ;;;
@@ -180,27 +190,33 @@ No effect if proof-display-splash-time is zero."
 ))
 ;;; End splash screen code
 
+
 
 ;;;
-;;; Requires for included modules.
+;;; Load included modules.
 ;;;
 
-;; FIXME da: I think some of these should be autoloaded (etags,...)
+
+;; FIXME da: I think these ones should be autoloaded!!
 (require 'cl)
 (require 'compile)
 (require 'comint)
 (require 'etags)			
+(require 'easymenu)
+
+
+;; Spans are our abstraction of extents/overlays.
 (cond ((fboundp 'make-extent) (require 'span-extent))
       ((fboundp 'make-overlay) (require 'span-overlay))
       (t nil))
-(require 'easymenu)			; present in XEmacs 20.4 by default.
+
 
 (require 'proof-syntax)
 (require 'proof-indent)
 
 
 ;; browse-url function doesn't seem to be autoloaded in
-;; XEmacs 20.4, is in FSF Emacs 20.2.
+;; XEmacs 20.4, but it is in FSF Emacs 20.2.
 (or (fboundp 'browse-url)
     (autoload 'browse-url "browse-url"
       "Ask a WWW browser to load URL." t))
@@ -212,2785 +228,16 @@ No effect if proof-display-splash-time is zero."
    (list 'make-variable-buffer-local (list 'quote var))
    (list 'setq-default var value)))
 
-;; Load toolbar code if toolbars available.
-(if (featurep 'toolbar)
-    (require 'proof-toolbar))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; User options                                                     ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; The following variables are user options for Proof General.
-;; They appear in the 'proof' customize group and should
-;; not normally be touched by prover specific code.
-;;
-;;
-(defcustom proof-prog-name-ask-p nil
-  "*If non-nil, query user which program to run for the inferior process."
-  :type 'boolean
-  :group 'proof)
-
-(defcustom proof-one-command-per-line nil
-  "*If non-nil, format for newlines after each proof command in a script."
-  :type 'boolean
-  :group 'proof)
-
-(defcustom proof-general-home-page
-  "http://www.dcs.ed.ac.uk/home/proofgen"
-  "*Web address for Proof General"
-  :type 'string
-  :group 'proof-internal)
- 
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Configuration for proof assistant				    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; The variables in the "prover-config" customize group are those
-;; which are intended to be set by the prover specific elisp,
-;; i.e. constants set on a per-prover basis.
-;;
-;; Putting these in a customize group is useful for documenting
-;; this type of variable, and for developing a new instantiation
-;; of Proof General.
-;; But it is *not* useful for final user-level customization!
-;; The reason is that saving these customizations across a session is
-;; not liable to work, because the prover specific elisp usually
-;; overrides with a series of setq's in <assistant>-mode-config type
-;; functions.  This is why prover-config appears under the
-;; proof-internal group.
-;;
-;;
-
-;; The Customization menus would be nicer if the variables in
-;; prover-config group were uniformly renamed prover-config-*
-;; (and similarly for other variables/groups).  But it's
-;; somewhat of a horror in the code?
-
-(defcustom proof-www-home-page ""
-  "Web address for information on proof assistant"
-  :type 'string
-  :group 'prover-config)
-
-(defcustom proof-shell-cd nil
-  "Command to the inferior process to change the directory."
-  :type 'string
-  :group 'prover-config)
-
-(defcustom proof-tags-support t
-  "If non-nil, include tags functions in menus.
-This variable should be set before requiring proof.el"
-  :type 'boolean
-  :group 'prover-config)
-
-(defcustom proof-shell-process-output-system-specific nil
-  "Set this variable to handle system specific output.
-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 pair 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."
-  :type '(cons (function function))
-  :group 'prover-config)
-
-(defcustom proof-activate-scripting-hook nil
-  "Hook run when a buffer is switched into scripting mode.
-The current buffer will be the newly active scripting buffer.
-
-This hook may be useful for synchronizing with the proof
-assistant, for example, to switch to a new theory.")
-
-;;
-;; The following variables should be set before proof-config-done
-;; is called.  These configure the mode for the script buffer,
-;; including highlighting, etc.
-;;
-
-(defgroup proof-script nil
-  "Proof General configuration of scripting buffer mode."
-  :group 'prover-config)
-
-
-(defcustom proof-terminal-char nil
-  "Character which terminates a proof command in a script buffer."
-  :type 'character
-  :group 'proof-script)
-
-(defcustom proof-comment-start ""
-  "String which starts a comment in the proof assistant command language.
-The script buffer's comment-start is set to this string plus a space."
-  :type 'string
-  :group 'proof-script)
-
-(defcustom proof-comment-end ""
-  "String which starts a comment in the proof assistant command language.
-The script buffer's comment-end is set to this string plus a space."
-  :type 'string
-  :group 'proof-script)
-
-(defcustom proof-save-command-regexp nil 
-  "Matches a save command"
-  :type 'regexp
-  :group 'prover-config)
-
-(defcustom proof-save-with-hole-regexp nil 
-  "Matches a named save command"
-  :type 'regexp
-  :group 'proof-script)
-
-(defcustom proof-goal-with-hole-regexp nil 
-  "Matches a saved goal command"
-  :type 'regexp
-  :group 'proof-script)
-
-(defcustom proof-goal-command-p nil 
-  "Is this a goal"
-  :type 'function
-  :group 'proof-script)
-
-(defcustom proof-lift-global nil
-  "This function lifts local lemmas from inside goals out to top level.
-This function takes the local goalsave span as an argument. Set this
-to `nil' of the proof assistant does not support nested goals."
-  :type '(choice nil function)
-  :group 'proof-script)
-
-(defcustom proof-count-undos-fn nil 
-  "Compute number of undos in a target segment"
-  :type 'function
-  :group 'proof-script)
-
-(defcustom proof-atomic-sequence-lists nil
-  "list of instructions for setting up atomic sequences of commands (ACS).
-
-Each instruction is
-a list of the form `(END START &optional FORGET-COMMAND)'. END is a
-regular expression to recognise the last command in an ACS. START
-is a function. Its input is the last command of an ACS. Its output
-is a regular exression to recognise the first command of the ACS.
-It is evaluated once and the output is successively matched agains
-previously processed commands until a match occurs (or the
-beginning of the current buffer is reached). The region determined
-by (START,END) is locked as an ACS. Optionally, the ACS is
-annotated with the actual command to retract the ACS. This is
-computed by applying FORGET-COMMAND to the first and last command
-of the ACS."
-  :type '(repeat (cons regexp function (choice (const nil) function)))
-  :group 'proof-shell)
-
-
-(defconst proof-no-command "COMMENT"
-  "String used as a nullary action (send no command to the proof assistant).
-Only relevant for proof-find-and-forget-fn.")
-
-(defcustom proof-find-and-forget-fn nil
-  "Function returning a command string to forget back to before its argument span.
-The special string proof-no-command means there is nothing to do."
-  :type 'function
-  :group 'proof-script)
-
-(defcustom 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"
-  :type 'function
-  :group 'proof-script)
-
-(defcustom proof-kill-goal-command ""
-  "Command to kill a goal."
-  :type 'string
-  :group 'proof-script)
-
-(defcustom proof-global-p nil
-  "Whether a command is a global declaration.  Predicate on strings or nil.
-This is used to handle nested goals allowed by some provers."
-  :type 'function
-  :group 'proof-script)
-
-(defcustom proof-state-preserving-p nil
-  "A predicate, non-nil if its argument preserves the proof state."
-  :type 'function
-  :group 'proof-script)
-
-(defcustom pbp-change-goal nil
-  "Command to change to the goal %s"
-  :type 'string
-  :group 'prover-config)
-
-;;
-;; The following variables should be set in
-;; proof-pre-shell-start-hook.
-;;
-
-;; FIXME da: these could be put in another customize group? 
-
-(defcustom proof-prog-name nil
-  "Command to run program name in proof shell"
-  :type 'string
-  :group 'prover-config)
-
-(defcustom proof-mode-for-shell nil
-  "Mode for proof shell"
-  :type 'function
-  :group 'prover-config)
-
-(defcustom proof-mode-for-pbp nil
-  "Mode for Proof-by-Pointing."
-  :type 'function
-  :group 'prover-config)
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  Generic config for proof shell	                            ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; The variables in this section concern the proof shell mode.
-;; The first group of variables are hooks invoked at various points.
-;; The second group of variables are concerned with matching the output
-;; from the proof assistant.
-;;
-;; Variables here are put into the customize group 'proof-shell'.
-;;
-;; These should be set in the shell mode configuration, again,
-;; before proof-shell-config-done is called.
-;;
-
-(defgroup proof-shell nil
-  "Settings for output from the proof assistant in the proof shell."
-  :group 'prover-config)
-
-;;
-;; Hooks for the proof shell
-;;
-
-(defcustom proof-shell-insert-hook nil 
-  "Hooks run by proof-shell-insert before inserting a command.
-Can be used to configure the proof assistant to the interface in
-various ways (for example, setting the line width of output).
-Any text inserted by these hooks will be sent to the proof process
-before every command issued by Proof General."
-  :type '(repeat function)
-  :group 'proof-shell)
-
-(defcustom proof-pre-shell-start-hook nil
-  "Hooks run before proof shell is started.
-Usually this is set to a function which configures the proof shell
-variables."
-  :type '(repeat function)
-  :group 'proof-shell)
-
-(defcustom proof-shell-init-cmd ""
-   "The command for initially configuring the proof process."
-   :type '(choice string (const nil))
-   :group 'proof-shell)
-
-(defcustom proof-shell-handle-delayed-output-hook
-  '(proof-pbp-focus-on-first-goal)
-  "Hooks run after new output has been displayed in the RESPONSE buffer."
-  :type '(repeat function)
-  :group 'proof-shell)
-
-(defcustom proof-shell-handle-error-hook
-  '(proof-goto-end-of-locked-if-pos-not-visible-in-window)
-  "Hooks run after an error has been reported in the RESPONSE buffer."
-  :type '(repeat function)
-  :group 'proof-shell)  
-
 ;;
-;; Regexp variables for matching output from proof process.
+;; Rest of code
 ;;
 
-(defcustom proof-shell-prompt-pattern nil 
-   "Proof shell's value for comint-prompt-pattern, which see."
-   :type 'regexp
-   :group 'proof-shell)
-
-;; FIXME da: replace this with wakeup-regexp or prompt-regexp?
-;; May not need next variable.
-(defcustom proof-shell-wakeup-char nil
-  "A special character which terminates an annotated prompt.
-Set to nil if proof assistant does not support annotated prompts."
-  :type '(choice character (const nil))
-  :group 'proof-shell)
-
-(defcustom proof-shell-annotated-prompt-regexp ""
-  "Regexp matching a (possibly annotated) prompt pattern.
-Output is grabbed between pairs of lines matching this regexp.
-To help matching you may be able to annotate the proof assistant
-prompt with a special character not appearing in ordinary output.
-The special character should appear in this regexp, should
-be the value of proof-shell-wakeup-char."
-  :type 'regexp
-  :group 'proof-shell)
-
-(defcustom proof-shell-abort-goal-regexp nil
-  "Regexp matching output from an aborted proof."
-  :type 'regexp
-  :group 'proof-shell)
-
-(defcustom proof-shell-error-regexp nil
-  "Regexp matching an error report from the proof assistant.
-We assume that an error message corresponds to a failure
-in the last proof command executed.  (So don't match
-mere warning messages with this regexp)."
-  :type 'regexp
-  :group 'proof-shell) 
-
-(defcustom proof-shell-interrupt-regexp nil
-  "Regexp matching output indicating the assistant was interrupted."
-  :type 'regexp
-  :group 'proof-shell) 
-
-(defcustom proof-shell-proof-completed-regexp nil
-  "Regexp matching output indicating a finished proof."
-  :type 'regexp
-  :group 'proof-shell)
-
-(defcustom proof-shell-result-start ""
-  "Regexp matching start of an output from the prover after pbp commands.
-In particular, after a `pbp-goal-command' or a `pbp-hyp-command'."
-  :type 'regexp
-  :group 'proof-shell)
-
-(defcustom proof-shell-result-end ""
-  "Regexp matching end of output from the prover after pbp commands.
-In particular, after a `pbp-goal-command' or a `pbp-hyp-command'."
-  :type 'regexp
-  :group 'proof-shell)
-
-(defcustom proof-shell-start-goals-regexp ""
-  "Regexp matching the start of the proof state output."
-  :type 'regexp
-  :group 'proof-shell)
-
-(defcustom proof-shell-end-goals-regexp ""
-  "Regexp matching the end of the proof state output."
-  :type 'regexp
-  :group 'proof-shell)
-
-(defcustom pbp-error-regexp nil
-  "Regexp indicating that the proof process has identified an error."
-  :type 'regexp
-  :group 'proof-shell)
-
-(defcustom proof-shell-process-file nil
-  "A tuple of the form (regexp . function) to match a processed file name.
-
-If REGEXP matches output, then the function FUNCTION is invoked on the
-output string chunk. It must return a script file name (with complete
-path) the system is currently processing. In practice, FUNCTION is
-likely to inspect the match data.  If it returns the empty string,
-the file name of the scripting buffer is used instead.  If it
-returns nil, no action is taken.
-
-Care has to be taken in case the prover only reports on compiled
-versions of files it is processing. In this case, FUNCTION needs to
-reconstruct the corresponding script file name. The new (true) file
-name is added to the front of `proof-included-files-list'."
-  :type '(choice (cons regexp function) (const nil))
-  :group 'proof-shell)
-
-(defcustom proof-shell-retract-files-regexp nil
-  "A REGEXP to match that the prover has retracted across file boundaries.
-
-At this stage, Proof General's view of the processed files is out of
-date and needs to be updated with the help of the function
-`proof-shell-compute-new-files-list'."
-  :type '(choice regexp (const nil))
-  :group 'proof-shell)
-
-(defcustom proof-shell-compute-new-files-list nil
-  "Function to update `proof-included-files list'.
-
-It needs to return an up to date list of all processed files. Its
-output is stored in `proof-included-files-list'. Its input is the
-string of which `proof-shell-retract-files-regexp' matched a
-substring. In practice, this function is likely to inspect the
-previous (global) variable `proof-included-files-list' and the match
-data triggered by `proof-shell-retract-files-regexp'."
-  :type '(choice function (const nil))
-  :group 'proof-shell)
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  Internal variables used by scripting and pbp                    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defconst proof-mode-name "Proof-General")
-
-;; FIXME da: remove proof-terminal-string.  At the moment some
-;; commands need to have the terminal string, some don't.
-;; We should assume commands are terminated properly at the
-;; specific level.
-(defvar proof-terminal-string nil 
-  "End-of-line string for proof process.")
-
-(defvar proof-re-end-of-cmd nil 
-  "Regexp matching end of command.  Based on proof-terminal-string.
-Set in proof-config-done.")
-
-(defvar proof-re-term-or-comment nil 
-  "Regexp matching terminator, comment start, or comment end.
-Set in proof-config-done.")
-
-(defvar proof-marker nil 
-  "Marker in proof shell buffer pointing to previous command input.")
-
-(defvar proof-shell-buffer nil
-  "Process buffer where the proof assistant is run.")
-
-(defvar proof-script-buffer-list nil
-  "Scripting buffers with locked regions.
-The first element is current and in scripting minor mode.
-The cdr of the list of corresponding file names is a subset of
-`proof-included-files-list'.")
-
-(defvar proof-pbp-buffer nil
-  "The goals buffer (also known as the pbp buffer).")
-
-(defvar proof-response-buffer nil
-  "The response buffer.")
-
-(defvar proof-shell-busy nil 
-  "A lock indicating that the proof shell is processing.
-When this is non-nil, proof-check-process-available will give
-an error.")
-
-(deflocal proof-buffer-type nil 
-  "Symbol indicating the type of this buffer: 'script, 'shell, or 'pbp.")
-
-(defvar proof-action-list nil "action list")
-
-(defvar proof-included-files-list nil 
-  "List of files currently included in proof process.
-Whenever a new file is being processed, it gets added to the front of
-the list. When the prover retracts across file boundaries, this list
-is resynchronised. It contains files in canonical truename format")
-
-(deflocal proof-active-buffer-fake-minor-mode nil
-  "An indication in the modeline that this is the *active* script buffer")
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; A few small utilities					    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun proof-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. Moves point after the match.
-
-The package fume-func provides the function
-`fume-match-find-next-function-name' with the same specification.
-However, fume-func's version is incorrec"
-  ;; DO NOT USE save-excursion; we need to move point!
-  ;; save-excursion is called at a higher level in the func-menu
-  ;; package 
-    (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-message (str)
-  "Output STR in minibuffer."
-  (message (concat "[" proof-assistant "] " str)))
-
-;; append-element in tl-list
-(defun proof-append-element (ls elt)
-  "Append ELT to last of LS if ELT is not nil. [proof.el]
-This function coincides with `append-element' in the package
-[tl-list.el.]"
-  (if elt
-      (append ls (list elt))
-    ls))
-
-(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) 
-  "Return the list of words in S separated by SEPARATOR."
-  (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)))))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Basic code for the locked region and the queue region            ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; FIXME: da: doc below needs fixing.
-(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)
-
-(defface proof-queue-face
-  '((((type x) (class color) (background light))
-     (:background "mistyrose"))
-    (((type x) (class color) (background dark))
-     (:background "mediumvioletred"))
-    (t				
-     (:foreground "white" :background "black")))
-  "Face for commands in proof script waiting to be processed."
-  :group 'proof)
-
-(defface proof-locked-face
-  '((((type x) (class color) (background light))   
-     (:background "lavender"))
-    (((type x) (class color) (background dark))   
-     (:background "navy"))
-    (t				
-     (:underline t)))
-  "Face for locked region of proof script (processed commands)."
-  :group 'proof)
-
-(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)
-
-  (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)
-
-  (set-span-property proof-locked-span 'face 'proof-locked-face)
-
-  (detach-span proof-locked-span))
-
-(defsubst proof-lock-unlocked ()
-  "Make the locked region read only."
-  (span-read-only proof-locked-span))
-
-(defsubst proof-unlock-locked ()
-  "Make the locked region read-write."
-  (span-read-write proof-locked-span))
-
-(defsubst proof-set-queue-endpoints (start end)
-  "Set the queue span to be START, END."
-  (set-span-endpoints proof-queue-span start end))
-
-(defsubst proof-set-locked-endpoints (start end)
-  "Set the locked span to be START, END."
-  (set-span-endpoints proof-locked-span start end))
-
-(defsubst proof-detach-queue ()
-  "Remove the span for the queue region."
-  (and proof-queue-span (detach-span proof-queue-span)))
-
-(defsubst proof-detach-locked ()
-  "Remove the span for the locked region."
-  (and proof-locked-span (detach-span proof-locked-span)))
-
-(defsubst proof-set-queue-start (start)
-  "Set the queue span to begin at START."
-  (set-span-start proof-queue-span start))
-
-(defsubst proof-set-queue-end (end)
-  "Set the queue span to end at END."
-  (set-span-end proof-queue-span end))
-
-(defun proof-detach-segments (&optional buffer)
-  "Remove locked and queue region from BUFFER.
-Defaults to current buffer when BUFFER is nil."
-  (let ((buffer (or buffer (current-buffer))))
-    (save-excursion
-      (proof-detach-queue)
-      (proof-detach-locked))))
-
-(defsubst proof-set-locked-end (end)
-  "Set the end of the locked region to be END, sort of? FIXME.
-If END is past the end of the buffer, remove the locked region.
-Otherwise set the locked region to be from the start of the
-buffer to END."
-  (if (>= (point-min) end)
-      (proof-detach-locked)
-    (set-span-endpoints proof-locked-span (point-min) end)))
-
-(defun proof-unprocessed-begin ()
-  "Return end of locked region in current buffer or (point-min) otherwise."
-  (or 
-   (and (member (current-buffer) proof-script-buffer-list)
-	proof-locked-span (span-end proof-locked-span))
-   (point-min)))
-
-(defun proof-locked-end ()
-  "Return end of the locked region of the current buffer.
-Only call this from a scripting buffer."
-  (if (member (current-buffer) proof-script-buffer-list)
-      (proof-unprocessed-begin)
-    (error "bug: proof-locked-end called from wrong buffer")))
-
-(defsubst proof-end-of-queue ()
-  "Return the end of the queue region, or nil if none."
-  (and proof-queue-span (span-end proof-queue-span)))
-
-(defun proof-dont-show-annotations ()
-  "Set display values of annotations (characters 128-255) to be invisible."
-  (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)))))
-
-(defun proof-mark-buffer-atomic (buffer)
-  "Mark BUFFER as having been processed in a single step.
-
-If buffer already contains a locked region, only the remainder of the
-buffer is closed off atomically." 
-  (save-excursion
-    (set-buffer buffer)
-    (let ((span (make-span (proof-unprocessed-begin) (point-max)))
-	  cmd)
-      ;; compute first command of buffer
-      (goto-char (point-min))
-      (proof-find-next-terminator)
-      (let ((cmd-list (member-if
-		       (lambda (entry) (equal (car entry) 'cmd))
-		       (proof-segment-up-to (point)))))
-	(proof-init-segmentation)
-	(if cmd-list 
-	    (progn
-	      (setq cmd (second (car cmd-list)))
-	      (set-span-property span 'type 'vanilla)
-	      (set-span-property span 'cmd cmd))
-	  ;; If there was no command in the buffer, atomic
-	  ;; span becomes a comment.
-	  (set-span-property span 'type 'comment)))
-      (proof-set-locked-end (point-max))
-      (or (member buffer proof-script-buffer-list)
-	  (setq proof-script-buffer-list
-		(append proof-script-buffer-list (list buffer)))))))
-
-(defun proof-file-truename (filename)
-  "Returns the true name of the file FILENAME or nil."
-  (and filename (file-exists-p filename) (file-truename filename)))
-
-(defun proof-register-possibly-new-processed-file (file)
-  "Register a possibly new FILE as having been processed by the prover."
-  (let* ((cfile (file-truename file))
-	 (buffer (proof-file-to-buffer cfile)))
-    (if (not (member cfile proof-included-files-list))
-	(progn
-	  (setq proof-included-files-list
-		(cons cfile proof-included-files-list))
-	  (or (equal cfile
-		     (file-truename (buffer-file-name
-				     (car proof-script-buffer-list))))
-	      (not buffer)
-	      (proof-mark-buffer-atomic buffer))))))
-
-
-;;; begin messy COMPATIBILITY HACKING for FSFmacs.
-;;; 
-;;; In case Emacs is not aware of the function read-shell-command,
-;;; and read-shell-command-map, we duplicate some code adjusted from
-;;; minibuf.el distributed with XEmacs 20.4.
-;;;
-;;; This code is still required as of FSF Emacs 20.2.
-;;;
-;;; I think bothering with this just to give completion for
-;;; when proof-prog-name-ask-p=t is a big overkill!   - da.
-;;;	
-(defvar read-shell-command-map
-  (let ((map (make-sparse-keymap 'read-shell-command-map)))
-    (if (not (fboundp 'set-keymap-parents))
-        (if (fboundp 'set-keymap-parent)
-	    ;; FSF Emacs 20.2
-	    (set-keymap-parent map minibuffer-local-map)
-	  ;; Earlier FSF Emacs
-	  (setq map (append minibuffer-local-map map))
-	  ;; XEmacs versions?
-	  (set-keymap-parents map minibuffer-local-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.")
-
-(or (fboundp 'read-shell-command)
-    (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)))))
-
-
-;;; end messy COMPATIBILITY HACKING
-
-
-;;
-;; Misc movement functions
-;;
-
-;; FIXME da: these next two functions slightly different, why?
-;; (unprocessed-begin vs proof-locked-end)
-(defun proof-goto-end-of-locked-interactive ()
-  "Jump to the end of the locked region."
-  (interactive)
-  (switch-to-buffer (car proof-script-buffer-list))
-  (goto-char (proof-locked-end)))
-
-(defun proof-goto-end-of-locked ()
-  "Jump to the end of the locked region."
-  (goto-char (proof-unprocessed-begin)))
-
-(defun proof-in-locked-region-p ()
-  "Non-nil if point is in locked region.  Assumes proof script buffer current."
-  (< (point) (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 it."
-  (interactive)
-  (let* ((proof-script-buffer (car proof-script-buffer-list))
-	 (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 ()
-  "Return buffer of active proof assistant, or nil if none running."
-  (and proof-shell-buffer
-       (comint-check-proc proof-shell-buffer)
-       proof-shell-buffer))
-
-(defun proof-start-shell ()
-  "Initialise a shell-like buffer for a proof assistant.
-
-Also generates goal and response buffers.
-Initialises current buffer for scripting.
-Does nothing if proof assistant is already running."
-  (if (proof-shell-live-buffer)
-      ()
-    (run-hooks 'proof-pre-shell-start-hook)
-    (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 "*"))
-	    proof-pbp-buffer (get-buffer-create (concat "*" proc "-goals*"))
-	    proof-response-buffer (get-buffer-create (concat "*" proc
-	    "-response*")))
-
-      (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-list (list (current-buffer)))
-      (proof-init-segmentation)
-      (setq proof-active-buffer-fake-minor-mode t)
-      (run-hooks 'proof-activate-scripting-hook)
-
-      (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)))))
-  
-
-;; Should this be the same as proof-restart-script?
-;; Perhaps this is redundant.
-(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)
-		(mapcar 'proof-detach-segments proof-script-buffer-list)
-	      (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 (member (current-buffer) proof-script-buffer-list) (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 (car proof-script-buffer-list))
-      (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 annotation field start.  A regular expression or nil.
-An eager annotation indicates to Emacs that some following output
-should be displayed immediately and not accumulated for parsing.
-Set to nil if the proof to disable this feature.")
-
-(defvar proof-shell-eager-annotation-end "$"
-  "Eager annotation field end.  A regular expression or nil.
-An eager annotation indicates to Emacs that some following output
-should be displayed immediately and not accumulated for parsing.
-Set to nil if the proof to disable this feature.
-
-The default value is \"$\" to match up to the end of the line.")
-
-(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?
-;; Answer: this is used in *specific* modes, see e.g.
-;; lego-goal-hyp.  This stuff needs making more generic.
-(defvar proof-shell-goal-regexp nil
-  "A regular expression 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 da: 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-shell-proof-completed nil
-  "Flag indicating that a completed proof has just been observed.")
-
-(defvar proof-analyse-using-stack nil
-  "Are annotations sent by proof assistant local or global")
-
-(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-output (start-regexp end-regexp append-face)
-  "Pretty print output in process buffer in specified region.
-The region begins with the match for START-REGEXP and is delimited by
-END-REGEXP. The match for END-REGEXP is not part of the specified region.
-Removes any annotations in the region.
-Fontifies the region.
-Appends APPEND-FACE to the text property of the region .
-Returns the string (with faces) in the specified region."
-  (let (start end string)
-    (save-excursion
-      (set-buffer proof-shell-buffer)
-      (goto-char (point-max))
-      (setq start (search-backward-regexp start-regexp))
-      (save-excursion (setq end (- (search-forward-regexp end-regexp)
-				   (length (match-string 0)))))
-      (setq string
-	    (proof-shell-strip-annotations (buffer-substring start end)))
-      (delete-region start end)
-      (insert string)
-      (setq end (+ start (length string)))
-      ;; This doesn't work with FSF Emacs 20.2's version of Font-lock
-      ;; because there are no known keywords in the process buffer
-      ;; Never mind. In a forthcoming version, the process buffer will
-      ;; not be tempered with. Fontification will take place in a
-      ;; separate response buffer.
-      ;; (font-lock-fontify-region start end)
-      (font-lock-append-text-property start end 'face append-face)
-      (buffer-substring start end))))
-
-(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")))
-
-
-;; Notes on markup in the scripting buffer. (da)
-;;
-;; The locked region is covered by a collection of non-overlaping
-;; spans (our abstraction of extents/overlays).
-;;
-;; For an unfinished proof, there is one extent for each command 
-;; or comment outside a command.   For a finished proof, there
-;; is one extent for the whole proof.
-;;
-;; Each command span has a 'type property, one of:
-;;
-;;     'vanilla      Initialised in proof-semis-to-vanillas, for
-;;     'goalsave 
-;;     'comment      A comment outside a command.
-;;
-;;  All spans except those of type 'comment have a 'cmd property,
-;;  which is set to a string of its command.  This is the
-;;  text in the buffer stripped of leading whitespace and any comments.
-;;
-;; 
-
-(defun proof-shell-handle-error (cmd string)
-  "React on an error message triggered by the prover.
-We display the process buffer, scroll to the end, beep and fontify the
-error message. At the end it calls `proof-shell-handle-error-hook'. "
-    ;; We extract all text between text matching
-    ;; `proof-shell-error-regexp' and the following prompt.
-    ;; Alternatively one could higlight all output between the
-    ;; previous and the current prompt.
-    ;; +/- of our approach
-    ;; + Previous not so relevent output is not highlighted
-    ;; - Proof systems have to conform to error messages whose start  can be
-    ;;   detected by a regular expression.
-  (proof-shell-handle-output
-   proof-shell-error-regexp proof-shell-annotated-prompt-regexp
-   'font-lock-error-face)
-  (save-excursion (display-buffer proof-shell-buffer)
-		  (beep)
-
-		  ;; unwind script buffer
-		  (set-buffer (car proof-script-buffer-list))
-		  (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 (car proof-script-buffer-list)))
-  (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)
-  "Process shell output by matching on STRING.
-This function 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'.
-
-This 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-proof-completed t)
-    (setq proof-shell-delayed-output
-	  (cons 'insert (concat "\n" (match-string 0 string)))))
-
-   ((string-match proof-shell-start-goals-regexp string)
-    (setq proof-shell-proof-completed nil)
-    (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)
-    (setq proof-shell-proof-completed nil)
-    (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                     ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; FIXME da: Should this kind of ordinary input go onto the queue of
-;; things to do?  Then errors during processing would prevent it being
-;; sent.  Also the proof shell lock would be set automatically, which
-;; might be nice?
-(defun proof-shell-insert (string)
-  (save-excursion
-    (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))))
-
-;; da: This function strips carriage returns from string, then
-;; sends it.  (Why strip CRs?)
-(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)))
-
-(defun proof-check-process-available (&optional relaxed)
-  "Adjust internal variables for scripting of current buffer.
-
-Signals an error if current buffer is not a proof script or if the
-proof process is not idle. If RELAXED is set, nothing more is done. No
-changes are necessary if the current buffer is already in Scripting
-minor mode. Otherwise, the current buffer will become the current
-scripting buffer provided the current scripting buffer has either no
-locked region or everything in it has been processed."
-  (proof-start-shell)
-  (cond
-   ((not (or relaxed (eq proof-buffer-type 'script)))
-    (error "Must be running in a script buffer"))
-   (proof-shell-busy (error "Proof Process Busy!"))
-   (relaxed ())			;exit cond
-
-   ;; No buffer is in Scripting minor mode.
-   ;; We assume the setup is done somewhere else
-   ;; so this should never happen
-   ((null proof-script-buffer-list) (assert nil))
-
-   ;; The current buffer is in Scripting minor mode
-   ;; so there's nothing to do
-   ((equal (current-buffer) (car proof-script-buffer-list)))
-
-   (t
-    (let ((script-buffer (car proof-script-buffer-list))
-	  (current-buffer (current-buffer)))
-      (save-excursion
-	(set-buffer script-buffer)
-	;; We only allow switching of the Scripting buffer if the
-	;; locked region is either empty or full for all buffers.
-	;; Here we check the current Scripting buffer's status.
-	(let
-	    ((locked-is-empty (eq (proof-unprocessed-begin) (point-min)))
-	     (locked-is-full  (progn
-				(goto-char (point-max))
-				(skip-chars-backward " \t\n")
-				(>= (proof-unprocessed-begin) (point)))))
-	  (if locked-is-full
-	      ;; We're switching from a buffer which has been
-	      ;; completely processed.  Make sure that it's
-	      ;; registered on the included files list, in
-	      ;; case it has been processed piecemeal.
-	      (if buffer-file-name
-		  (proof-register-possibly-new-processed-file 
-		   buffer-file-name)))
-
-	  (if (or locked-is-full locked-is-empty)
-	      ;; we are changing the scripting buffer
-	      (progn
-		(setq proof-active-buffer-fake-minor-mode nil)
-		(set-buffer current-buffer)
-
-		;; does the current buffer contain locked regions already?
-		(if (member current-buffer proof-script-buffer-list)
-		    (setq proof-script-buffer-list
-			  (remove current-buffer proof-script-buffer-list))
-		  (proof-init-segmentation))
-		(setq proof-script-buffer-list
-		      (cons current-buffer proof-script-buffer-list))
-		(setq proof-active-buffer-fake-minor-mode t)
-		(run-hooks 'proof-activate-scripting-hook))
-	    ;; Locked region covers only part of the buffer
-	    ;; FIXME da: ponder alternative of trying to complete rest
-	    ;; of current scripting buffer?
-	    (error "Cannot deal with two unfinished script buffers!"))))))))
-
-
-(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 in proof-release-lock: Proof process not busy")
-	    (message "Nag, nag, nag: proof-release-lock: Proof process not busy"))
-	(if (not (member (current-buffer) proof-script-buffer-list))
-	    (error "Bug in proof-release-lock: 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))) 
-		       proof-no-command))
-    (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
-
-
-;; 
-;; 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.
-
-(defun proof-shell-exec-loop () 
-"Process the proof-action-list.
-proof-action-list contains a list of (span,command,action) triples.
-This function is called with a non-empty proof-action-list, where the
-head of the list is the previously executed command which succeeded.
-We execute (action span) on the first item, then (action span) on
-following items which have proof-no-command as their cmd components.
-Return non-nil if the action list becomes empty; unlock the process
-and removes the queue region.  Otherwise send the next command to the
-proof process."
-  (save-excursion
-    (set-buffer (car proof-script-buffer-list))
-    ;; (if (null proof-action-list) 
-    ;;	(error "proof-shell-exec-loop: called with empty proof-action-list."))
-    ;; Be more relaxed about calls with empty action list
-    (if proof-action-list
-	(let ((item (car proof-action-list)))
-	  ;; Do (action span) on first item in list
-	  (funcall (nth 2 item) (car item))
-	  (setq proof-action-list (cdr proof-action-list))
-	  ;; Process following items in list with the form
-	  ;; ("COMMENT" cmd) by calling (cmd "COMMENT")
-	  (while (and proof-action-list
-		      (string= 
-		       (nth 1 (setq item (car proof-action-list))) 
-		       proof-no-command))
-	    ;; Do (action span) on comments
-	    (funcall (nth 2 item) (car item))
-	    (setq proof-action-list (cdr proof-action-list)))
-	  ;; If action list is empty now, release the process lock
-	  (if (null proof-action-list)
-	      (progn (proof-release-lock)
-		     (proof-detach-queue)
-		     ;; indicate finished
-		     t)
-	    ;; Send the next command to the process
-	    (proof-send (nth 1 item))
-	    ;; indicate not finished
-	    nil))
-      ;; Just indicate finished if called with empty proof-action-list.
-      t)))
-
-(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 (car proof-script-buffer-list))
-    (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.
-
-;; FIXME: highlight eager annotation-end : fix proof-shell-handle-output
-;; to highlight whole string.
-(defun proof-shell-popup-eager-annotation ()
-  "Process urgent messages.
-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 ((str (proof-shell-handle-output
-	      proof-shell-eager-annotation-start
-	      proof-shell-eager-annotation-end
-	      'font-lock-eager-annotation-face))
-	file module)
-    (proof-message str)))
-
-(defun proof-response-buffer-display (str face)
-  "Display STR with FACE in response buffer."
-  (let ((start))
-    (save-excursion
-      (set-buffer proof-response-buffer)
-      (setq start (goto-char (point-max)))
-      (insert str)
-      (font-lock-fontify-region start (point-max))
-      (font-lock-append-text-property start (point-max) 'face face)
-      (insert "\n"))))
-
-(defun proof-file-to-buffer (filename)
-  "Converts a FILENAME  into a buffer name"
-  (let* ((buffers (buffer-list))
-	 (pos
-	  (position (file-truename filename)
-		    (mapcar 'proof-file-truename
-			    (mapcar 'buffer-file-name
-				    buffers))
-		    :test 'equal)))
-    (and pos (nth pos buffers))))
-
-(defun proof-files-to-buffers (filenames)
-  "Converts a list of FILENAMES into a list of BUFFERS."
-  (if (null filenames) nil
-    (let* ((buffer (proof-file-to-buffer (car filenames)))
-	  (rest (proof-files-to-buffers (cdr filenames))))
-      (if buffer (cons buffer rest) rest))))
-	  
-		  
-(defun proof-shell-process-urgent-message (message)
-  "Display and analyse urgent MESSAGE for asserting or retracting files."
-  
-  ;; Is the prover processing a file?
-  (cond ((and proof-shell-process-file 
-	      (string-match (car proof-shell-process-file) message))
-	 (let
-	     ((file (funcall (cdr proof-shell-process-file) message)))
-	   (if (string= file "") 
-	       (setq file (buffer-file-name (car proof-script-buffer-list))))
-	   (if file
-	       (proof-register-possibly-new-processed-file file))))
-
-  ;; Is the prover retracting across files?
-	((and proof-shell-retract-files-regexp
-	      (string-match proof-shell-retract-files-regexp message))
-	 (let ((current-included proof-included-files-list))
-	   (setq proof-included-files-list
-		 (funcall proof-shell-compute-new-files-list message))
-	   (proof-restart-buffers
-	    (remove (car proof-script-buffer-list)
-		    (proof-files-to-buffers
-		     (set-difference current-included
-				     proof-included-files-list))))))
-	(t
-	 (proof-message message)
-	 (proof-response-buffer-display message
-					'font-lock-eager-annotation-face))))
-
-(defun proof-shell-process-urgent-messages (str)
-  "Scan the process output for urgent messages.
-Display them immediately in the Response buffer.
-Keep `proof-included-files-list' up to date.
-The input STR is the most recent chunk of output sent to the process
-filter. We assume that urgent messages are fully contained in STR."
-  (let ((start (string-match proof-shell-eager-annotation-start str))
-	end)
-    (and start
-	 (setq end
-	       (string-match proof-shell-eager-annotation-end str
-	       start))
-	 (progn
-	   (proof-shell-process-urgent-message
-	    (proof-shell-strip-annotations (substring str start end)))
-	   (proof-shell-process-urgent-messages (substring str end))))))
-
-(defun proof-shell-filter (str) 
-  "Filter for the proof assistant 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."
-  (and proof-shell-eager-annotation-start
-       (proof-shell-process-urgent-messages str)) 
-       
-  (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 annotated 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)
-	    (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?
-	  (setq cmd (nth 1 (car proof-action-list)))
-	  (save-excursion
-	    ;; 
-	    (setq res (proof-shell-process-output cmd string))
-	    ;; da: Added this next line to redisplay, for proof-toolbar
-	    ;; FIXME: should do this for all frames displaying the script
-	    ;; buffer!
-	    ;; ODDITY: has strange effect on highlighting, leave it.
-	    ;; (redisplay-frame (window-buffer  t)
-	    (cond
-	     ((eq (car-safe res) 'error)
-	      (proof-shell-handle-error cmd (cdr res)))
-	     ((eq res 'interrupt)
-	      (proof-shell-handle-interrupt))
-	     ((eq (car-safe 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)))
-    
-(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                                       ;;
-
-
-(defun proof-check-atomic-sequents-lists (span cmd end)
-  "Check if CMD is the final command in an ACS.
-
-If CMD is matched by the end regexp in `proof-atomic-sequents-list',
-the ACS is marked in the current buffer. If CMD does not match any,
-`nil' is returned, otherwise non-nil."
-  ;;FIXME tms: needs implementation
-  nil)
-
-(defun proof-done-advancing (span)
-  "The callback function for assert-until-point."
-  (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))
-     ((proof-check-atomic-sequents-lists span cmd end))
-     ((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)
-
-      (and proof-lift-global
-	   (funcall proof-lift-global gspan)))
-     (t
-      (set-span-property span 'mouse-face 'highlight)
-      (and proof-global-p 
-	   (funcall proof-global-p cmd)
-	   proof-lift-global
-	   (funcall proof-lift-global span))))))
-
-
-
-;; FIXME da: Below it would probably be faster to use the primitive
-;; skip-chars-forward rather than scanning character-by-character 
-;; with a lisp loop over the whole region. Also I'm not convinced that
-;; Emacs should be better at skipping whitespace and comments than the
-;; proof process itself!
-
-(defun proof-segment-up-to (pos &optional next-command-end)
-  "Create a list of (type,int,string) tuples from end of locked region to POS.
-Each tuple denotes 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.
-If optional NEXT-COMMAND-END is non-nil, we contine past POS until
-the next command end."
-  (save-excursion
-      ;; 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
-    (let ((str (make-string (- (buffer-size)
-			       (proof-unprocessed-begin) -10) ?x))
-	  (i 0) (depth 0) (quote-parity t) done alist c)
-     (proof-goto-end-of-locked)
-     (while (not done)
-       (cond
-	;; Case 1. We've reached POS, not allowed to go past it,
-	;; and are inside a comment
-	((and (not next-command-end) (= (point) pos) (> depth 0))
-	 (setq done t alist (cons 'unclosed-comment alist)))
-	;; Case 2. We've reached the end of the buffer while
-	;; scanning inside a comment or string
-	((= (point) (point-max))
-	 (cond
-	  ((not quote-parity)
-	   (message "Warning: unclosed quote"))
-	  ((> depth 0)
-	   (setq done t alist (cons 'unclosed-comment alist))))
-	 (setq done t))
-	;; Case 3. Found a comment end, not inside a string
-	((and (looking-at (regexp-quote proof-comment-end)) quote-parity)
-	 (if (= depth 0) 
-	     (progn
-	       (message "Warning: extraneous comment end")
-	       (setq done t))
-	   (setq depth (- depth 1))
-	   (forward-char (length proof-comment-end))
-	   (if (eq i 0) 
-	       (setq alist (cons (list 'comment "" (point)) alist))
-	     (aset str i ?\ )
-	     (incf i))))
-	;; Case 4. Found a comment start, not inside a string
-	((and (looking-at (regexp-quote proof-comment-start)) quote-parity)
-	 (setq depth (+ depth 1))
-	 (forward-char (length proof-comment-start)))
-	;; Case 5. Inside a comment. 
-	((> depth 0)
-	 (forward-char))
-	;; Case 6. Anything else
-	(t
-	 ;; Skip whitespace before the start of a command, otherwise
-	 ;; other characters in the accumulator string str
-	 (setq c (char-after (point)))
-	 (if (or (> i 0) (not (= (char-syntax c) ?\ )))
-	     (progn
-	       (aset str i c)
-	       (incf i)))
-	 
-	 (if (looking-at "\"")	; FIXME da: should this be more generic?
-	     (setq quote-parity (not quote-parity)))
-	 
-	 (forward-char)
-
-	 ;; Found the end of a command
-	 (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-unprocessed-begin)) 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 proof-no-command 'proof-done-advancing) alist)))
-	(setq semis (cdr semis)))
-    (nreverse alist)))
-
-;;
-;; Two commands for moving forwards in proof scripts.
-;; Moving forward for a "new" command may insert spaces
-;; or new lines.  Moving forward for the "next" command
-;; does not.
-;;
-
-(defun proof-script-new-command-advance ()
-  "Move point to a nice position for a new command.
-Assumes that point is at the end of a command."
-  (interactive)
-  (if proof-one-command-per-line
-      ;; One command per line: move to next new line,
-      ;; creating one if at end of buffer or at the
-      ;; start of a blank line.  (This has the pleasing
-      ;; effect that blank regions of the buffer are
-      ;; automatically extended when inserting new commands).
-      (cond
-       ((eq (forward-line) 1)
-	(newline))
-       ((eolp)
-        (newline)
-	(forward-line -1)))
-    ;; Multiple commands per line: skip spaces at point,
-    ;; and insert the same number of spaces that were
-    ;; skipped in front of point (at least one).
-    ;; This has the pleasing effect that the spacing
-    ;; policy of the current line is copied: e.g.
-    ;;   <command>;  <command>;
-    ;; Tab columns don't work properly, however.
-    ;; Instead of proof-one-command-per-line we could
-    ;; introduce a "proof-command-separator" to improve
-    ;; this.
-    (let ((newspace (max (skip-chars-forward " \t") 1))
-	  (p (point)))
-	(insert-char ?\ newspace)
-	(goto-char p))))
-
-(defun proof-script-next-command-advance ()
-  "Move point to the beginning of the next command if it's nearby.
-Assumes that point is at the end of a command."
-  (interactive)
-  ;; skip whitespace on this line
-  (skip-chars-forward " \t")		
-  (if (and proof-one-command-per-line (eolp))
-      ;; go to the next line if we have one command per line
-      (forward-line)))
-
-
-
-; 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.
-
-;; FIXME da: this command doesn't behave as the doc string says when
-;; inside comments.  Also is unhelpful at the start of commands, and
-;; in the locked region.  I prefer the new version below.
-
-(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-check-process-available)))
-	semis)
-    (save-excursion
-      (if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t))
-	  (progn (goto-char pt)
-		 (error "I don't know what I should be doing in this buffer!")))
-      (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 "I don't know what I should be doing in this buffer!"))
-      (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-unprocessed-begin) (point) vanillas))))))
-
-
-;; da: This is my alternative version of the above.
-;; It works from the locked region too.
-;; I find it more convenient to assert up to the current command (command
-;; point is inside), and move to the next command.
-;; This means proofs can be easily replayed with point at the start
-;; of lines.  Above function gives stupid "nothing to do error." when
-;; point is on the start of line or in the locked region.
-
-;; FIXME: behaviour inside comments may be odd at the moment.  (it
-;; doesn't behave as docstring suggests, same prob as
-;; proof-assert-until-point)
-;; FIXME: polish the undo behaviour and quit behaviour of this
-;; command (should inhibit quit somewhere or other).
-
-(defun proof-assert-next-command
-  (&optional unclosed-comment-fun ignore-proof-process-p
-	     dont-move-forward for-new-command)
-  "Process until the end of the next unprocessed command after point.
-If inside a comment, just to go 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.
-Afterwards, move forward to near the next command afterwards, unless
-DONT-MOVE-FORWARD is non-nil.  If FOR-NEW-COMMAND is non-nil,
-a space or newline will be inserted automatically."
-  (interactive)
-  (let ((pt (point))
-	(crowbar (or ignore-proof-process-p (proof-check-process-available)))
-	semis)
-    (save-excursion
-      ;; CHANGE from old proof-assert-until-point: don't bother check
-      ;; for non-whitespace between locked region and point.
-      ;; CHANGE: ask proof-segment-up-to to scan until command end
-      ;; (which it used to do anyway, except in the case of a comment)
-      (setq semis (proof-segment-up-to (point) t)))
-    ;; old code:
-    ;;(if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t))
-    ;;	  (progn (goto-char pt)
-    ;;       (error "I don't know what I should be doing in this buffer!")))
-    ;; (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))
-	  ;; CHANGE: if inside a comment, do as the documentation
-	  ;; suggests.
-	  (setq semis nil))
-      (if (and (not ignore-proof-process-p) (not crowbar) (null semis))
-	  (error "I don't know what I should be doing in this buffer!"))
-      (goto-char (nth 2 (car semis)))
-      (if (not ignore-proof-process-p)
-	   (let ((vanillas (proof-semis-to-vanillas (nreverse semis))))
-;	     (if crowbar (setq vanillas (cons crowbar vanillas)))
-	     (proof-start-queue (proof-unprocessed-begin) (point) vanillas)))
-      ;; This is done after the queuing to be polite: it means the
-      ;; spacing policy enforced here is not put into the locked
-      ;; region so the user can re-edit.
-      (if (not dont-move-forward)
-	   (if for-new-command
-	       (proof-script-new-command-advance)
-	     (proof-script-next-command-advance))))))
-
-;;         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-unprocessed-begin) (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) proof-no-command
-			       (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)))
-
-;; FIXME da:  I would rather that this function moved point to
-;; the start of the region retracted?
-
-(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-check-process-available))
-    (save-excursion
-      (if (not (re-search-backward "\\S-" (proof-locked-end) t))
-	  (progn (goto-char pt)
-		 (error "I don't know what I should be doing in this buffer!")))
-      (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 "I don't know what I should be doing in this buffer!"))
-      (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-unprocessed-begin) (point) vanillas)))))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;         misc other user functions                                ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-
-(defun proof-undo-last-successful-command (&optional no-delete)
-  "Undo last successful command at end of locked region.
-Unless optional NO-DELETE is set, the text is also deleted from
-the proof script."
-  (interactive "p")
-  (let ((lastspan (span-at-before (proof-locked-end) 'type)))
-    (if lastspan
-	(progn
-	  (goto-char (span-start lastspan))
-	  (proof-retract-until-point (not no-delete)))
-      (error "Nothing to undo!"))))
-
-(defun proof-interrupt-process ()
-  (interactive)
-  (if (not (proof-shell-live-buffer))
-      (error "Proof Process Not Started!"))
-  (if (not (member (current-buffer) proof-script-buffer-list))
-      (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-goto-command-start ()
-  "Move point to start of current command."
-  (interactive)
-  (let ((cmd (span-at (point) 'type)))
-    (if cmd (goto-char (span-start cmd)) ; BUG: only works for unclosed proofs.
-      (let ((semis (proof-segment-up-to (point) t)))
-	(if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis)))
-	(if (and semis (car semis) (car (car semis)))
-	    (progn
-	      (goto-char (nth 2 (car (car semis))))
-	      (skip-chars-forward " \t\n")))))))
-
-(defun proof-process-buffer ()
-  "Process the current buffer and set point at the end of the buffer."
-  (interactive)
-  (goto-char (point-max))
-  (proof-assert-until-point))
-
-(defun proof-restart-buffer (buffer)
-  "Remove all extents in BUFFER and update `proof-script-buffer-list'."
-  (save-excursion
-    (if (buffer-live-p buffer)
-	(progn
-	  (set-buffer buffer)
-	  (setq proof-active-buffer-fake-minor-mode nil)
-	  (delete-spans (point-min) (point-max) 'type)
-	  (proof-detach-segments)))
-    (setq proof-script-buffer-list
-	  (remove buffer proof-script-buffer-list))))
-
-(defun proof-restart-buffers (bufferlist)
-  "Remove all extents in BUFFERLIST and update `proof-script-buffer-list'."
-  (mapcar 'proof-restart-buffer bufferlist))
-  
-;; For when things go horribly wrong
-;; FIXME: this needs to politely stop the process by sending
-;; an EOF or customizable command.  (maybe timeout waiting for
-;; it to die before killing the buffer)
-;; maybe better:
-;;  Put a funciton to remove all extents in buffers into
-;; the kill-buffer-hook for the proof shell.  Then this
-;; function just stops the shell nicely (see proof-stop-shell).
-(defun proof-restart-script ()
-  "Restart Proof General.
-Kill off the proof assistant process and remove all markings in the
-script buffers."
-  (interactive)
-  (proof-restart-buffers proof-script-buffer-list)
-  ;; { (equal proof-script-buffer-list nil) }
-   (setq proof-shell-busy nil
-	 proof-included-files-list nil
-	 proof-shell-proof-completed 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))
-   (and (buffer-live-p proof-response-buffer)
-	(kill-buffer proof-response-buffer)))
-
-;; For when things go not-quite-so-horribly wrong
-;; FIXME: this may need work, and maybe isn't needed at
-;; all (proof-retract-file when it appears may be enough).
-(defun proof-restart-script-same-process ()
-  (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)))))
-
-;; 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 (member (current-buffer) proof-script-buffer-list))
-    (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
-  "History of proof commands 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)))
-
-;; da: below functions for input history simulation are quick hacks.
-;; Could certainly be made more efficient.
-
-(defvar proof-command-history nil
-  "History used by proof-previous-matching-command and friends.")
-
-(defun proof-build-command-history ()
-  "Construct proof-command-history from script buffer.
-Based on position of point."
-  ;; let
-  )
-
-(defun proof-previous-matching-command (arg)
-  "Search through previous commands for new command matching current input."
-  (interactive))
-  ;;(if (not (memq last-command '(proof-previous-matching-command
-  ;; proof-next-matching-command)))
-      ;; Start a new search
-      
-  
-
-(defun proof-next-matching-command (arg)
-  "Search through following commands for new command matching current input."
-  (interactive "p")
-  (proof-previous-matching-command (- arg)))
-	  
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;; Popup and Pulldown Menu ;;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;;; Menu commands for the underlying proof assistant
-
-;;; These are defcustom'd so that users may re-configure
-;;; the system to their liking.
-(defcustom proof-ctxt-string ""
-  "*Command to display the context in proof assistant."
-  :type 'string
-  :group 'proof)
-
-(defcustom proof-help-string ""
-  "*Command to ask for help in proof assistant."
-  :type 'string
-  :group 'proof)
-
-(defcustom proof-prf-string ""
-  "Command to display proof state in proof assistant."
-  :type 'string
-  :group 'proof)
-
-(defvar proof-goal-command nil
-  "Command to set a goal in the proof assistant.  String or fn.
-If a string, the format character %s will be replaced by the
-goal string. If a function, should return a command string to
-insert when called interactively.")
-
-(defvar proof-save-command nil
-  "Command to save a proved theorem in the proof assistant.  String or fn.
-If a string, the format character %s will be replaced by the
-theorem name. If a function, should return a command string to
-insert when called interactively.")
-
-;;; Functions using the above 
-
-(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)))
-
-
-
-;; FIXME: da: add more general function for inserting into the
-;; script buffer and the proof process together, and using
-;; a choice of minibuffer prompting (hated by power users, perfect
-;; for novices).
-;; Add named goals.
-;; TODO:
-;;   Add named goals.
-;;   Coherent policy for movement here and elsewhere based on
-;;    proof-one-command-per-line user option.
-;;   Coherent policy for sending to process after writing into
-;;    script buffer.  Could have one without the other.
-;;    For example, may be more easy to edit complex goal string
-;;    first in the script buffer.  Ditto for tactics, etc.
-
-(defvar proof-issue-goal-history nil
-  "History of goals for proof-issue-goal.")
-
-(defun proof-issue-goal (goal-cmd)
-  "Insert a goal command into the script buffer, issue it to prover."
-  (interactive
-   (if proof-goal-command 
-       (if (stringp proof-goal-command)
-	   (list (format proof-goal-command
-			 (read-string "Goal: " ""
-				      proof-issue-goal-history)))
-	 (proof-goal-command))
-     (error
-      "Proof General not configured for goals: set proof-goal-command.")))
-  (let ((proof-one-command-per-line t))   ; Goals always start at a new line
-    (proof-issue-new-command goal-cmd)))
-
-(defvar proof-issue-save-history nil
-  "History of theorem names for proof-issue-save.")
-
-(defun proof-issue-save (thmsave-cmd)
-  "Insert a save theorem command into the script buffer, issue it."
-  (interactive
-   (if proof-save-command
-       (if (stringp proof-save-command)
-	   (list (format proof-save-command
-			 (read-string "Save as: " ""
-				      proof-issue-save-history)))
-	 (proof-save-command))
-     (error
-      "Proof General not configured for save theorem: set proof-save-command.")))
-  (let ((proof-one-command-per-line t))   ; Goals always start at a new line
-    (proof-issue-new-command thmsave-cmd)))
-
-(defun proof-issue-new-command (cmd)
-  "Insert CMD into the script buffer and issue it to the proof assistant.
-If point is in the locked region, move to the end of it first.
-Start up the proof assistant if necessary."
-  ;; FIXME: da: I think we need a (proof-script-switch-to-buffer)
-  ;; function (so there is some control over display).
-  ;; (switch-to-buffer proof-script-buffer)
-  (if (proof-shell-live-buffer)
-      (if (proof-in-locked-region-p)
-	  (proof-goto-end-of-locked-interactive)))
-  (proof-script-new-command-advance)
-  ;; FIXME: fixup behaviour of undo here.  Really want
-  ;; to temporarily disable undo for insertion.
-  ;; (buffer-disable-undo) this trashes whole undo list!
-  (insert cmd)
-  ;; FIXME: could do proof-indent-line here, but let's
-  ;; wait until indentation is fixed.
-  (proof-assert-until-point))
-
-
-
-
-;;; To be called from menu
-(defun proof-info-mode ()
-  "Call info on Proof General."
-  (interactive)
-  (info "ProofGeneral"))
-
-(defun proof-exit ()
-  "Exit Proof-assistant."
-  (interactive)
-  (proof-restart-script))
-
-(defvar proof-help-menu
-  `("Help"
-    [,(concat proof-assistant " web page")
-     (browse-url proof-www-home-page) t]
-    ["Proof General home page"
-     (browse-url proof-general-home-page) t]
-    ["Proof General Info" proof-info-mode t]
-    )
-  "The Help Menu in Script Management.")
-
-(defvar proof-shared-menu
-  (proof-append-element
-   (append
-    (list
-     ["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)])
-    (if proof-tags-support
-	(list
-	 "----"
-	 ["Find definition/declaration" find-tag-other-window t])
-      nil))
-    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 proof command terminator, and assert up to it.
-Fire up proof process if necessary."
-  (let ((mrk (point)) ins incomment)
-    (if (looking-at "\\s-\\|\\'\\|\\w") 
-	(if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t))
-	    (error "I don't know what I should be doing in this buffer!")))
-    (if (not (= (char-after (point)) proof-terminal-char))
-	(progn (forward-char) (insert proof-terminal-string) (setq ins t)))
-    (proof-assert-until-point
-     (function (lambda ()
-		 (setq incomment t)
-		 (if ins (backward-delete-char 1))
-		 (goto-char mrk)
-		 (insert proof-terminal-string))))
-    (or incomment
-	(proof-script-next-command-advance))))
-
-(defun proof-active-terminator ()
-  "Insert the terminator, perhaps sending the command to the assistant.
-If proof-active-terminator-minor-mode is non-nil, the command will be
-sent to the assistant."
-  (interactive)
-  (if proof-active-terminator-minor-mode 
-      (proof-process-active-terminator)
-    (self-insert-command 1)))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Proof General scripting mode configuration			    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-
-;; da: this isn't so nice if a scripting buffer should inherit
-;; from another mode: e.g. for Isabelle, we would like to use
-;; sml-mode.
-;; FIXME: add more doc to the mode below, to give hints on
-;; configuring for new assistants.
-(define-derived-mode proof-mode fundamental-mode 
-  proof-mode-name
-  "Proof General major mode for proof scripts.
-\\{proof-mode-map}
-"
-  (setq proof-buffer-type 'script)
-
-  ;; Has buffer already been processed?
-  (and (member buffer-file-truename proof-included-files-list)
-       (proof-mark-buffer-atomic (current-buffer)))
-
-  (make-local-variable 'kill-buffer-hook)
-  (add-hook 'kill-buffer-hook
-	    (lambda ()
-	      (setq proof-script-buffer-list
-		    (remove (current-buffer) proof-script-buffer-list)))))
-
-;; FIXME: da: could we put these into another keymap already?
-;; FIXME: da: it's offensive to experience users to rebind global stuff
-;;        like meta-tab, this should be removed.
-(defconst proof-universal-keys
-  (append
-   '(([(control c) (control c)] . proof-interrupt-process)
-    ([(control c) (control v)] . proof-execute-minibuffer-cmd))
-   (if proof-tags-support
-       '(([(meta tab)]	       . tag-complete-symbol))
-     nil))
-"List of keybindings which for the script and response buffer. 
-Elements of the list are tuples (k . f) 
-where `k' is a keybinding (vector) and `f' the designated function.")
-
-;; Fixed definitions in proof-mode-map, which don't depend on
-;; prover configuration.
-;;; INDENT HACK: font-lock only recognizes define-key at start of line
-(let ((map proof-mode-map))
-(define-key map [(control c) (control e)] 'proof-find-next-terminator)
-(define-key map [(control c) (control a)] 'proof-goto-command-start)
-(define-key map [(control c) (control n)] 'proof-assert-next-command)
-(define-key map [(control c) (return)]	  'proof-assert-next-command)
-(define-key map [(control c) (control t)] 'proof-try-command)
-(define-key map [(control c) ?u]	  'proof-retract-until-point)
-(define-key map [(control c) (control u)] 'proof-undo-last-successful-command)
-(define-key map [(control c) ?\']	  'proof-goto-end-of-locked-interactive)
-(define-key map [(control button1)]	  'proof-send-span)
-(define-key map [(control c) (control b)] 'proof-process-buffer)
-(define-key map [(control c) (control z)] 'proof-frob-locked-end)
-(define-key map [(control c) (control p)] 'proof-prf)
-(define-key map [(control c) ?c]	  'proof-ctxt)
-(define-key map [(control c) ?h]	  'proof-help)
-(define-key map [(meta p)]		  'proof-previous-matching-command)
-(define-key map [(meta n)]		  'proof-next-matching-command)
-;; FIXME da: this shouldn't need setting, because it works
-;; via indent-line-function which is set below.  Check this.
-(define-key map [tab] 'proof-indent-line)
-(proof-define-keys map proof-universal-keys))
-
-
-
-;; 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 () 
-  "Finish setup of Proof General scripting mode.
-Call this function in the derived mode for the proof assistant to
-finish setup which depends on specific proof assistant configuration."
-  ;; calculate some strings and regexps for searching
-  (setq proof-terminal-string (char-to-string proof-terminal-char))
-
-  ;; FIXME: these are LEGO specific!
-  (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string))
-  (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string))
-
-  ;; FIXME da: I'm not sure we ought to add spaces here, but if
-  ;; we don't, there would be trouble overloading these settings
-  ;; to also use as regexps for finding comments.
-  ;; 
-  (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 'proof-match-find-next-function-name)
-	     fume-find-function-name-method-alist))
-
-  ;; Additional key definitions which depend on configuration for
-  ;; specific proof assistant.
-  (define-key proof-mode-map
-    (vconcat [(control c)] (vector proof-terminal-char))
-    'proof-active-terminator-minor-mode)
-
-  (define-key proof-mode-map (vector proof-terminal-char)
-    'proof-active-terminator)
-
-  (make-local-variable 'indent-line-function)
-  (setq indent-line-function 'proof-indent-line)
-
-  ;; Toolbar
-  (if (featurep 'proof-toolbar)
-      (proof-toolbar-setup))
-
-  ;; Menu
-  (easy-menu-define proof-mode-menu  
-		    proof-mode-map
-		    "Menu used in Proof General scripting mode."
-		    (cons proof-mode-name
-			  (append
-			   (cdr proof-menu)
-			   ;; begin UGLY COMPATIBILTY HACK
-			   ;; older/non-existent customize doesn't have 
-			   ;; this function.  
-			   (if (fboundp 'customize-menu-create)
-			       (list (customize-menu-create 'proof)
-				     (customize-menu-create 'proof-internal
-							    "Internals"))
-			     nil)
-			   ;; end UGLY COMPATIBILTY HACK
-			   )))
-  (easy-menu-add proof-mode-menu proof-mode-map)
-
-  ;; For fontlock
-
-  ;; setting font-lock-defaults explicitly is required by FSF Emacs
-  ;; 20.2's version of font-lock
-  (make-local-variable 'font-lock-defaults)
-  (setq font-lock-defaults '(font-lock-keywords))
-
-  ;; FIXME (da): zap commas support is too specific, should be enabled
-  ;; by each proof assistant as it likes.
-  (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.
-  ;; FIXME (da): setting this to t everywhere is too brutal.  Should
-  ;; probably make it local.
-  (and (boundp 'font-lock-always-fontify-immediately)
-       (setq font-lock-always-fontify-immediately t))
-
-  (run-hooks 'proof-mode-hook))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Proof General shell mode configuration			    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; 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 proof-shell-proof-completed nil)
-  (make-local-variable 'proof-shell-insert-hook)
-
-  ;; comint customisation. comint-prompt-regexp is used by
-  ;; comint-get-old-input, comint-skip-prompt, comint-bol, backward
-  ;; matching input, etc.  
-  (setq comint-prompt-regexp proof-shell-prompt-pattern)
-
-  ;; An article by Helen Lowe in UITP'96 suggests that the user should
-  ;; not see all output produced by the proof process. 
-  (remove-hook 'comint-output-filter-functions
-	       'comint-postoutput-scroll-to-bottom 'local)
-
-  (add-hook 'comint-output-filter-functions 'proof-shell-filter nil 'local)
-  (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 Proof General shell mode."
-		  (cons proof-mode-name (cdr proof-shell-menu)))
-
-(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"))))
+;; Load toolbar code if toolbars available.
+(if (featurep 'toolbar)
+    (require 'proof-toolbar))
 
-(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))
+(require 'proof-script)
+(require 'proof-shell)
 
 
 (provide 'proof)