Doc tweaks via checkdoc.

2 files changed, 201 insertions, 174 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 8252838b..28ec1545 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -7,7 +7,11 @@
 ;;
 ;; $Id$
 ;;
+;;; Commentary:
 ;; 
+;; This implements the main mode for script management, including
+;; parsing script buffers and setting spans inside them.
+;;
 
 ;;; Code:
 
@@ -184,11 +188,12 @@ scripting buffer may have an active queue span.")
 ;; ** Getters and setters
 
 (defun proof-span-give-warning (&rest args)
-  "Give a warning message."
+  "Give a warning message.
+Optional argument ARGS is ignored."
   (message "You should not edit here!"))
 
 (defun proof-span-read-only (span &optional always)
-  "Make SPAN be read-only according to `proof-strict-read-only' or ALWAYS."
+  "Make SPAN be read-only according to variable `proof-strict-read-only' or ALWAYS."
   (if (or always (not (memq proof-strict-read-only '(nil retract))))
       (span-read-only span)
     (span-write-warning span
@@ -197,7 +202,7 @@ scripting buffer may have an active queue span.")
                           'proof-span-give-warning))))
 
 (defun proof-strict-read-only ()
-  "Set locked spans in script buffers according to `proof-strict-read-only'."
+  "Set locked spans in script buffers according to variable `proof-strict-read-only'."
   ;; NB: read-only is synchronized in all script buffers
   (interactive)
   (proof-map-buffers
@@ -226,7 +231,7 @@ scripting buffer may have an active queue span.")
               ;; writable part of the buffer.
               t ;; proof-allow-undo-in-read-only
               )
-    (setq buffer-undo-list 
+    (setq buffer-undo-list
 	  (undo-make-selective-list end (point-max))))
   (span-set-endpoints proof-queue-span start end)))
  (t
@@ -235,8 +240,9 @@ scripting buffer may have an active queue span.")
   (span-set-endpoints proof-queue-span start end))))
 
 (defun proof-set-overlay-arrow (pos)
+  "Set the position of the overlay marker to POS."
   (and (markerp proof-overlay-arrow)
-       (set-marker proof-overlay-arrow 
+       (set-marker proof-overlay-arrow
 		   (save-excursion
 		     (goto-char pos)
 		     (skip-chars-forward " \t\s\n")
@@ -251,12 +257,12 @@ scripting buffer may have an active queue span.")
 
 (defsubst proof-detach-queue ()
   "Remove the span for the queue region."
-  (and proof-queue-span 
+  (and proof-queue-span
        (span-detach proof-queue-span)))
 
 (defsubst proof-detach-locked ()
   "Remove the span for the locked region."
-  (and proof-locked-span 
+  (and proof-locked-span
        (span-detach proof-locked-span))
   (and (markerp proof-overlay-arrow)
        (set-marker proof-overlay-arrow nil)))
@@ -323,6 +329,7 @@ Also clear list of script portions."
 
 ;;;###autoload
 (defun proof-colour-locked ()
+  "Alter the colour of the locked region according to variable `proof-colour-locked'."
   (interactive)
   (proof-map-buffers (proof-buffers-in-mode proof-mode-for-script)
    (and (span-live-p proof-locked-span)
@@ -364,7 +371,7 @@ value of proof-locked span."
 	  (setq bufs-got (cons buf bufs-got))))))
 
 (defun proof-script-remove-all-spans-and-deactivate ()
-  "Remove all spans from scripting buffers via proof-restart-buffers."
+  "Remove all spans from scripting buffers via `proof-restart-buffers'."
   (proof-restart-buffers (proof-script-buffers-with-spans)))
 
 (defun proof-script-clear-queue-spans ()
@@ -378,6 +385,7 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}."
 	(proof-script-delete-spans (proof-locked-end) (point-max)))))
 
 (defun proof-script-delete-spans (beg end)
+  "Delete spans between BEG and END."
   (span-delete-spans beg end 'type)
   (span-delete-spans beg end 'idiom)
   (span-delete-spans beg end 'pghelp))
@@ -401,7 +409,7 @@ The position is actually one beyond the last locked character."
 
 (defun proof-script-end ()
   "Return the character beyond the last non-whitespace character.
-This is the same position proof-locked-end ends up at when asserting
+This is the same position `proof-locked-end' ends up at when asserting
 the script.  Works for any kind of buffer."
   (save-excursion
     (goto-char (point-max))
@@ -454,7 +462,7 @@ Works on any buffer."
   (eq (proof-unprocessed-begin) (point-min)))
 
 (defun proof-only-whitespace-to-locked-region-p ()
-  "Non-nil if only whitespace separates char after point from end of locked region.
+  "Non-nil if only whitespace between point and end of locked region.
 Point should be after the locked region.
 NB: If nil, point is left at first non-whitespace character found.
 If non-nil, point is left where it was."
@@ -507,7 +515,7 @@ Does nothing if there is no active scripting buffer, or if
 	(proof-goto-end-of-locked t))))
 
 (defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window ()
-  "As `proof-goto-end-of-locked-if-pos-not-visible-in-window' except not for interrupts.
+  "As `proof-goto-end-of-locked-if-pos-not-visible-in-window', but not for interrupts.
 Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
   (interactive)
   (cond
@@ -556,7 +564,7 @@ Assumes script buffer is current"
 This is used for cleaning `buffer-invisibility-spec' in
 `pg-clear-script-portions': it doesn't need to be exactly accurate.")
 
-(defconst pg-default-invisibility-spec 
+(defconst pg-default-invisibility-spec
   ;; Default supports X-Symbol, see `x-symbol-hide-revealed-at-point'
   '((t . nil) (hide . nil)))
 
@@ -564,7 +572,7 @@ This is used for cleaning `buffer-invisibility-spec' in
   "Clear record of script portion names and types from internal list.
 Also clear all visibility specifications."
   (setq pg-script-portions nil)
-  (mapcar 'remove-from-invisibility-spec 
+  (mapcar 'remove-from-invisibility-spec
 	  pg-visibility-specs))
 
 (defun pg-add-script-element (elt)
@@ -652,11 +660,11 @@ NAME does not need to be unique."
   (pg-redisplay-for-gnuemacs))
 
 (defun pg-redisplay-for-gnuemacs ()
-  "GNU Emacs requires redisplay for changes in buffer-invisibility-spec."
+  "GNU Emacs requires redisplay for change in `buffer-invisibility-spec'."
   (redraw-frame (selected-frame)))
 
 (defun pg-show-all-portions (idiom &optional hide)
-  "Show or hide all portions of kind IDIOM."
+  "Show or conceal portions of kind IDIOM; if HIDE is non-nil, conceal."
   (interactive
    (list
     (completing-read
@@ -684,7 +692,7 @@ NAME does not need to be unique."
   (pg-show-all-portions "proof" 'hide))
 
 (defun pg-add-proof-element (name span controlspan)
-  "Add a nested span proof element."
+  "Add a span proof element to SPAN with name NAME and parent CONTROLSPAN."
   (let ((proofid   (proof-next-element-id 'proof)))
     (pg-add-element "proof"  proofid span name)
     ;; Set id in controlspan
@@ -740,7 +748,8 @@ NAME does not need to be unique."
 ;;;###autoload
 (defun pg-set-span-helphighlights (span &optional nohighlight)
   "Add a daughter help span for SPAN with help message, highlight, actions.
-We add the last output to the hover display here."
+We add the last output to the hover display here.
+Optional argument NOHIGHLIGHT means do not add highlight mouse face property."
   (let ((helpmsg    (pg-span-name span))
 	(proofstate (pg-last-output-displayform))
 	(newspan    (let ((newstart (save-excursion
@@ -749,7 +758,7 @@ We add the last output to the hover display here."
 				      (point))))
 		      (span-make newstart (span-end span)))))
     (setq helpmsg
-	  (concat (if (> (length proofstate) 2) "" helpmsg) 
+	  (concat (if (> (length proofstate) 2) "" helpmsg)
 		  proofstate))
     (span-set-property newspan 'pghelp t)
     (if pg-show-hints ;; only message in minibuf if hints on
@@ -775,7 +784,7 @@ We add the last output to the hover display here."
 ;; Multiple file handling
 ;;
 (defun proof-complete-buffer-atomic (buffer)
-  "Make sure BUFFER is marked as completely processed, completing with a single step.
+  "Ensure BUFFER marked completely processed, completing with a single step.
 
 If buffer already contains a locked region, only the remainder of the
 buffer is closed off atomically.
@@ -867,6 +876,7 @@ proof assistant and Emacs has a modified buffer visiting the file."
 	     'wait))))))
 
 (defun proof-inform-prover-file-retracted (rfile)
+  "Send a message to the prover to tell it RFILE has been undone."
   (cond
    ((stringp proof-shell-inform-file-retracted-cmd)
     (proof-shell-invisible-command
@@ -875,7 +885,7 @@ proof assistant and Emacs has a modified buffer visiting the file."
      'wait))
    ;; If it's a function it might not actually be informing the prover at all,
    ;; but merely cleans up proof-included-files-list by its own magic.  We
-   ;; do the same thing as in proof-shell.el.  
+   ;; do the same thing as in proof-shell.el.
    ;; FIXME: clean and amalgamate this code.
    ((functionp proof-shell-inform-file-retracted-cmd)
     (let ((current-included proof-included-files-list))
@@ -891,7 +901,7 @@ If `proof-auto-multiple-files' is nil, no action is taken.
 If CFILE does not appear on `proof-included-files-list', no action taken.
 
 Any buffers which are visiting files in `proof-included-files-list'
-before CFILE are retracted using proof-protected-process-or-retract.
+before CFILE are retracted using `proof-protected-process-or-retract'.
 They are retracted in reverse order.
 
 Since the `proof-included-files-list' is examined, we expect scripting
@@ -909,7 +919,7 @@ information.  A warning message is given for these cases, since it
 could cause inconsistency problems.
 
 NB!  Retraction can cause recursive calls of this function.
-This is a subroutine for proof-unregister-buffer-file-name."
+This is a subroutine for `proof-unregister-buffer-file-name'."
   (if proof-auto-multiple-files
       (let ((depfiles (reverse
 		       (cdr-safe
@@ -948,7 +958,7 @@ internal file-management.
 
 If `proof-auto-multiple-files' is non-nil, any buffers on
 `proof-included-files-list' before this one will be automatically
-retracted using proof-auto-retract-dependencies."
+retracted using `proof-auto-retract-dependencies'."
   (if buffer-file-name
       (let ((cfile (file-truename
 		    (or buffer-file-name
@@ -1316,7 +1326,8 @@ With ARG, turn on scripting iff ARG is positive."
 ;; `proof-done-advancing'
 
 (defun proof-done-advancing (span)
-  "The callback function for assert-until-point."
+  "The callback function for assert-until-point.
+Argument SPAN ."
   ;; FIXME da: if the buffer dies, this function breaks horribly.
   (if (not (span-live-p span))
       (proof-debug
@@ -1383,7 +1394,7 @@ With ARG, turn on scripting iff ARG is positive."
 
        ;; CASE 4: A "Require" type of command is seen (Coq).
        ;; 
-       ((and 
+       ((and
 	 proof-shell-require-command-regexp
 	 (proof-string-match proof-shell-require-command-regexp cmd))
 	;; We take additional action dependent on prover
@@ -1411,7 +1422,7 @@ With ARG, turn on scripting iff ARG is positive."
 
 
 (defun proof-done-advancing-comment (span)
-  "A subroutine of `proof-done-advancing'."
+  "A subroutine of `proof-done-advancing'.  Add comment element for SPAN."
   ;; Add an element for a new span, which should span
   ;; the text of the comment.
   ;; FIXME: might be better to use regexps/skip spaces for matching
@@ -1420,7 +1431,7 @@ With ARG, turn on scripting iff ARG is positive."
   ;; 
   (let ((bodyspan  (span-make
 		    (+ (length comment-start) (span-start span))
-		    (- (span-end span) 
+		    (- (span-end span)
 		       (max 1 (length comment-end)))))
 	(id        (proof-next-element-id 'comment)))
     (pg-add-element "comment" id bodyspan)
@@ -1430,7 +1441,7 @@ With ARG, turn on scripting iff ARG is positive."
 
 
 (defun proof-done-advancing-save (span)
-  "A subroutine of `proof-done-advancing'."
+  "A subroutine of `proof-done-advancing'.  Add info for save span SPAN."
   (unless (eq proof-shell-proof-completed 1)
     ;; We expect saves to succeed only for recently completed proofs.
     ;; Give a hint to the proof assistant implementor in case something
@@ -1523,7 +1534,8 @@ With ARG, turn on scripting iff ARG is positive."
 	  (proof-depends-process-dependencies nam gspan)))))
 
 (defun proof-make-goalsave (gspan goalend savestart saveend nam &optional nestedundos)
-  "Make new goal-save span, using GSPAN. Subroutine of `proof-done-advancing-save'."
+  "Make new goal-save span, using GSPAN. Subroutine of `proof-done-advancing-save'.
+Argument GOALEND is the end of the goal;."
   (span-set-end gspan saveend)
   (span-set-property gspan 'type 'goalsave)
   (span-set-property gspan 'idiom 'proof);; links to nested proof element
@@ -2252,13 +2264,13 @@ a space or newline will be inserted automatically."
          (proof-retract-until-point))))
 
 (defun proof-inside-comment (pos)
-  (save-excursion 
+  (save-excursion
     (goto-char pos)
     (eq (proof-buffer-syntactic-context) 'comment)))
 
 (defun proof-goto-point ()
   "Assert or retract to the command at current position.
-Calls proof-assert-until-point or proof-retract-until-point as
+Calls `proof-assert-until-point' or `proof-retract-until-point' as
 appropriate."
   (interactive)
   (if (<= (proof-queue-or-locked-end) (point))
@@ -2292,7 +2304,7 @@ appropriate."
   "Insert CMD into the proof script, execute assert-until-point."
   (proof-with-script-buffer
     (proof-goto-end-of-locked)
-    (insert "\n") ;; could be user opt 
+    (insert "\n") ;; could be user opt
     (insert cmd)
     (proof-assert-until-point)))
 
@@ -2547,7 +2559,7 @@ command."
   ;; Set after change functions
   (proof-script-set-after-change-functions)
 
-  (add-hook 'after-set-visited-file-name-hooks 
+  (add-hook 'after-set-visited-file-name-hooks
 	    'proof-script-set-visited-file-name nil t)
 
   (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t))
@@ -2561,7 +2573,7 @@ command."
 This is a hook function for `after-set-visited-file-name-hooks'.
 
 For some provers, the file from which script commands are being
-processed may be important, and if it is changed with C-x C-w, for
+processed may be important, and if it is changed with \\[write-file], for
 example, we might have to retract the contents or inform the proof
 assistant of the new name.  This should be done by adding
 additional functions to `after-set-visited-file-name-hooks'.
@@ -2590,8 +2602,8 @@ to restore them using `after-set-visited-file-name-hooks'."
 (defun proof-script-kill-buffer-fn ()
   "Value of `kill-buffer-hook' for proof script buffers.
 Clean up before a script buffer is killed.
-If killing the active scripting buffer, run proof-deactivate-scripting-auto.
-Otherwise just do proof-restart-buffers to delete some spans from memory."
+If killing the active scripting buffer, run `proof-deactivate-scripting-auto'.
+Otherwise just do `proof-restart-buffers' to delete some spans from memory."
   ;; Deactivate scripting in the current buffer if need be, forcing
   ;; automatic retraction if the buffer is not fully processed.
   (if (eq (current-buffer) proof-script-buffer)
@@ -2688,7 +2700,7 @@ assistant."
 ;; and function hooks, and so that the other hooks can be functions too.
 
 (defun proof-generic-goal-command-p (span)
-  "Is STR a goal?  Decide by matching with `proof-goal-command-regexp'."
+  "Is SPAN a goal?  Decide by matching with `proof-goal-command-regexp'."
   (proof-string-match-safe proof-goal-command-regexp
 			   (or (span-property span 'cmd) "")))
 
@@ -2702,7 +2714,7 @@ assistant."
   (not (proof-string-match-safe proof-non-undoables-regexp cmd)))
 
 (defun proof-generic-count-undos (span)
-  "Count number of undos in a span, return command needed to undo that far.
+  "Count number of undos in SPAN, return command needed to undo that far.
 Command is set using `proof-undo-n-times-cmd'.
 
 A default value for `proof-count-undos-fn'.
@@ -2915,7 +2927,7 @@ Choice of function depends on configuration setting."
       (and (boundp 'imenu-generic-expression)
 	   imenu-generic-expression)
     (set (make-local-variable 'imenu-generic-expression)
-	 (or 
+	 (or
 	  proof-script-imenu-generic-expression
 	     (delq nil
 	       (list
@@ -2995,7 +3007,7 @@ Choice of function depends on configuration setting."
 ;; A simplistic first attempt: we only cache the last region that was
 ;; parsed.  It would be better to maintain a parse cache for the
 ;; unedited prefix of the buffer.  Also, we may perhaps assume that
-;; extending the parsed region can only possibly affect the last command 
+;; extending the parsed region can only possibly affect the last command
 ;; in the cache but leaves the rest intact.  (NB: in Isabelle/Isar a
 ;; command can be a proper prefix of a longer one and there are no
 ;; explicit terminators).
@@ -3003,7 +3015,7 @@ Choice of function depends on configuration setting."
 (defun proof-segment-up-to-using-cache (pos &rest args)
   "A wrapper for `proof-segment-up-to' which uses a cache to speed things up."
   (let (res pos1)
-    (if (and 
+    (if (and
 	 proof-use-parser-cache ;; safety measure while testing
 	 (setq pos1 (save-excursion (goto-char pos)
 				    (skip-chars-forward " \t\n")
@@ -3033,17 +3045,17 @@ Choice of function depends on configuration setting."
   (let ((semis  (reverse proof-segment-up-to-cache))
 	(start  (proof-queue-or-locked-end))
 	usedsemis semiend)
-    (while semis 
+    (while semis
       (setq semiend (nth 2 (car semis)))
       (if (> semiend start)
 	  (setq usedsemis (cons (car semis) usedsemis)))
-      (setq semis 
+      (setq semis
 	    (if (<= semiend pos) (cdr semis))))
     usedsemis))
 
 (defun proof-script-after-change-function (start end prelength)
   "Value for `after-change-functions' in proof script buffers."
-  (setq proof-last-edited-low-watermark 
+  (setq proof-last-edited-low-watermark
 	(min (or proof-last-edited-low-watermark (point-max))
 	     start))
   (if (and (markerp proof-overlay-arrow)
@@ -3053,7 +3065,8 @@ Choice of function depends on configuration setting."
       (proof-set-overlay-arrow start)))
 
 (defun proof-script-set-after-change-functions ()
-  (add-hook 'after-change-functions 
+  "Set `after-change-functions' for script buffers."
+  (add-hook 'after-change-functions
 	    'proof-script-after-change-function nil t))
   
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 44aae2c8..12dfc738 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1,13 +1,19 @@
 ;;; proof-shell.el --- Proof General shell mode.
 ;;
-;; Copyright (C) 1994-2008 LFCS Edinburgh. 
+;; Copyright (C) 1994-2009 LFCS Edinburgh.
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
+;;; Commentary:
+;; 
+;; Mode for buffer which interacts with proof assistant.
+;; Includes management of a queue of commands waiting to be sent.
+;;
 
+;;; Code:
 (eval-when-compile
   (require 'cl)
   (require 'span)
@@ -15,6 +21,8 @@
   (require 'font-lock)
   (require 'proof-utils))
 
+
+
 (require 'proof-autoloads)
 (require 'pg-response)
 (require 'pg-goals)
@@ -25,15 +33,16 @@
 ;; Internal variables used by proof shell
 ;;
 
-(defvar proof-marker nil 
+(defvar proof-marker nil
   "Marker in proof shell buffer pointing to previous command input.")
 
 (defvar proof-action-list nil
-  "A list of lists of the form
+  "The main queue of things to do, containing spans commands and actions.
+The value is a list of lists of the form
 
-  (SPAN COMMAND ACTION [FLAGS])
+   (SPAN COMMAND ACTION [FLAGS])
 
-which is a queue of things to do.  Flags are set for non-standard
+which is the queue of things to do.  Flags are set for non-standard
 commands (out of script).  They may include
 
   'no-response-display   do not display messages in *response* buffer
@@ -69,13 +78,13 @@ Specifically:
  'systemspecific Something specific to a particular system,
 		  -- see `proof-shell-classify-output-system-specific'
 
-The output corresponding to this will be in proof-shell-last-output.
+The output corresponding to this will be in `proof-shell-last-output'.
 
 See also `proof-shell-proof-completed' for further information about
 the proof process output, when ends of proofs are spotted.
 
 This variable can be used for instance specific functions which want
-to examine proof-shell-last-output.")
+to examine `proof-shell-last-output'.")
 
 (defvar proof-shell-delayed-output ""
   "A copy of `proof-shell-last-output' held back for processing at end of queue.")
@@ -104,7 +113,7 @@ of the queue region."
     (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist)
   (setq minor-mode-alist
 	(append minor-mode-alist
-		(list 
+		(list
 		 (list
 		  'proof-active-buffer-fake-minor-mode
 		  proof-shell-active-scripting-indicator)))))
@@ -119,14 +128,14 @@ of the queue region."
 ;; code is single-threaded, a loop parsing process output cannot get
 ;; pre-empted by the user trying to send more input to the process,
 ;; or by the process filter trying to deal with more output.
-;; (Moreover, we can tell when the process is busy because the 
+;; (Moreover, we can tell when the process is busy because the
 ;; queue is non-empty).
 ;;
 
 ;;
 ;; We have two functions:
 ;;
-;;  proof-shell-ready-prover   
+;;  proof-shell-ready-prover
 ;;    starts proof shell, gives error if it's busy.
 ;;
 ;;  proof-activate-scripting  (in proof-script.el)
@@ -151,7 +160,7 @@ No change to current buffer or point."
   (proof-shell-start)
   (unless (or (not proof-shell-busy)
 	      (eq queuemode proof-shell-busy)
-	      (and (listp queuemode) 
+	      (and (listp queuemode)
 		   (member proof-shell-busy queuemode)))
     (error "Proof Process Busy!")))
 
@@ -164,7 +173,7 @@ No change to current buffer or point."
 
 ;;;###autoload
 (defun proof-shell-available-p ()
-  "Returns non-nil if there is a proof shell active and available.
+  "Return non-nil if there is a proof shell active and available.
 No error messages.  Useful as menu or toolbar enabler."
   (and (proof-shell-live-buffer)
        (not proof-shell-busy)))
@@ -194,10 +203,10 @@ to err-or-int."
 
 
 ;;
-;;  Starting and stopping the proof shell  
+;;  Starting and stopping the proof shell
 ;;
 
-(defcustom proof-shell-fiddle-frames t 
+(defcustom proof-shell-fiddle-frames t
   "Non-nil if proof-shell functions should fire-up/delete frames.
 NB: this is a temporary config variable, it will be removed at some point!"
   :type 'boolean
@@ -207,7 +216,7 @@ NB: this is a temporary config variable, it will be removed at some point!"
   "Adjust representation for the current buffer to match `proof-shell-unicode'."
   (if proof-shell-unicode
       nil ;; leave at default for now; new Emacsen OK
-    (and 
+    (and
      ;; On GNU Emacs, prevent interpretation of multi-byte characters.
      ;; If not done, chars 128-255 get remapped higher, breaking regexps
      (fboundp 'toggle-enable-multibyte-characters)
@@ -244,19 +253,19 @@ Does nothing if proof assistant is already running."
 		;; Otherwise, cut prog name on spaces
 		(split-string proof-prog-name)))
 	     (prog-name-list
-	      ;; Splice in proof-rsh-command if it's non-nil 
+	      ;; Splice in proof-rsh-command if it's non-nil
 	      (if (and proof-rsh-command
 		       (> (length proof-rsh-command) 0))
 		  (append (split-string proof-rsh-command)
 			  prog-name-list1)
 		prog-name-list1))
-	     (prog-command-line 
+	     (prog-command-line
 	      (proof-splice-separator " " prog-name-list))
 
 	     (process-connection-type
 	      proof-shell-process-connection-type)
 
-	     ;; Adjust the LANG variable to remove UTF-8 encoding 
+	     ;; Adjust the LANG variable to remove UTF-8 encoding
 	     ;; if not wanted; it conflicts with using chars 128-255 for markup
 	     ;; and results in blocking in C libraries.
 	    (process-environment
@@ -264,7 +273,7 @@ Does nothing if proof assistant is already running."
 		     (if proof-shell-unicode           ;; if specials not used,
 			 process-environment	       ;; leave it alone
 		       (cons
-			(if (getenv "LANG")            
+			(if (getenv "LANG")
 			    (format "LANG=%s"
 				    (replace-in-string (getenv "LANG")
 						       "\\.UTF-8" ""))
@@ -280,9 +289,9 @@ Does nothing if proof assistant is already running."
 	    ;; unibyte below.
 	    ;;
 	    ;; Update: there are problems here with systems where
-	    ;;  i) coding-system-for-read/write is not available 
+	    ;;  i) coding-system-for-read/write is not available
 	    ;;  (e.g. MacOS XEmacs non-mule)
-	    ;; ii) 'rawtext can give wrong behaviour anyway 
+	    ;; ii) 'rawtext can give wrong behaviour anyway
 	    ;;     (e.g. Mac OS GNU Emacs, maybe Windows)
 	    ;;     probably because of line-feed conversion.
 	    ;;
@@ -292,13 +301,13 @@ Does nothing if proof assistant is already running."
 	    (normal-coding-system-for-read (and (boundp 'coding-system-for-read)
 						coding-system-for-read))
 	    (coding-system-for-read
-	     (if proof-shell-unicode 
+	     (if proof-shell-unicode
 		 (or (condition-case nil
 			 (check-coding-system 'utf-8)
 		       (error nil))
 		     normal-coding-system-for-read)
 
-	       (if (string-match "Linux" 
+	       (if (string-match "Linux"
 				 (shell-command-to-string "uname"))
 		   'raw-text
 		 normal-coding-system-for-read)))
@@ -306,7 +315,7 @@ Does nothing if proof assistant is already running."
 	    (coding-system-for-write coding-system-for-read))
 
 	;; PG 3.7: there is now yet another way to influence this:
-	;; (unless 
+	;; (unless
 	;;    (assoc (concat proof-prog-name " .*") process-coding-system-alist)
 	;;  (setq process-coding-system-alist
 	;;	(cons (cons (concat proof-prog-name " .*")
@@ -398,7 +407,7 @@ Does nothing if proof assistant is already running."
 ;; Hooks here are handy for liaising with prover config stuff.
 
 (defvar proof-shell-kill-function-hooks nil
-  "Functions run from proof-shell-kill-function.")
+  "Functions run from `proof-shell-kill-function'.")
   
 (defun proof-shell-kill-function ()
   "Function run when a proof-shell buffer is killed.
@@ -528,7 +537,7 @@ left around so the user may discover what killed the process."
 (defun proof-shell-restart ()
   "Clear script buffers and send `proof-shell-restart-cmd'.
 All locked regions are cleared and the active scripting buffer
-deactivated.  
+deactivated.
 
 If the proof shell is busy, an interrupt is sent with
 `proof-interrupt-process' and we wait until the process is ready.
@@ -591,7 +600,7 @@ This is a subroutine of `proof-shell-handle-error'."
       ;; that may be needed in our start-regexp parameter (e.g. Isabelle).
 
       (goto-char (point-max))
-      (setq end (re-search-backward 
+      (setq end (re-search-backward
 		 proof-shell-annotated-prompt-regexp))
       (goto-char (marker-position proof-marker))
       (setq start (point))
@@ -611,7 +620,8 @@ This is a subroutine of `proof-shell-handle-error'."
 
 (defsubst proof-shell-strip-output-markup (string &optional push)
   "Strip output markup from STRING.
-Convenience function to call ` proof-shell-strip-output-markup'."
+Convenience function to call function `proof-shell-strip-output-markup'.
+Optional argument PUSH is ignored."
   (funcall proof-shell-strip-output-markup string))
 
 
@@ -621,7 +631,7 @@ Convenience function to call ` proof-shell-strip-output-markup'."
 ;;
 
 (defvar proof-shell-no-error-display nil
-  "If non-nil, do not display errors from the prover. 
+  "If non-nil, do not display errors from the prover.
 An internal setting used in `proof-shell-invisible-cmd-get-result'.")
 
 ;; TODO: combine next two functions
@@ -652,7 +662,7 @@ Runs `proof-shell-error-or-interrupt-action'."
       (if proof-shell-truncate-before-error proof-shell-interrupt-regexp)
       'proof-error-face)
      ;;  (proof-display-and-keep-buffer proof-response-buffer)
-     (proof-warning 
+     (proof-warning
       "Interrupt: script management may be in an inconsistent state
            (but it's probably okay)")
      (setq proof-shell-interrupt-pending nil)
@@ -681,7 +691,7 @@ flags) will not invoke this action."
     ;; Give a hint about C-c C-`.  NB: this is rather approximate,
     ;; we ought to check whether there is an error location in the
     ;; latest message, not just somewhere in the response buffer.
-    (if (pg-response-has-error-location) 
+    (if (pg-response-has-error-location)
 	(pg-next-error-hint)))
 
     ;; Make sure that prover is outputting data now.
@@ -736,10 +746,10 @@ To extend this function, set `proof-shell-classify-output-system-specific'.
 The \"aborted\" case is intended for killing off an open proof during
 retraction.  Typically it matches the message caused by a
 `proof-kill-goal-command'.  It simply inserts the word \"Aborted\" into
-the response buffer.  So it is expected to be the result of a 
+the response buffer.  So it is expected to be the result of a
 retraction, rather than the indication that one should be made.
 
-This function sets variables: `proof-shell-last-output', 
+This function sets variables: `proof-shell-last-output',
 `proof-shell-last-output-kind', `proof-shell-proof-completed'."
   ;; Keep a record of the last message from the prover
   (setq proof-shell-last-output string)
@@ -759,12 +769,12 @@ This function sets variables: `proof-shell-last-output',
     ((proof-shell-string-match-safe proof-shell-proof-completed-regexp string)
      ;; FIXME PG 4.0: want to remove side effects here
      ;;  In case no goals display
-     ;;     (proof-clean-buffer proof-goals-buffer) 
+     ;;     (proof-clean-buffer proof-goals-buffer)
      (setq proof-shell-last-output-kind 'goals) ;; PG 4.0: test
      ;; counter of commands since proof complete.
      (setq proof-shell-proof-completed 0)
      ;; But!  We carry on matching below for goals output, so that
-     ;; provers may include proof completed message as part of 
+     ;; provers may include proof completed message as part of
      ;; goals message (Isabelle, HOL) or not (LEGO, Coq).
      nil))
 
@@ -777,17 +787,17 @@ This function sets variables: `proof-shell-last-output',
        (while (string-match proof-shell-start-goals-regexp string start)
 	 (setq start (match-end 0)))
        ;; Convention: provers with special characters appearing in
-       ;; proof-start-goals-regexp don't include the match in their 
+       ;; proof-start-goals-regexp don't include the match in their
        ;; goals output.  Others do.
        ;; (Improvement to examine proof-start-goals-regexp suggested
        ;;  for Coq by Robert Schneck because Coq has specials but
        ;;  doesn't markup goals output specially).
 ;; FIXME: try to remove this for PG 4.0
-;;        (unless (and 
+;;        (unless (and
 ;; 		pg-subterm-first-special-char
-;; 		(not (string-equal 
+;; 		(not (string-equal
 ;; 		      proof-shell-start-goals-regexp
-;; 		      (pg-assoc-strip-subterm-markup 
+;; 		      (pg-assoc-strip-subterm-markup
 ;; 		       proof-shell-start-goals-regexp))))
        (setq start (match-beginning 0))
        (setq end (if proof-shell-end-goals-regexp
@@ -816,7 +826,7 @@ This function sets variables: `proof-shell-last-output',
 	      cmd string))
 
     ;; Finally, any other output will appear as a response.
-    (t 
+    (t
      (setq proof-shell-last-output-kind 'response)))))
 
 
@@ -831,9 +841,9 @@ This function sets variables: `proof-shell-last-output',
   "Insert STRING at the end of the proof shell, call `comint-send-input'.
 
 First we call `proof-shell-insert-hook'.  The arguments `action' and
-`scriptspan' may be examined by the hook to determine how to modify 
+`scriptspan' may be examined by the hook to determine how to modify
 the `string' variable (exploiting dynamic scoping) which will be
-the command actually sent to the shell. 
+the command actually sent to the shell.
 
 Note that the hook is not called for the empty (null) string
 or a carriage return.
@@ -849,8 +859,8 @@ used in `proof-append-alist' when we start processing a queue, and in
     (goto-char (point-max))
     
     ;; Hook for munging `string' and other dirty hacks.
-    (unless (or (null string) 
-		(string-equal string "") 
+    (unless (or (null string)
+		(string-equal string "")
 		(string-equal string "\n"))
       (run-hooks 'proof-shell-insert-hook))
 
@@ -868,7 +878,7 @@ used in `proof-append-alist' when we start processing a queue, and in
     ;; FIXME da: this space fudge is actually a visible hack:
     ;; the response string begins with a space and a newline.
     ;; It was needed to work around differences in Emacs versions.
-    ;; PG 4.0: consider alternative of maintaining marker at 
+    ;; PG 4.0: consider alternative of maintaining marker at
     ;; position -1
     (insert " ")
 
@@ -940,10 +950,10 @@ track what happens in the proof queue."
 
 (defun proof-append-alist (alist &optional queuemode)
   "Chop off the vacuous prefix of the command queue ALIST and queue it.
-For each `proof-no-command' item at the head of the list, invoke its 
+For each `proof-no-command' item at the head of the list, invoke its
 callback and remove it from the list.
 
-Append the result onto `proof-action-list', and if the proof 
+Append the result onto `proof-action-list', and if the proof
 shell isn't already busy, grab the lock with QUEUEMODE and
 start processing the queue.
 
@@ -952,8 +962,8 @@ then QUEUEMODE must match the mode of the queue currently
 being processed."
   (let (item)
     ;; NB: wrong time for callbacks for no-op commands, if queue non-empty.
-    (while (and alist (string= 
-		       (nth 1 (setq item (car alist))) 
+    (while (and alist (string=
+		       (nth 1 (setq item (car alist)))
 		       proof-no-command))
       (proof-shell-invoke-callback item)
       (setq alist (cdr alist)))
@@ -988,7 +998,7 @@ being processed."
 	    (if (proof-shell-should-be-silent (length alist))
 		;; 
 		(progn
-		  (setq proof-action-list 
+		  (setq proof-action-list
 			(list (proof-shell-start-silent-item)))
 		  (setq item (car proof-action-list))))
 	    (setq proof-action-list
@@ -996,7 +1006,7 @@ being processed."
 	    ;; Really start things going here
 	    (proof-shell-insert (nth 1 item) (nth 2 item) (nth 0 item)))))))
 
-;;;###autoload    
+;;;###autoload
 (defun proof-start-queue (start end alist)
   "Begin processing a queue of commands in ALIST.
 If START is non-nil, START and END are buffer positions in the
@@ -1017,7 +1027,7 @@ The queue mode is set to 'advancing"
   (proof-append-alist alist 'advancing))
 
 
-(defun proof-shell-exec-loop () 
+(defun proof-shell-exec-loop ()
   "Process the `proof-action-list'.
 
 `proof-action-list' contains a list of (SPAN COMMAND ACTION [FLAGS]) lists.
@@ -1027,18 +1037,18 @@ head of the list is the previously executed command which succeeded.
 We execute (ACTION SPAN) on the first item, then (ACTION SPAN) on any
 following items which have `proof-no-command' as their cmd components.
 
-If a there is a next command after that, send it to the process.  
+If a there is a next command after that, send it to the process.
 
 If the action list becomes empty, unlock the process and remove
 the queue region.
 
 The return value is non-nil if the action list is now empty."
 
-  (or 
+  (or
    (null proof-action-list)
    (save-excursion
      (if proof-script-buffer		      ; switch to active script
-	 (set-buffer proof-script-buffer)) 
+	 (set-buffer proof-script-buffer))
      
      (let ((item  (car proof-action-list))
 	   (flags (nthcdr 3 (car proof-action-list))))
@@ -1049,14 +1059,14 @@ The return value is non-nil if the action list is now empty."
 
        ;; slurp comments without sending to prover
        (while (and proof-action-list
-		   (string= 
-		    (nth 1 (setq item (car proof-action-list))) 
+		   (string=
+		    (nth 1 (setq item (car proof-action-list)))
 		    proof-no-command))
 	 (proo-shell-invoke-callback item)
 	 (setq proof-action-list (cdr proof-action-list)))
 
        ;; if action list is (nearly) empty, ensure prover is noisy.
-       ;; FIXME: chance to loose output if we processed a bunch of o/p 
+       ;; FIXME: chance to loose output if we processed a bunch of o/p
        ;; ending with a series of comments!
        (if (and proof-shell-silent
 		(or (null proof-action-list)
@@ -1090,7 +1100,7 @@ The return value is non-nil if the action list is now empty."
 
 (defun proof-shell-insert-loopback-cmd  (cmd)
   "Insert command sequence sent from prover into script buffer.
-String is inserted at the end of locked region, after a newline 
+String is inserted at the end of locked region, after a newline
 and indentation.  Assumes proof-script-buffer is active."
   (unless (string-match "^\\s-*$" cmd)	; FIXME: assumes cmd is single line
     (with-current-buffer proof-script-buffer
@@ -1103,7 +1113,7 @@ and indentation.  Assumes proof-script-buffer is active."
 	;; assumed the pbp command would succeed, but it seems fine?
 	;; But this action belongs in the proof script code.
 	;; NB: difference between ordinary commands and pbp is that
-	;; pbp can return *several* commands, that are treated as 
+	;; pbp can return *several* commands, that are treated as
 	;; a unit, i.e. sent to the proof assistant together.
 	;; FIXME da: this seems very similar to proof-insert-pbp-command
 	;; in proof-script.el.  Should be unified, I suspect.
@@ -1111,31 +1121,31 @@ and indentation.  Assumes proof-script-buffer is active."
 	(span-set-property span 'type 'pbp)
 	(span-set-property span 'cmd cmd)
 	(proof-set-queue-endpoints (proof-locked-end) (point))
-	(setq proof-action-list 
-	      (cons (car proof-action-list) 
+	(setq proof-action-list
+	      (cons (car proof-action-list)
 		    (cons (list span cmd 'proof-done-advancing)
 			  (cdr proof-action-list))))))))
 
 (defun proof-shell-message (str)
   "Output STR in minibuffer."
   (message "%s" ;; to escape format characters
-	   (concat "[" proof-assistant "] " 
+	   (concat "[" proof-assistant "] "
 		   ;; TODO: rather than stripping, could try fontifying
 		   (proof-shell-strip-output-markup str))))
 
 (defun proof-shell-process-urgent-message (message)
   "Analyse urgent MESSAGE for various cases.
-Cases are: included file, retracted file, cleared response buffer, 
-variable setting or dependency list. 
+Cases are: included file, retracted file, cleared response buffer,
+variable setting or dependency list.
 If none of these apply, display MESSAGE.
 
-MESSAGE should be a string annotated with 
+MESSAGE should be a string annotated with
 `proof-shell-eager-annotation-start', `proof-shell-eager-annotation-end'."
     (cond
      ;; CASE tracing output: use tracing buffer
      ((and proof-shell-trace-output-regexp
 	   (string-match proof-shell-trace-output-regexp message))
-      (proof-trace-buffer-display 
+      (proof-trace-buffer-display
 ;; FIXME: remove for PG 4.0
 ;;       (if (or pg-use-specials-for-fontify
 ;;	       proof-shell-unicode)
@@ -1152,7 +1162,7 @@ MESSAGE should be a string annotated with
 
        
      ;; CASE processing file: update known files list
-     ((and proof-shell-process-file 
+     ((and proof-shell-process-file
 	   (string-match (car proof-shell-process-file) message))
       (let
 	  ((file (funcall (cdr proof-shell-process-file) message)))
@@ -1169,7 +1179,7 @@ MESSAGE should be a string annotated with
 	    ;; Previously active scripting buffer
 	    ((scrbuf proof-script-buffer))
 	  ;; NB: we assume that no new buffers are *added* by
-	  ;; the proof-shell-compute-new-files-list 
+	  ;; the proof-shell-compute-new-files-list
 	  (proof-restart-buffers
 	   (proof-files-to-buffers
 	  (set-difference current-included
@@ -1193,17 +1203,17 @@ MESSAGE should be a string annotated with
 	   (string-match proof-shell-clear-goals-regexp message))
       (proof-clean-buffer proof-goals-buffer))
    
-     ;; CASE variable setting: prover asks PG to set some variable 
+     ;; CASE variable setting: prover asks PG to set some variable
      ((and proof-shell-set-elisp-variable-regexp
 	   (string-match proof-shell-set-elisp-variable-regexp message))
-      (let 
+      (let
 	  ((variable   (match-string 1 message))
 	   (expr       (match-string 2 message)))
 	(condition-case nil
 	    (with-temp-buffer
 	      (insert expr) ; massive risk from malicious provers!!
 	      (set (intern variable) (eval-last-sexp t)))
-	  (t (proof-debug 
+	  (t (proof-debug
 	      (concat
 	       "lisp error when obeying proof-shell-set-elisp-variable: \n"
 	       "setting `" variable "'\n to: \n"
@@ -1223,40 +1233,40 @@ MESSAGE should be a string annotated with
 	(pg-pgip-process-packet parsed-pgip)))
      
      ;; CASE theorem dependency: prover lists thms used in last proof
-     ((and proof-shell-theorem-dependency-list-regexp 
+     ((and proof-shell-theorem-dependency-list-regexp
 	   (string-match proof-shell-theorem-dependency-list-regexp message))
       (let ((names   (match-string 1 message))
 	    (deps    (match-string 2 message)))
-	(setq proof-last-theorem-dependencies 
-	      (cons 
-	       (split-string names 
+	(setq proof-last-theorem-dependencies
+	      (cons
+	       (split-string names
 			     proof-shell-theorem-dependency-list-split)
-	       (split-string deps  
+	       (split-string deps
 			     proof-shell-theorem-dependency-list-split)))))
 
 	   
      (t
-      ;; CASE everything else.  We're about to display a message.  
+      ;; CASE everything else.  We're about to display a message.
       ;; Clear the response buffer this time, but not next, leave window.
       (pg-response-maybe-erase nil nil)
 ;; FIXME: remove for PG 4.0
-;;      (let ((stripped (if proof-shell-unicode 
+;;      (let ((stripped (if proof-shell-unicode
 ;;			  (proof-shell-strip-eager-annotations message)
 ;;			(pg-remove-specials-in-string
 ;;			 (pg-assoc-strip-subterm-markup message)))))
 	;; Display first chunk of output in minibuffer.
 	;; Maybe this should be configurable, it can get noisy.
-	(proof-shell-message 
+	(proof-shell-message
 	 (substring message 0 (or (string-match "\n" message)
 				   (min (length message) 75))))
-	(pg-response-display-with-face 
+	(pg-response-display-with-face
 	 (proof-shell-strip-eager-annotations message)
 	 'proof-eager-annotation-face))))
 
 (defun proof-shell-strip-eager-annotations (string)
   "Strip `proof-shell-eager-annotation-{start,end}' from STRING."
   (save-match-data
-   (substring 
+   (substring
     string
     (if (string-match proof-shell-eager-annotation-start string)
 	(match-end 0) 0)
@@ -1270,7 +1280,7 @@ MESSAGE should be a string annotated with
   "Issue MSG as a prompt and receive user input."
   (let ((input
 	 (ignore-errors
-	   (read-string msg nil 
+	   (read-string msg nil
 	    'proof-shell-minibuffer-urgent-interactive-input-history))))
     ;; Always send something, even if read-input was errorful
     (proof-shell-insert (or input "") 'interactive-input)))
@@ -1347,7 +1357,7 @@ is only changed when input is sent in `proof-shell-insert'."
     ;; needed, as matching the prompt may be efficient enough anyway.
 
     (if ;; Some proof systems can be hacked to have annotated prompts;
-	;; for these we set proof-shell-wakeup-char to the annotation 
+	;; for these we set proof-shell-wakeup-char to the annotation
 	;; special, and look for it in the output before doing anything.
 	(if proof-shell-wakeup-char
 	    ;; NB: this match doesn't work in emacs-mule, darn.
@@ -1367,24 +1377,24 @@ is only changed when input is sent in `proof-shell-insert'."
 	    ;; Set marker to after the first prompt in the
 	    ;; output buffer if one can be found now.
 	    ;; NB: ideally, we'd rather do this initialization outside
-	    ;; of the filter function for slightly better efficiency.  
+	    ;; of the filter function for slightly better efficiency.
 	    ;; Could be achieved by switching between filter functions.
 	    (progn
 	      (goto-char (point-min))
 	      (if (re-search-forward proof-shell-annotated-prompt-regexp nil t)
 		  (progn
 		    (set-marker proof-marker (point))
-		    ;; The first time a prompt is seen we ignore any 
+		    ;; The first time a prompt is seen we ignore any
 		    ;; output that occured before it, assuming that
-		    ;; corresponds to uninteresting startup messages. 
+		    ;; corresponds to uninteresting startup messages.
 		    ;; We process the
 		    ;; action list to remove the first item if need
-		    ;; be (proof-shell-init-cmd sent if 
+		    ;; be (proof-shell-init-cmd sent if
 		    ;; proof-shell-config-done).
 		    (if proof-action-list
 			(proof-shell-filter-manage-output "")))))
 	  ;; Now we're looking for the end of the piece of output
-	  ;; which will be processed.  
+	  ;; which will be processed.
 	  
 	  ;; Note that the way this filter works, only one piece of
 	  ;; output can be dealt with at a time so we loose sync if
@@ -1392,7 +1402,7 @@ is only changed when input is sent in `proof-shell-insert'."
 	  
 	  (if proof-action-list
 	      ;; We were expecting some output, examine it.
-	      (let ((urgnt    (marker-position 
+	      (let ((urgnt    (marker-position
 			       proof-shell-urgent-message-marker))
 		    string startpos prev-prompt)
 
@@ -1402,7 +1412,7 @@ is only changed when input is sent in `proof-shell-insert'."
 		;; to filter out or delete the urgent messages which
 		;; have been processed already.
 		(setq prev-prompt (goto-char (marker-position proof-marker)))
-		(setq startpos prev-prompt) 
+		(setq startpos prev-prompt)
 		(if (and urgnt
 			 (< startpos urgnt))
 		    (setq startpos (goto-char urgnt))
@@ -1410,8 +1420,8 @@ is only changed when input is sent in `proof-shell-insert'."
 		  (if (eq (char-after startpos) ?\ )
 		      (setq startpos (goto-char (+ 2 startpos)))
 		    (setq startpos (goto-char (1+ startpos)))))
-		;; Find next prompt.  
-		(if (re-search-forward 
+		;; Find next prompt.
+		(if (re-search-forward
 		     proof-shell-annotated-prompt-regexp nil t)
 		    (progn
 		      (setq proof-shell-last-prompt
@@ -1424,20 +1434,20 @@ is only changed when input is sent in `proof-shell-insert'."
 		      (setq proof-shell-expecting-output nil)
 		      ;; Process output string.
 		      (proof-shell-filter-manage-output string)
-		      ;; Cleanup shell buffer 
+		      ;; Cleanup shell buffer
 		      (unless proof-general-debug
 			(pg-remove-specials prev-prompt (point-max)))
 		      )))
 	    (if proof-shell-busy
 		;; internal error recovery:
 		(progn
-		  (proof-debug 
+		  (proof-debug
 		   "proof-shell-filter found empty action list yet proof shell busy.")
 		  (proof-release-lock))))))))
 
 (defun proof-shell-process-urgent-messages ()
   "Scan the shell buffer for urgent messages.
-Scanning starts from `proof-shell-urgent-message-scanner' or 
+Scanning starts from `proof-shell-urgent-message-scanner' or
 `comint-last-input-end', which ever is later.  We deal with strings
 between regexps eager-annotation-start and eager-annotation-end.
 
@@ -1446,12 +1456,12 @@ being filtered process because we have no guarantees about where
 chunks are broken: it may be in the middle of an annotation.
 
 This is a subroutine of `proof-shell-filter'."
-  (let ((pt (point)) (end t) lastend 
+  (let ((pt (point)) (end t) lastend
 	(start (max (marker-position proof-shell-urgent-message-scanner)
 		    (marker-position comint-last-input-end))))
     (goto-char start)
     (while (and end
-		(re-search-forward proof-shell-eager-annotation-start 
+		(re-search-forward proof-shell-eager-annotation-start
 				   nil 'end))
       (setq start (match-beginning 0))
       (if (setq end
@@ -1479,7 +1489,7 @@ This is a subroutine of `proof-shell-filter'."
 	;; If the search for the starting annotation was unsuccessful,
 	;; set the scanner marker to the limit of the last search for
 	;; the starting annotation, less the maximal length of the
-	;; annotation.  
+	;; annotation.
 	(set-marker
 	 proof-shell-urgent-message-scanner
 	 (min
@@ -1518,7 +1528,7 @@ This is a subroutine of `proof-shell-filter'."
 Appropriate action is taken depending on what
 `proof-shell-classify-output' returns: maybe handle an interrupt, an
 error, or deal with ordinary output which is a candidate for the goal
-or response buffer.  
+or response buffer.
 
 Ordinary output is only displayed when the proof action list
 becomes empty, to avoid a confusing rapidly changing output.
@@ -1541,7 +1551,7 @@ by the filter is to send the next command from the queue."
 
      ;; Otherwise, delay handling ordinary script functions: don't act
      ;; unless all the commands the queue region have been processed.
-     (t 
+     (t
       (setq proof-shell-delayed-output-kind proof-shell-last-output-kind)
       (setq proof-shell-delayed-output proof-shell-last-output)
       (setq proof-shell-delayed-flags flags)
@@ -1593,16 +1603,16 @@ interrupt message is printed from the prover after the last output.")
   "Interrupt the proof assistant.  Warning! This may confuse Proof General.
 
 This sends an interrupt signal to the proof assistant, if Proof General
-thinks it is busy.  
+thinks it is busy.
 
-This command is risky because we don't know whether the last command 
-succeeded or not.  The assumption is that it didn't, which should be true 
+This command is risky because we don't know whether the last command
+succeeded or not.  The assumption is that it didn't, which should be true
 most of the time, and all of the time if the proof assistant has a careful
 handling of interrupt signals.
 
 Some provers may ignore (and lose) interrupt signals, or fail to indicate
-that they have been acted upon but get stop in the middle of output.  
-In the first case, PG will terminate the queue of commands at the first 
+that they have been acted upon but get stop in the middle of output.
+In the first case, PG will terminate the queue of commands at the first
 available point.  In the second case, you may need to press enter inside
 the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*)."
   (interactive)
@@ -1612,7 +1622,7 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*).
     (error "Proof Process Not Active!"))
   (with-current-buffer proof-shell-buffer
     (if proof-shell-expecting-output
-	(progn 
+	(progn
 	  (setq proof-shell-interrupt-pending t) ; interrupt even if no interrupt message
 	  (interrupt-process nil comint-ptyp))
       ;; otherwise, interrupt the queue right here
@@ -1631,8 +1641,8 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*).
 ;;   tracing output has ended
 ;; -- need to fontify remaining portion of buffer in case
 ;;   tracing output has ended when in slow mode (and refresh
-;;   final display)  
-;; -- shouldn't be trigger for only a small amount of output 
+;;   final display)
+;; -- shouldn't be trigger for only a small amount of output
 ;;   (e.g. output from blast).  Or a count of number of successive
 ;;   bursts?
 
@@ -1656,28 +1666,28 @@ Only works when system timer has microsecond count available."
     (if pg-tracing-slow-mode
 	(if (eq (nth 0 pg-last-tracing-output-time) (nth 0 tm))
 	    ;; see if seconds has changed by at least pg-slow-mode-duration
-	    (if (> (- (nth 1 tm) (nth 1 pg-last-tracing-output-time)) 
+	    (if (> (- (nth 1 tm) (nth 1 pg-last-tracing-output-time))
 		   pg-slow-mode-duration)
 		;; go out of slow mode
-		(progn 
+		(progn
 		  (setq pg-tracing-slow-mode nil)
 		  (setq pg-last-tracing-output-time tm)
 		  (cancel-timer pg-tracing-cleanup-timer))
 	      ;; otherwise: stay in slow mode
 	      t)
 	  ;; different seconds-major count: go out of slow mode
-	  (progn 
+	  (progn
 	    (setq pg-last-tracing-output-time tm)
 	    (setq pg-tracing-slow-mode nil)))
       ;; ordinary mode: examine difference since last output
       (if
-	  (and pg-last-tracing-output-time 
+	  (and pg-last-tracing-output-time
 	       (eq (nth 0 tm) (nth 0 pg-last-tracing-output-time))
 	       (eq (nth 1 tm) (nth 1 pg-last-tracing-output-time))
 	       ;; Same second: examine microsecond
 	       (> (nth 2 tm) 0) ;; some systems always have zero count
 	       ;; 
-	       (< (- (nth 2 tm) (nth 2 pg-last-tracing-output-time)) 
+	       (< (- (nth 2 tm) (nth 2 pg-last-tracing-output-time))
 		  pg-fast-tracing-mode-threshold))
 	  ;; quickly consecutive and large tracing outputs: go into slow mode
 	  (progn
@@ -1723,17 +1733,17 @@ in some cases.   May be called by `proof-shell-invisible-command'."
 	    (accept-process-output proverproc 1)
 	    (sit-for 1))
 	  (if quit-flag
-	      ;; This *shouldn't* really happen, but lockups in this 
+	      ;; This *shouldn't* really happen, but lockups in this
 	      ;; function have been seen in some odd scenarios.
 	      (error "Proof General: Quit in proof-shell-wait"))))))
 
 (defun proof-done-invisible (span)
-  "Callback for proof-shell-invisible-command.  
+  "Callback for proof-shell-invisible-command.
 Calls proof-state-change-hook."
   (run-hooks 'proof-state-change-hook))
 
 ;;;###autoload
-(defun proof-shell-invisible-command (cmd &optional wait invisiblecallback 
+(defun proof-shell-invisible-command (cmd &optional wait invisiblecallback
 					  &rest flags)
   "Send CMD to the proof process.
 The CMD is `invisible' in the sense that it is not recorded in buffer.
@@ -1749,7 +1759,7 @@ before and after sending the command.
 In case CMD is (or yields) nil, do nothing.
 
 INVISIBLECALLBACK will be invoked after the command has finished,
-if it is set.  It should probably run the hook variables 
+if it is set.  It should probably run the hook variables
 `proof-state-change-hook'.
 
 If NOERROR is set, surpress usual error action."
@@ -1767,14 +1777,14 @@ If NOERROR is set, surpress usual error action."
 	(if wait (proof-shell-wait))
 	(proof-shell-ready-prover)  ; start proof assistant; set vars.
 	(let* ((callback
-		(if invisiblecallback 
+		(if invisiblecallback
 		    (lexical-let ((icb invisiblecallback))
 		      (lambda (span)
 			(funcall icb span)))
 		  'proof-done-invisible)))
 	  (proof-start-queue nil nil
-			     (list (proof-shell-action-list-item 
-				    cmd 
+			     (list (proof-shell-action-list-item
+				    cmd
 				    callback
 				    flags))))
 	(if wait (proof-shell-wait)))))
@@ -1811,7 +1821,7 @@ Error messages are displayed as usual."
 
 ;(eval-and-compile			; to define vars
 ;;;###autoload
-(define-derived-mode proof-shell-mode comint-mode 
+(define-derived-mode proof-shell-mode comint-mode
   "proof-shell" "Proof General shell mode class for proof assistant processes"
 
   (setq proof-buffer-type 'shell)
@@ -1824,12 +1834,12 @@ Error messages are displayed as usual."
 
   ;; comint customisation. comint-prompt-regexp is used by
   ;; comint-get-old-input, comint-skip-prompt, comint-bol, backward
-  ;; matching input, etc.  
+  ;; matching input, etc.
   (if proof-shell-prompt-pattern
       (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. 
+  ;; not see all output produced by the proof process.
   (remove-hook 'comint-output-filter-functions
 	       'comint-postoutput-scroll-to-bottom 'local)
 
@@ -1845,12 +1855,12 @@ Error messages are displayed as usual."
   ;; Urgent message marker records end position of last urgent
   ;; message seen.
   (setq proof-shell-urgent-message-marker (make-marker))
-  ;; Urgent message scan marker records starting position to 
+  ;; Urgent message scan marker records starting position to
   ;; scan for urgent messages from
   (setq proof-shell-urgent-message-scanner (make-marker))
   (set-marker proof-shell-urgent-message-scanner (point-min))
 
-  ;; Make cut functions work with proof shell output 
+  ;; Make cut functions work with proof shell output
   (add-hook 'buffer-substring-filters 'proof-shell-strip-output-markup)
 
   ;; FIXME da: before entering proof assistant specific code,
@@ -1907,10 +1917,10 @@ processing."
 
       (if (memq (process-status proc) '(open run))
 	  (progn
-	    ;; Also ensure that proof-action-list is initialised. 
+	    ;; Also ensure that proof-action-list is initialised.
 	    (setq proof-action-list nil)
 	    ;; Send main intitialization command and wait for it to be
-	    ;; processed.   
+	    ;; processed.
 	    
 	    ;; First, if the prover supports PGIP and preferences are
 	    ;; not configured, we may configure them.  (NB: this
@@ -1927,7 +1937,7 @@ processing."
 		  (if proof-shell-init-cmd
 		      (proof-shell-invisible-command proof-shell-init-cmd t))
 		  (if proof-assistant-settings
-		      (proof-shell-invisible-command 
+		      (proof-shell-invisible-command
 		       (proof-assistant-settings-cmd) t)))
 
 	      ;; Configure for unicode input
@@ -1937,3 +1947,7 @@ processing."
 
 (provide 'proof-shell)
 ;; proof-shell.el ends here
+
+(provide 'proof-shell)
+
+;;; proof-shell.el ends here