Clean whitespace

30 files changed, 528 insertions, 531 deletions

diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index 1a1dcd23..6d041c08 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -1,6 +1,6 @@
 ;;; pg-assoc.el --- Functions for associated buffers
 ;;
-;; Copyright (C) 1994-2008 LFCS Edinburgh. 
+;; Copyright (C) 1994-2008 LFCS Edinburgh.
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
@@ -13,7 +13,7 @@
 
 ;;; Code:
 
-(eval-when-compile 
+(eval-when-compile
   (require 'proof-syntax)			; proof-replace-{string,regexp}
   (require 'span)				; spans
   (require 'cl))				; incf
@@ -24,7 +24,7 @@
     proof-general-name "Universal keymaps only"
     ;; Doesn't seem to supress TAB, RET
     (suppress-keymap proof-universal-keys-only-mode-map 'all)
-    (proof-define-keys proof-universal-keys-only-mode-map 
+    (proof-define-keys proof-universal-keys-only-mode-map
 		       proof-universal-keys)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -34,7 +34,7 @@
 
 ;;;###autoload
 (defun proof-associated-buffers ()
-  "Return a list of the associated buffers.  
+  "Return a list of the associated buffers.
 Some may be dead/nil."
   (list proof-goals-buffer
 	proof-response-buffer
@@ -44,7 +44,7 @@ Some may be dead/nil."
 
 ;;;###autoload
 (defun proof-associated-windows ()
-  "Return a list of the associated buffers windows.  
+  "Return a list of the associated buffers windows.
 Dead or nil buffers are not represented in the list."
   (let ((bufs (proof-associated-buffers))
 	buf wins)
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index a8185557..5fb14f0b 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -12,13 +12,13 @@
 ;; -- add more precise functional tests to check results
 ;; -- add negative tests
 ;; -- output test results to stdout
-;; 
+;;
 ;; $Id$
 
 (require 'proof)
 
 ;;; Commentary:
-;; 
+;;
 
 ;;; Code:
 (defvar pg-autotest-success t)		;; success unless error caught
@@ -112,9 +112,8 @@ An error is signalled if scripting doesn't complete."
 (defun pg-autotest-finished ()
   "Exit Emacs returning Unix success 0 if all tests succeeded."
   (kill-emacs (if pg-autotest-success 0 1)))
-    
-    
+
+
 
 (provide 'pg-autotest)
 ;;; pg-autotest.el ends here
-
diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index b49c35ad..7457de50 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -7,7 +7,7 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Prover specific settings and user options.
 ;;
 ;; The settings defined here automatically use the current proof
@@ -16,7 +16,7 @@
 ;;
 ;; This file is loaded only by mode stubs defined in `proof-site.el',
 ;; immediately after `proof-assistant' and similar settings have been
-;; configured.  
+;; configured.
 ;;
 ;; WARNING: loading this file without these variables being set will
 ;; give errors, because defpgcustom calls are expanded to top-level
@@ -150,7 +150,7 @@ of `easy-menu-define' for more details."
 (defpgcustom keymap (make-keymap (concat proof-assistant " keymap"))
   "Proof assistant specific keymap, used under prefix C-c a."
   :type 'sexp
-  :group 'prover-config) 
+  :group 'prover-config)
 
 (defpgcustom completion-table nil
   "List of identifiers to use for completion for this proof assistant.
@@ -178,7 +178,7 @@ Enabled by default for Coq.
 Currently this setting is UNIMPLEMENTED, changes have no effect."
   :type 'boolean
   :group 'prover-config)
-  
+
 
 
 
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index e3e53c5a..a0b125a4 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -58,7 +58,7 @@ May enable proof-by-pointing or similar features.
 (define-key proof-goals-mode-map [q] 'bury-buffer)
 ;; TODO: use standard Emacs button behaviour here (cf Info mode)
 (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
-(define-key proof-goals-mode-map [C-mouse-3] 
+(define-key proof-goals-mode-map [C-mouse-3]
   'proof-undo-and-delete-last-successful-command)
 
 
@@ -81,14 +81,14 @@ Converts term substructure markup into mouse-highlighted extents."
   (save-excursion
     ;; Response buffer may be out of date. It may contain (error)
     ;; messages relating to earlier proof states
-    
+
     ;; NB: this isn't always the case.  In Isabelle
     ;; we get <WARNING MESSAGE> <CURRENT GOALS> output,
     ;; or <WARNING MESSAGE> <ORDINARY MESSAGE>.  Both times
     ;; <WARNING MESSAGE> would be relevant.
     ;; We should only clear the output that was displayed from
     ;; the *previous* prompt.
-    
+
     ;; Erase the response buffer if need be, maybe removing the
     ;; window.  Indicate it should be erased before the next output.
     (pg-response-maybe-erase t t)
@@ -105,7 +105,7 @@ Converts term substructure markup into mouse-highlighted extents."
       (insert string)
       (setq buffer-read-only t)
       (set-buffer-modified-p nil)
-      
+
       ;; Keep point at the start of the buffer.
       (proof-display-and-keep-buffer
        proof-goals-buffer (point-min)))))
@@ -125,14 +125,14 @@ Converts term substructure markup into mouse-highlighted extents."
     (cond
      (sendback
       (with-current-buffer buf
-	(let* ((cmdstart (previous-single-property-change pos 'sendback 
+	(let* ((cmdstart (previous-single-property-change pos 'sendback
 							  nil (point-min)))
-	       (cmdend   (next-single-property-change pos 'sendback 
+	       (cmdend   (next-single-property-change pos 'sendback
 						      nil (point-max)))
 	       (cmd      (buffer-substring-no-properties cmdstart cmdend)))
 	  (proof-insert-sendback-command cmd)))))))
 
-	
+
 
 
 
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index 5750b325..2e8a75b0 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -8,15 +8,15 @@
 ;;
 ;; Analyse the goal buffer to produce a popup menu.
 ;;
-;; NB: this code is currently XEmacs specific 
+;; NB: this code is currently XEmacs specific
 ;; (uses make-gui-button, insert-gui-button, make-dialog-frame)
 ;;
-;; da: can you simply use 
+;; da: can you simply use
 ;;   make-button/make-text-button and something like
 ;;
 ;;   (make-frame '((minibuffer . nil) (menu-bar-lines . 0) (tool-bar-lines . nil)))
 
-;;   
+;;
 
 ;;; Code:
 (require 'proof)
@@ -89,7 +89,7 @@ Matches the region to be returned.")
 		      (span-read-only spl)))
 		  (span-property span 'occurrences)))))))
 
- 
+
 (defun pg-pbrpm-create-reset-buffer-menu ()
   "Create if necessary and erase all text in the buffer menu."
   (if (or (not pg-pbrpm-buffer-menu) (not (buffer-live-p pg-pbrpm-buffer-menu)))
@@ -118,7 +118,7 @@ If stores, in the variable pg-pbrpm-goal-description, a list with shape
      goal-name: the goal name (or number)
      start-concl: the position of first char of the conclusion of the goal
      hyps: the list of hypothesis with the shape:
-       
+
   (start-hyp start-hyp-text end-hyp hyp-name ...) with 4 elemets per hypothesis:
      start-hyp: the position of the first char of the hypothesis (including its name)
      start-hyp-text: the position of the first char of the hypothesis formula (no name)
@@ -152,7 +152,7 @@ If stores, in the variable pg-pbrpm-goal-description, a list with shape
 		      (append
 		       (list start-hyp start-hyp-text end-hyp hyp-name)
 		       hyps))))
-	    
+
 	    (setq goals
 		  (append
 		   (list start-goal end-goal goal-num
@@ -193,8 +193,8 @@ The prover command is processed via pg-pbrpm-run-command."
    (let ((click-info (pg-pbrpm-process-click event start end))) ; retrieve click informations
      (if click-info
 	 (let ((pbrpm-list
-		(pg-pbrpm-eliminate-id 
-		 nil 
+		(pg-pbrpm-eliminate-id
+		 nil
 		 (mapcar 'cdr
 			 (sort
 			  (proof-pbrpm-generate-menu
@@ -211,13 +211,13 @@ The prover command is processed via pg-pbrpm-run-command."
 		     (while pbrpm-list
 		       (let* ((pbrpm-list-car (pop pbrpm-list))
 			      (description (pop pbrpm-list-car))
-			      (command (concat "(*" description "*)\n" 
+			      (command (concat "(*" description "*)\n"
 					       (pop pbrpm-list-car))))
 			 (setq pbrpm-menu-desc
 			       (append pbrpm-menu-desc
 				       (list (vector
 					      description
-					      (list 'pg-pbrpm-run-command 
+					      (list 'pg-pbrpm-run-command
 						    (list command nil nil))))))))
 		     ;; finally display the pop-up-menu
 		     (popup-menu pbrpm-menu-desc))
@@ -235,14 +235,14 @@ The prover command is processed via pg-pbrpm-run-command."
 		     (let ((spans (pg-pbrpm-setup-span pos (point))))
 		       (insert-gui-button (make-gui-button
 					   (concat (int-to-string count) ")")
-					   'pg-pbrpm-run-command 
+					   'pg-pbrpm-run-command
 					   (list command act spans)) pos))
 		     (insert "\n")))
-		 (insert-gui-button 
+		 (insert-gui-button
 		  (make-gui-button
 		   "Cancel"
 		   (lambda (n) (pg-pbrpm-erase-buffer-menu) (delete-frame)) nil))
-		 ;; needs to be fixed for other prover than phox 
+		 ;; needs to be fixed for other prover than phox
 		 ;; da: I've removed code here, we should simply keep this
 		 ;; buffer with font lock on.
 		 (mapc 'span-read-only pg-pbrpm-spans)
@@ -308,7 +308,7 @@ The prover command is processed via pg-pbrpm-run-command."
       (cons allspan (sort (reverse spans) (lambda (sp1 sp2)
 				  (< (span-property sp1 'goalnum)
 				     (span-property sp1 'goalnum))))))))
-  
+
 (defun pg-pbrpm-run-command (args)
 "Insert COMMAND into the proof queue and then run it.
 -- adapted from proof-insert-pbp-command --"
@@ -342,8 +342,8 @@ The prover command is processed via pg-pbrpm-run-command."
   "Get position information for POS.
 Returns (n . s) where
     n is the goal name
-    s if either the hypothesis name, 
-         \"none\" (for the conclusion),
+    s if either the hypothesis name,
+	 \"none\" (for the conclusion),
 	 or \"whole\" in strange cases."
   (let ((l pg-pbrpm-goal-description)
 	(found nil)
@@ -390,10 +390,10 @@ See `pg-pbrpm-get-pos-info'."
 	     r1
 	   (cons (car r1) "whole"))
        nil)))
-	 
+
 (defun pg-pbrpm-auto-select-around-point ()
   "Extract some text arround point, according to `pg-pbrpm-auto-select-regexp'.
-If no match found, return the empty string." 
+If no match found, return the empty string."
   (save-excursion
     (let ((pos (point)))
       (beginning-of-line)
@@ -401,15 +401,15 @@ If no match found, return the empty string."
 	(while (< (point) pos)
 	  (unless (search-forward-regexp pg-pbrpm-auto-select-regexp nil t)
 	    (return-from 'loop ""))
-	  (if (and (<= (match-beginning 0) pos) 
+	  (if (and (<= (match-beginning 0) pos)
 		   (<= pos (match-end 0)))
 	      (return-from 'loop (match-string 0))))
 	(return-from 'loop "")))))
-    
+
 (defun pg-pbrpm-translate-position (buffer pos)
   "return pos if buffer is goals-buffer otherwise, return the point position in
    the goal buffer"
-  (if (eq proof-goals-buffer buffer) 
+  (if (eq proof-goals-buffer buffer)
       pos
     (with-current-buffer proof-goals-buffer
       (point))))
@@ -505,7 +505,7 @@ If no match found, return the empty string."
   (interactive "*e")
   (setq pg-pbrpm-remember-region-selected-region nil)
   (let ((mouse-track-drag-up-hook 'pg-pbrpm-remember-region-drag-up-hook)
- 	(mouse-track-click-hook 'pg-pbrpm-remember-region-click-hook)
+	(mouse-track-click-hook 'pg-pbrpm-remember-region-click-hook)
 	(start (point)) (end (mark)))
 	       (if (and start end) (pg-pbrpm-do-remember-region start end))
 	       (mouse-track event)
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index 8987b2a4..dad49539 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -21,14 +21,14 @@
 ;; -- parsescript input/outputs
 ;; -- guiconfig, some parts of
 ;; -- support fully native PGIP mode
-;; 
+;;
 
 
 ;;; Commentary:
-;; 
+;;
 
 (require 'cl)				; incf
-(require 'pg-xml)
+(require 'pg-xml)			;
 (require 'proof-config)			;; config variables
 
 ;;; Code:
@@ -107,13 +107,13 @@ Return a symbol representing the PGIP command processed, or nil."
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 
+;;
 ;; Message processing: fromprovermsg/kitconfig
 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun pg-pgip-process-askpgip (node)
-  (pg-pgip-debug "Received <askpgip> message with version `%s'" 
+  (pg-pgip-debug "Received <askpgip> message with version `%s'"
 		 (pg-xml-get-attr 'version node 'notreallyoptional))
   ;; TODO: send a uses PGIP message back?
   )
@@ -193,7 +193,7 @@ Return a symbol representing the PGIP command processed, or nil."
 (defun pg-pgip-process-prefval (node)
 ;;
 ;; <prefval name="n">value</prefval>
-;; 
+;;
 ;; Proof assistant advises that preference n has been updated.
 ;;
 ;; Protocol is that <setpref> sent on a PGIP channel is assumed to
@@ -282,7 +282,7 @@ Return a symbol representing the PGIP command processed, or nil."
   )
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 
+;;
 ;; Message processing: fromprovermsg/proveroutput
 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -325,7 +325,7 @@ Return a symbol representing the PGIP command processed, or nil."
   )
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 
+;;
 ;; Message processing: fromprovermsg/fileinfomsg
 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -335,7 +335,7 @@ Return a symbol representing the PGIP command processed, or nil."
 	 (url	    (pg-pgip-get-url node))
 	 (filename  (pg-pgip-get-url-filename url))) ;; FIXME: unimplemented!
     (proof-register-possibly-new-processed-file filename)))
-    
+
 (defun pg-pgip-process-informfileretracted (node)
   (let* ((thyname    (pg-pgip-get-thyname node))
 	 (url	    (pg-pgip-get-url node))
@@ -344,7 +344,7 @@ Return a symbol representing the PGIP command processed, or nil."
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 
+;;
 ;; Message processing: todisplaymsg/brokermsg
 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -362,7 +362,7 @@ Return a symbol representing the PGIP command processed, or nil."
   )
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 
+;;
 ;; Message processing: todisplaymsg/dispmsg/dispfilemsg
 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -384,7 +384,7 @@ Also sets local proverid and srcid variables for buffer."
 	(make-local-variable 'proverid)
 	(setq proverid proverid))
       (set pg-pgip-srcids (acons srcid (list buffer file) pg-pgip-srcids)))))
-      
+
 
 ;; FIXME: right action?
 (defun pg-pgip-process-filestatus (node)
@@ -402,7 +402,7 @@ Also sets local proverid and srcid variables for buffer."
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 
+;;
 ;; Message processing: todisplaymsg/dispmsg/dispobjmsg
 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -418,7 +418,7 @@ Also sets local proverid and srcid variables for buffer."
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 
+;;
 ;; Message processing: parsescript [incomplete]
 ;;
 ;; NB: pgip.rnc v 2.18 only has parsescript sent to prover,
@@ -426,7 +426,7 @@ Also sets local proverid and srcid variables for buffer."
 ;;
 ;; Provide parsing functionality for other interfaces (sacrilege!)
 ;;
-  
+
 (defun pg-pgip-process-parsescript (node)
   ;; Text ought to be cdata or something. We'll stick it into a buffer
   ;; and run the proof-script code on it.
@@ -441,7 +441,7 @@ Also sets local proverid and srcid variables for buffer."
 	;; FIXME: todo: make parseresult element according to types,
 	;; properscriptcmd = properproofcmd | properfilecmd | bindid
 	))))
-	
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -455,7 +455,7 @@ Also sets local proverid and srcid variables for buffer."
   (let ((tyname (and node (xml-node-name node))))
     (cond
      ((eq tyname 'pgipbool)	'boolean)
-     ((eq tyname 'pgipint) 	'integer) ;; TODO: implement range limits
+     ((eq tyname 'pgipint)	'integer) ;; TODO: implement range limits
      ((eq tyname 'pgipstring)	'string)
      ((eq tyname 'pgipconst)
       (let ((name	(pg-pgip-get-name node 'optional))
@@ -512,7 +512,7 @@ Also sets local proverid and srcid variables for buffer."
     (pg-pgip-interpret-choice (cdr type) value))
    (t
     (pg-pgip-error "pg-pgip-interpret-value: unkown type %s" type))))
-    
+
 (defun pg-pgip-interpret-choice (choices value)
   ;; Untagged union types: test for value in each type in turn.
   (let (res)
@@ -579,7 +579,7 @@ See `pg-pgip-assemble-packet' "
 REFSEQ and REFID are used for the corresponding attributes, if present.
 By default, the class of the message is \"pa\" (destined for prover).
 OTHERCLASS overrides this."
-  (let* ((tag 	        (pg-xml-attr tag
+  (let* ((tag	        (pg-xml-attr tag
 				     (concat "EmacsPG/"
 					     proof-general-short-version
 					     "/" proof-assistant)))
diff --git a/generic/pg-response.el b/generic/pg-response.el
index d97d58d5..30f7b329 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -8,7 +8,7 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; This mode is used for the response buffer proper, and
 ;; also the trace and theorems buffer. A sub-module of proof-shell.
 ;;
@@ -76,7 +76,7 @@
   (setq font-lock-defaults '(proof-response-font-lock-keywords)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 
+;;
 ;; Window configuration
 ;;   -- multiple frames for goals and response buffers,
 ;;   -- three window mode
@@ -96,7 +96,7 @@ Internal variable, setting this will have no effect!")
   "List of GNU Emacs frame parameters for secondary frames.")
 
 (defun proof-multiple-frames-enable ()
-  (let ((spdres (cons 
+  (let ((spdres (cons
 		 pg-response-special-display-regexp
 		 proof-multiframe-parameters)))
     (if proof-multiple-frames-enable
@@ -133,7 +133,7 @@ Internal variable, setting this will have no effect!")
    (if (buffer-live-p proof-response-buffer)
        proof-response-buffer (first (buffer-list)))
    nohorizontalsplit))
-   
+
 
 (defvar pg-frame-configuration nil
   "Variable storing last used frame configuration.")
@@ -207,9 +207,9 @@ For multiple frame mode, this function obeys the setting of
 	       (fm (and win (window-frame win))))
 	  (unless (equal mainframe fm)
 	    (if fm (delete-frame fm))))))))
-	
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 
+;;
 ;; Displaying in the response buffer
 ;;
 
@@ -264,13 +264,13 @@ Returns non-nil if response buffer was cleared."
 ;;
 ;; Images for the response buffer
 ;;
-;(defimage pg-response-error-image 
+;(defimage pg-response-error-image
 ;  ((:type xpm :file "/home/da/PG/images/epg-interrupt.xpm")))
 
-;(defimage pg-response-warning-image 
+;(defimage pg-response-warning-image
 ;  ((:type xpm :file "/home/da/PG/images/epg-abort.xpm")))
 
-  
+
 ;; TODO: this function should be combined with
 ;; pg-response-maybe-erase-buffer.
 ;;;###autoload
@@ -296,10 +296,10 @@ Also updates `proof-shell-last-output'."
 	(insert str)
 	(setq proof-shell-last-output str)
 	(unless (bolp) (newline))
- 	(when face
- 	  (overlay-put
- 	   (make-overlay start (point-max))
- 	   'face face))
+	(when face
+	  (overlay-put
+	   (make-overlay start (point-max))
+	   'face face))
 
 	(setq buffer-read-only t)
 	(set-buffer-modified-p nil))))))
@@ -413,7 +413,7 @@ See `pg-next-error-regexp'."
 	(set-buffer proof-response-buffer)
 	(goto-char (point-min))
 	(re-search-forward pg-next-error-regexp nil t))))
-	
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -448,7 +448,7 @@ We fontify the output only if we're not too busy to do so."
       (newline))))
 ;;; FIXME: reinstate this, turning font lock off then on, mebbe
 ;;;     (or proof-trace-last-fontify-pos
-;;; 	(setq proof-trace-last-fontify-pos (point)))
+;;;	(setq proof-trace-last-fontify-pos (point)))
 ;;;     (insert str)
 ;;;     (unless (bolp)
 ;;;       (newline))
@@ -456,20 +456,20 @@ We fontify the output only if we're not too busy to do so."
 ;;;     ;; fontifying every chunk and batch it up instead.
 ;;;     (unless pg-tracing-slow-mode
 ;;;       (let ((fontifystart (proof-trace-fontify-pos)))
-;;; 	;; Catch errors, in case fontification buggy
-;;; 	(unwind-protect
-;;; 	    (proof-fontify-region fontifystart (point))
-;;; 	  (setq proof-trace-last-fontify-pos nil))
-;;; 	(set-buffer-modified-p nil)))))
+;;;	;; Catch errors, in case fontification buggy
+;;;	(unwind-protect
+;;;	    (proof-fontify-region fontifystart (point))
+;;;	  (setq proof-trace-last-fontify-pos nil))
+;;;	(set-buffer-modified-p nil)))))
 
 (defun proof-trace-buffer-finish ()
   "Complete fontification in tracing buffer now that there's time to do so."
   )
 ;;;   (let ((fontifystart (proof-trace-fontify-pos)))
 ;;;     (if (and fontifystart (not quit-flag));; may be done already
-;;; 	(save-excursion
-;;; 	   (set-buffer proof-trace-buffer)
-;;; 	   (proof-fontify-region fontifystart (point-max))))))
+;;;	(save-excursion
+;;;	   (set-buffer proof-trace-buffer)
+;;;	   (proof-fontify-region fontifystart (point-max))))))
 
 
 
@@ -482,7 +482,7 @@ We fontify the output only if we're not too busy to do so."
 ;; Revives an old idea from Isamode: a buffer displaying a bunch
 ;; of theorem names.
 ;;
-;; 
+;;
 
 (defun pg-thms-buffer-clear ()
   "Clear the theorems buffer."
diff --git a/generic/pg-thymodes.el b/generic/pg-thymodes.el
index de4c31ca..b019e6ef 100644
--- a/generic/pg-thymodes.el
+++ b/generic/pg-thymodes.el
@@ -7,7 +7,7 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Functions for defining "theory" modes, i.e.  modes for
 ;; non-interactive proof assistant files which do not contain proof
 ;; scripts.
@@ -71,7 +71,7 @@ All of these settings are optional."
 (defmacro pg-do-unless-null (val &rest body)
   `(if ,val
        (progn ,@body)))
-    
+
 
 (defun pg-symval (sym &optional other)
   "Return (symbol-value SYM) or nil/OTHER if SYM unbound."
@@ -89,9 +89,9 @@ All of these settings are optional."
     (if (boundp modesym)
 	(symbol-value modesym)
       other)))
-  
 
-  
+
+
 
 (provide 'pg-thymodes)
 ;;; pg-thymodes.el ends here
diff --git a/generic/pg-user.el b/generic/pg-user.el
index b92280da..37710977 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -8,7 +8,7 @@
 ;;
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; This file defines some user-level commands.  Most of them
 ;; are script-based operations.  Exported user-level commands
 ;; are defined here as autoloads to avoid circular requires.
@@ -96,7 +96,7 @@ Assumes script buffer is current."
 	      (if win
 		  (set-window-point win dest)))))
 	 ((eq proof-follow-mode 'locked)
-	  (if pos 
+	  (if pos
 	      (goto-char dest)
 	    (proof-script-next-command-advance)))
 	 ((and (eq proof-follow-mode 'followdown)
@@ -188,7 +188,7 @@ the proof script."
 	       (goto-char (span-start lastspan))
 	       (proof-retract-until-point delete))
 	   (error "Nothing to undo!"))))
-     (if lastspan (proof-maybe-follow-locked-end 
+     (if lastspan (proof-maybe-follow-locked-end
 		   (span-start lastspan))))))
 
 (defun proof-retract-buffer ()
@@ -246,12 +246,12 @@ the proof script."
   "Set point to end of command at point."
   (interactive)
   (let ((cmd (span-at (point) 'type)))
-    (if cmd 
+    (if cmd
 	(goto-char (span-end cmd))
       (let ((semis (save-excursion
 		     (proof-segment-up-to-using-cache (point)))))
 	(if semis
-	    (progn 
+	    (progn
 	      (goto-char (nth 2 (car semis)))
 	      (skip-chars-backward " \t\n")
 	      (unless (eq (point) (point-min))
@@ -269,7 +269,7 @@ the proof script."
    (mouse-set-point event)
    (proof-goto-point)
    (proof-maybe-follow-locked-end)))
-  
+
 
 
 
@@ -352,12 +352,12 @@ a proof command."
 
 
 
-	  
+
 
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;; 
+;;;
 ;;; Non-scripting proof assistant commands.
 ;;;
 
@@ -420,7 +420,7 @@ CMDVAR is a variable holding a function or string.  Automatically has history."
        (proof-if-setting-configured ,cmdvar
 	   (if (stringp ,cmdvar)
 	       (list (format ,cmdvar
-		 	 (read-string
+			 (read-string
 			   ,(concat prompt ": ") ""
 			   ,(intern (concat (symbol-name fn) "-history")))))
 	     (funcall ,cmdvar))))
@@ -531,7 +531,7 @@ This is intended as a value for `proof-activate-scripting-hook'"
   ;; TODO: probably even this isn't necessary
   (force-mode-line-update))
 
-(proof-deftoggle proof-electric-terminator-enable 
+(proof-deftoggle proof-electric-terminator-enable
 		 proof-electric-terminator-toggle)
 
 (defun proof-process-electric-terminator ()
@@ -563,7 +563,7 @@ comment, and insert or skip to the next semi)."
 	    (progn
 	      (setq incomment t)
 	      ;; delete spurious char in comment
-	      (if ins (backward-delete-char 1)) 
+	      (if ins (backward-delete-char 1))
 	      (goto-char mrk)
 	      (insert proof-terminal-string))
 	  (proof-assert-semis semis)
@@ -753,7 +753,7 @@ If NUM is negative, move upwards.  Return new span."
 	    (span-set-property span 'controlspan new-parent)
 	    (list span))))
     start end 'type)))
-      
+
 (defun pg-move-region-down (&optional num)
   "Move the region under point downwards in the buffer, past NUM spans."
   (interactive "p")
@@ -783,9 +783,9 @@ If NUM is negative, move upwards.  Return new span."
 ;      (if span
 ;	  (if pg-drag-region-point
 ;	      ;; Move the region at point to region here.
-	      
 
-	  
+
+
 ;(defun pg-mouse-drag-up-move-region-function (event click-count)
 ;  (setq pg-drag-region-point nil))
 
@@ -817,13 +817,13 @@ If NUM is negative, move upwards.  Return new span."
 (defun proof-backward-command (&optional num)
   (interactive "p")
   (proof-forward-command (- num)))
-  
 
-   
 
 
 
-  
+
+
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -907,13 +907,13 @@ If NUM is negative, move upwards.  Return new span."
   (goto-char (span-start span))
   (proof-retract-until-point))
 
-  
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Generic adjustmenth of prover's pretty-printing width
 ;; (adapted from Lego's mode, was also used in Isar and Plastic)
-;; 
+;;
 ;; FIXME: complete this.
 
 ;(defvar pg-prover-current-line-width nil
@@ -929,8 +929,8 @@ If NUM is negative, move upwards.  Return new span."
 ;	(progn
 ;	  ;; Update the prover's output width
 ;	  (proof-shell-invisible-command
-	   
-	
+
+
 ;with-current-buffer buffer
 ;    (let ((current-width
 ;	   (window-width (get-buffer-window proof-goals-buffer)))
@@ -967,7 +967,7 @@ If NUM is negative, move upwards.  Return new span."
 ;;;###autoload
 (defun pg-jump-to-end-hint ()
   (pg-hint "Use \\[proof-goto-end-of-locked] to jump to end of processed region"))
-  
+
 ;;;###autoload
 (defun pg-processing-complete-hint ()
   "Display hint for showing end of locked region or processing complete."
@@ -1019,8 +1019,8 @@ The function `substitute-command-keys' is called on the argument."
 (defun pg-identifier-near-point-query ()
   (interactive)
   (let* ((stend       (if (region-active-p)
-		          (cons (region-beginning) (region-end))
-		        (pg-current-word-pos)))
+			  (cons (region-beginning) (region-end))
+			(pg-current-word-pos)))
 	 (start       (car-safe stend))
 	 (end         (cdr-safe stend))
 	 (identifier  (if start
@@ -1031,11 +1031,11 @@ The function `substitute-command-keys' is called on the argument."
 			    (goto-char start)
 			    (proof-buffer-syntactic-context)))))
     (if start
-	(pg-identifier-query 
+	(pg-identifier-query
 	 identifier ctxt
 	 ;; the callback
 	 (lexical-let ((s start) (e end))
-	   (lambda (x) 
+	   (lambda (x)
 	     (let ((idspan (span-make s e)))
 	       ;; TODO: clean these up!
 	       (span-set-property idspan 'help-echo
@@ -1045,7 +1045,7 @@ The function `substitute-command-keys' is called on the argument."
 (defvar proof-query-identifier-history nil)
 
 (defun proof-query-identifier (string)
-  (interactive 
+  (interactive
    (list
     (completing-read "Query identifier: "
 		     proof-query-identifier-collection
@@ -1327,7 +1327,7 @@ removed if it matches the last item in the ring."
 	   (not (ring-empty-p pg-input-ring))
 	   (string-equal (ring-ref pg-input-ring 0) cmd))
       (ring-remove pg-input-ring 0)))
-  
+
 
 ;;;###autoload
 (defun  pg-clear-input-ring ()
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 402608a8..ec673ed6 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -7,7 +7,7 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Global variables used in several files.
 ;;
 ;;
@@ -21,19 +21,19 @@
 
 (defvar proof-assistant-cusgrp nil
   "Symbol for the customization group of the user options for the proof assistant.
-Do not change this variable! It is set automatically by the mode 
-stub defined in proof-site, from the name given in 
+Do not change this variable! It is set automatically by the mode
+stub defined in proof-site, from the name given in
 proof-assistant-table.")
 
 (defvar proof-assistant-internals-cusgrp nil
   "Symbol for the customization group of the PG internal settings proof assistant.
-Do not change this variable! It is set automatically by the mode 
+Do not change this variable! It is set automatically by the mode
 stub defined in proof-site, from the name given in
 proof-assistant-table.")
 
 (defvar proof-assistant ""
   "Name of the proof assistant Proof General is using.
-Do not change this variable! It is set automatically by the mode 
+Do not change this variable! It is set automatically by the mode
 stub defined in proof-site, from names given in proof-assistant-table.")
 
 (defvar proof-assistant-symbol nil
@@ -45,28 +45,28 @@ Non-nil indicates PG has been initialised for an assistant.
 If this is nil, the hook functions in `proof-ready-for-assistant-hook'
 are yet to be run.
 
-Do not change this variable! It is set automatically by the mode 
-stub defined in proof-site, from the symbols given in 
+Do not change this variable! It is set automatically by the mode
+stub defined in proof-site, from the symbols given in
 `proof-assistant-table'.")
 
 (defvar proof-mode-for-shell nil
-  "Mode function for proof shell buffers. 
-Do not change this variable! It is set automatically by the mode 
+  "Mode function for proof shell buffers.
+Do not change this variable! It is set automatically by the mode
 stub defined in proof-site to <PA>-shell-mode.")
 
 (defvar proof-mode-for-response nil
   "Mode function for proof response buffer (and trace buffer, if used).
-Do not change this variable! It is set automatically by the mode 
+Do not change this variable! It is set automatically by the mode
 stub defined in proof-site to <PA>-response-mode.")
 
 (defvar proof-mode-for-goals nil
   "Mode for proof state display buffers.
-Do not change this variable! It is set automatically by the mode 
+Do not change this variable! It is set automatically by the mode
 stub defined in proof-site to <PA>-goals-mode.")
 
 (defvar proof-mode-for-script nil
   "Mode for proof script buffers.
-Do not change this variable! It is set automatically by the mode 
+Do not change this variable! It is set automatically by the mode
 stub defined in proof-site to <PA>-mode.")
 
 (defvar proof-ready-for-assistant-hook nil
@@ -76,7 +76,7 @@ has been set.")
 
 
 ;;;
-;;; Later variables 
+;;; Later variables
 ;;; (could be separated to cut down Emacs env pollution)
 ;;;
 
@@ -162,7 +162,7 @@ of the proof (starting from 1).")
 
 ;;
 ;; Internal variables
-;; -- usually local to a couple of modules but here to avoid 
+;; -- usually local to a couple of modules but here to avoid
 ;; compile warnings
 ;;
 
@@ -173,7 +173,7 @@ This is raw string, for internal use only.")
 (defvar proof-assistant-settings nil
  "A list of default values kept in Proof General for current proof assistant.
 A list of lists (SYMBOL SETTING TYPE DESCR) where SETTING is a string value
-to send to the proof assistant using the value of SYMBOL and 
+to send to the proof assistant using the value of SYMBOL and
 and the function `proof-assistant-format'.  The TYPE item determines
 the form of the menu entry for the setting and the DESCR description
 string is used as a help tooltip in the settings menu.")
@@ -234,7 +234,7 @@ where `k' is a key binding (vector) and `f' the designated function."
   :type 'sexp
   :group 'proof-general-internals)
 
- 
+
 
 (provide 'pg-vars)
 ;; pg-vars.el ends here
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 73be1b7b..53338267 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -28,8 +28,8 @@ Stop keeping ring history for current buffer.
 Minor mode retaining an in-memory history of the buffer contents.
 
 Commands:\\<bufhist-minor-mode-map>
-\\[bufhist-prev]    bufhist-prev    go back in history  
-\\[bufhist-next]    bufhist-next    go forward in history  
+\\[bufhist-prev]    bufhist-prev    go back in history
+\\[bufhist-next]    bufhist-next    go forward in history
 \\[bufhist-first]   bufhist-first   go to first item in history
 \\[bufhist-last]    bufhist-last    go to last (current) item in history.
 \\[bufhist-clear]   bufhist-clear   clear history.
@@ -90,13 +90,13 @@ This mode is only useful with a font which can display the maths repertoire.
 ;;; Generated autoloads from pg-assoc.el
 
 (autoload 'proof-associated-buffers "pg-assoc" "\
-Return a list of the associated buffers.  
+Return a list of the associated buffers.
 Some may be dead/nil.
 
 \(fn)" nil nil)
 
 (autoload 'proof-associated-windows "pg-assoc" "\
-Return a list of the associated buffers windows.  
+Return a list of the associated buffers windows.
 Dead or nil buffers are not represented in the list.
 
 \(fn)" nil nil)
@@ -384,7 +384,7 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit.
 Turn on or off maths-menu mode in Proof General script buffer.
 This invokes `maths-menu-mode' to toggle the setting for the current
 buffer, and then sets PG's option for default to match.
-Also we arrange to have maths menu mode turn itself on automatically 
+Also we arrange to have maths menu mode turn itself on automatically
 in future if we have just activated it for this buffer.
 
 \(fn)" t nil)
diff --git a/generic/proof-auxmodes.el b/generic/proof-auxmodes.el
index 69dc0b72..f4f2a60f 100644
--- a/generic/proof-auxmodes.el
+++ b/generic/proof-auxmodes.el
@@ -5,7 +5,7 @@
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 
 ;;; Commentary:
-;; 
+;;
 ;; Startup code from auxiliary modes are collected here, allowing late
 ;; loading of their main defining files and the possibility to disable them.
 ;;
@@ -36,7 +36,7 @@
 (proof-eval-when-ready-for-assistant
     (if (and (proof-ass mmm-enable)
 	     (proof-mmm-support-available))
-        (proof-mmm-set-global t)))
+	(proof-mmm-set-global t)))
 
 
 ;;
@@ -55,7 +55,7 @@ The test loads optional prover-specific config in <foo>-maths-menu.el"
 
 ;;
 ;; Unicode tokens
-;; 
+;;
 (defun proof-unicode-tokens-support-available ()
   "A test to see whether unicode tokens support is available."
   ;; Requires prover-specific config in <foo>-unicode-tokens.el
diff --git a/generic/proof-config.el b/generic/proof-config.el
index b0612661..c472187e 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -7,11 +7,11 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; This file declares all prover-specific configuration variables for
 ;; Proof General.  The variables are used variously by the proof
 ;; script mode and the proof shell mode, menus, and toolbar.
-;; 
+;;
 ;; To customize Proof General for a new proof assistant, you
 ;; should read this file carefully!
 ;;
@@ -54,10 +54,10 @@
 ;;    (b) add a magical comment in ProofGeneral.texi/PG-Adapting.texi
 ;;
 ;; ii.  Presently the customize library seems a bit picky over the
-;;  	:type property and some correct but complex types don't work:
-;;  	If the type is ill-formed, editing the whole group will be
-;;  	broken.  Check after updates, by killing all customize buffers
-;;  	and invoking customize-group
+;;	:type property and some correct but complex types don't work:
+;;	If the type is ill-formed, editing the whole group will be
+;;	broken.  Check after updates, by killing all customize buffers
+;;	and invoking customize-group
 ;;
 ;;
 ;; See also:
@@ -85,16 +85,14 @@
 ;; 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-general-internal
-;; group.
+;; 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-general-internal group.
 
 (defcustom proof-guess-command-line nil
   "Function to guess command line for proof assistant, given a filename.
@@ -394,7 +392,7 @@ NB: This setting is not used for matching output from the prover."
 
 (defcustom proof-save-with-hole-regexp nil
   "Regexp which matches a command to save a named theorem.
-The name of the theorem is build from the variable
+
The name of the theorem is build from the variable
 `proof-save-with-hole-result' using the same convention as
 `query-replace-regexp'.
 Used for setting names of goal..save and proof regions and for
@@ -582,7 +580,7 @@ may be lost in the prover.  So we allow Proof General to close
 off the goal..[save] region in more flexible ways.
 The possibilities are:
 
-        nil  -  nothing special; close only when a save arrives
+	nil  -  nothing special; close only when a save arrives
   'closeany  -  close as soon as the next command arrives, save or not
  'closegoal  -  close when the next \"goal\" command arrives
     'extend  -  keep extending the closed region until a save or goal.
@@ -805,7 +803,7 @@ See also `proof-goals-font-lock-keywords' and `proof-response-font-lock-keywords
 (defcustom proof-script-syntax-table-entries nil
   "List of syntax table entries for proof script mode.
 A flat list of the form
- 
+
   (CHAR SYNCODE CHAR SYNCODE ...)
 
 See doc of `modify-syntax-entry' for details of characters
@@ -826,7 +824,7 @@ This should be a function which accepts three arguments: SPAN IDIOM NAME.
 See pg-user.el: pg-create-in-span-context-menu for more hints."
   :type 'function
   :group 'proof-script)
-  
+
 
 
 
@@ -852,7 +850,7 @@ See pg-user.el: pg-create-in-span-context-menu for more hints."
   :prefix "proof-shell-")
 
 
-;; 
+;;
 ;; 5a. commands
 ;;
 
@@ -1295,7 +1293,7 @@ The default value is \"\\n\" to match up to the end of the line."
 (defcustom proof-shell-strip-output-markup 'identity
   "A function which strips markup from the process output.
 This should remove any markup which is made invisible by font-lock
-when displayed in the output buffer.  This is used in 
+when displayed in the output buffer.  This is used in
 `pg-insert-last-output-as-comment' to insert output into the
 proof script, and for cut and paste operations."
   :type 'function
@@ -1331,7 +1329,7 @@ name is added to the front of `proof-included-files-list'."
 
 ;; FIXME da: why not amalgamate the next two into a single
 ;;	     variable as above?  Maybe because removing one
-;;	     
+;;
 
 (defcustom proof-shell-retract-files-regexp nil
   "Matches a message that the prover has retracted a file.
@@ -1565,13 +1563,13 @@ This setting is used inside the function `proof-format-filename'."
   ;; a good chance to guess if shell-command-to-string and uname
   ;; available.
   (not (and
-        ;; We should be using `system-type' here, instead.
+	;; We should be using `system-type' here, instead.
        (not (fboundp 'win32-long-file-name))
-        (fboundp 'shell-command-to-string)
-        (condition-case nil
-            ;; Which versions of Solaris are affected?  --Stef
-            (string-match "[sS]un" (shell-command-to-string "uname"))
-          (error nil))))
+	(fboundp 'shell-command-to-string)
+	(condition-case nil
+	    ;; Which versions of Solaris are affected?  --Stef
+	    (string-match "[sS]un" (shell-command-to-string "uname"))
+	  (error nil))))
   "The value of `process-connection-type' for the proof shell.
 Set non-nil for ptys, nil for pipes.
 The default (and preferred) option is to use pty communication.
@@ -1594,7 +1592,7 @@ If the prover can be set to output only one prompt for every chunk of
 input, then newlines can be retained in the input."
   :type 'boolean
   :group 'proof-shell)
-  
+
 (defcustom proof-shell-strip-crs-from-output (eq system-type 'cygwin32)
   ;; Cygwin32 probs with Isabelle noted by Norbert Voelker
   "If non-nil, remove carriage returns (^M) at the end of lines from output.
@@ -1705,7 +1703,7 @@ This hook is used within Proof General to refresh the toolbar."
 (defcustom proof-shell-syntax-table-entries nil
   "List of syntax table entries for proof script mode.
 A flat list of the form
- 
+
   (CHAR SYNCODE CHAR SYNCODE ...)
 
 See doc of `modify-syntax-entry' for details of characters
@@ -1785,7 +1783,7 @@ In particular, after a `pbp-goal-command' or a `pbp-hyp-command'."
   "Opening special character for subterm markup.
 Subsequent special characters with values *below*
 `pg-subterm-first-special-char' are assumed to be subterm position
-indicators.  Annotations should be finished with `pg-subterm-sep-char'; 
+indicators.  Annotations should be finished with `pg-subterm-sep-char';
 the end of the concrete syntax is indicated by `pg-subterm-end-char'.
 
 If `pg-subterm-start-char' is nil, subterm markup is disabled.
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 7605515f..e148df35 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -1,16 +1,16 @@
 ;; proof-depends.el  Theorem-theorem and theorem-definition dependencies.
 ;;
-;; Copyright (C) 2000-2004 University of Edinburgh. 
+;; Copyright (C) 2000-2004 University of Edinburgh.
 ;; Authors:      David Aspinall <David.Aspinall@ed.ac.uk>
 ;;	         Earlier version by Fiona McNeil.
 ;; License:      GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Status:       Experimental code
 ;;
 ;; $Id$
-;; 
+;;
 ;; Based on Fiona McNeill's MSc project on analysing dependencies
 ;; within proofs.  Code rewritten by David Aspinall.
-;; 
+;;
 
 (require 'cl)
 (require 'span)
@@ -42,14 +42,14 @@ For example, in isabelle, a file Stuff.ML contains theorems with
 fully qualified names of the form Stuff.theorem1, etc.
 For other provers, this function may need modifying."
   (if buffer-file-name
-      (file-name-nondirectory 
+      (file-name-nondirectory
        (file-name-sans-extension buffer-file-name)) ""))
 
 (defun proof-depends-module-of (name)
   "Return a pair of a module name and base name for a given item name.
 Assumes module name is given by dotted prefix."
   (let ((dot (string-match "\\." name)))
-    (if dot 
+    (if dot
 	(cons (substring name 0 dot) (substring name (+ dot 1)))
       (cons "" name))))
 
@@ -66,12 +66,12 @@ This is done using `proof-depends-module-name-for-buffer' and
       (setq names (cdr names)))
     ;; NB: reversed order
     samefile))
-	       
+
 
 ;;
 ;; proof-depends-process-dependencies: the main entry point.
 ;;
-;;;###autoload    
+;;;###autoload
 (defun proof-depends-process-dependencies (name gspan)
   "Process dependencies reported by prover, for NAME in span GSPAN.
 Called from `proof-done-advancing' when a save is processed and
@@ -91,15 +91,15 @@ Called from `proof-done-advancing' when a save is processed and
 	 ;; Find goalsave spans earlier in this file which this
 	 ;; one depends on; update their list of dependents,
 	 ;; and return resulting list paired up with names.
-	 (depspans    
+	 (depspans
 	  (apply 'append
-		 (span-mapcar-spans 
+		 (span-mapcar-spans
 		  (lambda (depspan)
 		    (let ((dname (span-property depspan 'name)))
 		      (if (and
 			   (eq (span-property depspan 'type) 'goalsave)
 			   (member dname samefilenames))
-			  (let ((forwarddeps 
+			  (let ((forwarddeps
 				 (span-property depspan 'dependents)))
 			    (span-set-property depspan 'dependents
 					       (cons
@@ -109,7 +109,7 @@ Called from `proof-done-advancing' when a save is processed and
 		  (point-min)
 		  (span-start gspan)
 		  'type))))
-    
+
     (span-set-property gspan 'dependencies-within-file depspans)
     (setq proof-last-theorem-dependencies nil)))
 
@@ -124,9 +124,9 @@ Called from `proof-done-advancing' when a save is processed and
 ;; which the dependency information is used.
 
 
-;;;###autoload    
+;;;###autoload
 (defun proof-dependency-in-span-context-menu (span)
-  "Make a portion of a context-sensitive menu showing proof dependencies." 
+  "Make a portion of a context-sensitive menu showing proof dependencies."
   ;; FIXME: might only activate this for dependency-relevant spans.
   (list
    "-------------"
@@ -151,7 +151,7 @@ Called from `proof-done-advancing' when a save is processed and
 (defun proof-dep-alldeps-menu (span)
   (or (span-property span 'dependencies-menu) ;; cached value
       (span-set-property span 'dependencies-menu
-			 (proof-dep-make-alldeps-menu 
+			 (proof-dep-make-alldeps-menu
 			  (span-property span 'dependencies)))))
 
 (defun proof-dep-make-alldeps-menu (deps)
@@ -161,7 +161,7 @@ Called from `proof-done-advancing' when a save is processed and
 	(let ((nestedtop   (proof-dep-split-deps deps)))
 	  (cons menuname
 		(append
-		 (mapcar (lambda (l) 
+		 (mapcar (lambda (l)
 			   (vector l (list showdep l) t))
 			 (cdr nestedtop))
 		 (mapcar (lambda (sm)
@@ -177,8 +177,8 @@ Called from `proof-done-advancing' when a save is processed and
   ;; NB: could handle deeper nesting here, but just do one level for now.
   (let (nested toplevel)
     ;; Add each name into a nested list or toplevel list
-    (mapcar 
-     (lambda (name) 
+    (mapcar
+     (lambda (name)
 	      (let* ((period   (string-match "\\." name))
 		     (ns       (and period (substring name 0 period)))
 		     (subitems (and ns (assoc ns nested))))
@@ -186,7 +186,7 @@ Called from `proof-done-advancing' when a save is processed and
 		 ((and ns subitems)
 		  (setcdr subitems (adjoin name (cdr subitems))))
 		 (ns
-		  (setq nested 
+		  (setq nested
 			(cons (cons ns (list name)) nested)))
 		 (t
 		  (setq toplevel (adjoin name  toplevel))))))
@@ -197,9 +197,9 @@ Called from `proof-done-advancing' when a save is processed and
   "Make menu items for a submenu NAME, using appfn applied to each elt in LIST.
 If LIST is empty, return a disabled menu item with NAME."
   (if list
-      (cons name 
-	    (mapcar `(lambda (l) 
-		       (vector (,namefn l) 
+      (cons name
+	    (mapcar `(lambda (l)
+		       (vector (,namefn l)
 			       (cons (quote ,appfn) l) t)) list))
     (vector name nil nil)))
 
@@ -210,7 +210,7 @@ If LIST is empty, return a disabled menu item with NAME."
 
 
 ;;
-;; Functions triggered by menus 
+;; Functions triggered by menus
 ;;
 
 (defun proof-goto-dependency (name span)
@@ -223,7 +223,7 @@ If LIST is empty, return a disabled menu item with NAME."
   "Show dependency THM using `proof-show-dependency-cmd'.
 This is simply to display the dependency somehow."
   (if proof-shell-show-dependency-cmd ;; robustness
-      (proof-shell-invisible-command 
+      (proof-shell-invisible-command
        (format proof-shell-show-dependency-cmd thm))))
 
 (defconst pg-dep-span-priority 500)
diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el
index 12b78242..de22153c 100644
--- a/generic/proof-easy-config.el
+++ b/generic/proof-easy-config.el
@@ -36,13 +36,13 @@
 	   ;; FIXME: in future versions, use these settings in *-config-done
 	   ;;        to simplify elisp code elsewhere.
 	   ;; FIXME: add imenu-generic-expression too
-	   ;; 
+	   ;;
 	   (modsyn    (intern (concat "proof-" suffixnm "-syntax-table-entries")))
 	   (fullbody  (append
 		       (if (and (boundp modsyn) (eval modsyn))
 			   (list `(let ((syn ,modsyn))
 				    (while syn
-				      (modify-syntax-entry 
+				      (modify-syntax-entry
 				       (car syn) (cadr syn))
 				      (setq syn (cddr syn))))))
 		       body)))
@@ -62,17 +62,17 @@
       (error "Macro proof-easy-config: second argument (%s) should be a string"
 	     name))
     (cond
-     ((or 
-       (and (boundp 'proof-assistant) proof-assistant 
+     ((or
+       (and (boundp 'proof-assistant) proof-assistant
 	    (not (equal proof-assistant ""))
 	    (not (equal proof-assistant name))
-	    (setq msg (format "\nproof-assistant name: \"%s\" doesn't match expected \"%s\"" 
+	    (setq msg (format "\nproof-assistant name: \"%s\" doesn't match expected \"%s\""
 			      proof-assistant name)))
        (and (boundp 'proof-assistant-symbol) proof-assistant-symbol
 	    (not (eq proof-assistant-symbol sym))
-	    (setq msg (format "\nproof-assistant symbol: '%s doesn't match expected '%s" 
+	    (setq msg (format "\nproof-assistant symbol: '%s doesn't match expected '%s"
 			      proof-assistant-symbol sym))))
-      (error "proof-easy-config: PG already in use or name/symbol mismatch %s" 
+      (error "proof-easy-config: PG already in use or name/symbol mismatch %s"
 	     msg))
      (t
       ;; Setting these here is nice for testing: no need to get
@@ -90,7 +90,6 @@ the `proof-assistant-table', which see."
      (setq
       ,@body)
      (proof-easy-config-define-derived-modes)))
-  
-;; 
-(provide 'proof-easy-config)
 
+;;
+(provide 'proof-easy-config)
diff --git a/generic/proof-faces.el b/generic/proof-faces.el
index ee6f426b..bc701565 100644
--- a/generic/proof-faces.el
+++ b/generic/proof-faces.el
@@ -7,7 +7,7 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Faces should work sensibly:
 ;;
 ;;   a) with default colours
@@ -29,7 +29,7 @@
   "Faces used by Proof General."
   :group 'proof-general
   :prefix "proof-")
-  
+
 ;; TODO: get rid of this list.  Does 'default work widely enough
 ;; by now?
 (defconst pg-defface-window-systems
@@ -161,7 +161,7 @@ Warning messages can come from proof assistant or from Proof General itself."
    (:italic t))
   "*Face for showing (backwards) dependent parts."
   :group 'proof-faces)
-  
+
 (defface proof-highlight-dependency-face
   (proof-face-specs
    (:background "khaki")
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index e792d931..1d00cf81 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -44,7 +44,7 @@
    (proof-looking-at-safe proof-indent-inner-regexp)
    (not
     (or (proof-looking-at-safe proof-indent-any-regexp)
-        (proof-looking-at-safe "\\s-*$")))))
+	(proof-looking-at-safe "\\s-*$")))))
 
 (defun proof-indent-goto-prev ()   ; Note: may change point, even in case of failure!
   "Goto to previous syntax element for script indentation, ignoring string/comment contexts."
@@ -60,12 +60,12 @@
        (found-prev (proof-indent-goto-prev)))
     (if (not found-prev) (goto-char current))   ; recover position
     (cond
-     ((and found-prev (or proof-indent-hang 
+     ((and found-prev (or proof-indent-hang
 			  (= (current-indentation) (current-column))))
       (+ indent
-         (current-column)
-         (if (and inner (not (proof-indent-inner-p))) 0 (proof-indent-indent))
-         (- (proof-indent-offset))))
+	 (current-column)
+	 (if (and inner (not (proof-indent-inner-p))) 0 (proof-indent-indent))
+	 (- (proof-indent-offset))))
      ((not found-prev) 0)         ;FIXME mmw: improve this case!?
      (t
       (proof-indent-calculate
@@ -77,16 +77,16 @@
   "Indent current line of proof script, if indentation enabled."
   (interactive)
   (unless (not (proof-ass script-indent))
-          (if (< (point) (proof-locked-end))
-              (if (< (current-column) (current-indentation))
-                  (skip-chars-forward "\t "))
-            (save-excursion
-              (indent-line-to
-               (max 0 (save-excursion
-                        (back-to-indentation)
-                        (proof-indent-calculate 
+	  (if (< (point) (proof-locked-end))
+	      (if (< (current-column) (current-indentation))
+		  (skip-chars-forward "\t "))
+	    (save-excursion
+	      (indent-line-to
+	       (max 0 (save-excursion
+			(back-to-indentation)
+			(proof-indent-calculate
 			 (proof-indent-offset) (proof-indent-inner-p))))))
-            (if (< (current-column) (current-indentation))
-                (back-to-indentation)))))
-      
+	    (if (< (current-column) (current-indentation))
+		(back-to-indentation)))))
+
 (provide 'proof-indent)
diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el
index a0764a98..de02cc7a 100644
--- a/generic/proof-maths-menu.el
+++ b/generic/proof-maths-menu.el
@@ -34,18 +34,18 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit."
     (if flag
 	(add-hook hook 'maths-menu-mode)
       (remove-hook hook 'maths-menu-mode))
-    (proof-map-buffers 
+    (proof-map-buffers
       (proof-buffers-in-mode proof-mode-for-script)
       (maths-menu-mode (if flag 1 0)))))
 
-  
-  
+
+
 ;;;###autoload
 (defun proof-maths-menu-enable ()
   "Turn on or off maths-menu mode in Proof General script buffer.
 This invokes `maths-menu-mode' to toggle the setting for the current
 buffer, and then sets PG's option for default to match.
-Also we arrange to have maths menu mode turn itself on automatically 
+Also we arrange to have maths menu mode turn itself on automatically
 in future if we have just activated it for this buffer."
   (interactive)
   (require 'maths-menu)
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 2f9da74f..53d692e8 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -1,6 +1,6 @@
 ;; proof-menu.el  Menus, keymaps, and misc commands for Proof General
 ;;
-;; Copyright (C) 2000,2001 LFCS Edinburgh. 
+;; Copyright (C) 2000,2001 LFCS Edinburgh.
 ;; Authors:   David Aspinall
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -22,22 +22,22 @@ A fixed number of repetitions of this command switches back to
 the same buffer.
 Also move point to the end of the response buffer if it's selected.
 If in three window or multiple frame mode, display two buffers.
-The idea of this function is to change the window->buffer mapping 
+The idea of this function is to change the window->buffer mapping
 without adjusting window layout."
   (interactive)
   ;; The GUI-tessence here is to implement a humane toggle, which
   ;; allows habituation.  E.g. two taps of C-c C-l always
   ;; shows the goals buffer, three the trace buffer, etc.
   ;; (That behaviour makes less sense from the menu, though,
-  ;;  where it seems more natural just to rotate from last 
+  ;;  where it seems more natural just to rotate from last
   ;;  position)
-  (cond 
-   ((and (interactive-p) 
+  (cond
+   ((and (interactive-p)
 	 (eq last-command 'proof-display-some-buffers))
     (incf proof-display-some-buffers-count))
    (t
     (setq proof-display-some-buffers-count 0)))
-  (let* ((assocbufs   (remove-if-not 'buffer-live-p 
+  (let* ((assocbufs   (remove-if-not 'buffer-live-p
 				     (list proof-response-buffer
 					   proof-thms-buffer
 					   proof-trace-buffer
@@ -48,7 +48,7 @@ without adjusting window layout."
     ;; If there's no live other buffers, we don't do anything.
     (unless (zerop numassoc)
       (let
-	 ((selectedbuf (nth (mod proof-display-some-buffers-count 
+	 ((selectedbuf (nth (mod proof-display-some-buffers-count
 				 numassoc) assocbufs))
 	  (nextbuf     (nth (mod (1+ proof-display-some-buffers-count)
 				 numassoc) assocbufs)))
@@ -76,7 +76,7 @@ without adjusting window layout."
 
 ;;;###autoload
 (defun proof-menu-define-keys (map)
-  ;; Prover specific keymap under C-c C-a 
+  ;; Prover specific keymap under C-c C-a
   (proof-eval-when-ready-for-assistant
       (define-key map [(control c) (control a)] (proof-ass keymap)))
   ;; M-a and M-e are usually {forward,backward}-sentence.
@@ -102,14 +102,14 @@ without adjusting window layout."
   ;; C-c C-u is proof-undo-last-successful-command in universal-keys
   ;; C-c C-w is pg-response-clear-displays in universal-keys
   (define-key map [(control c) (control z)] 'proof-frob-locked-end)
-  (define-key map [(control c) (control backspace)] 
+  (define-key map [(control c) (control backspace)]
     'proof-undo-and-delete-last-successful-command)
   ;; C-c C-v is proof-minibuffer-cmd in universal-keys
   ;; C-c C-. is proof-goto-end-of-locked in universal-keys
   (define-key map [(control c) (control return)] 'proof-goto-point)
   (define-key map [(control c) v] 'pg-toggle-visibility)
   (define-key map [(control mouse-3)] 'proof-mouse-goto-point)
-  ;; NB: next binding overwrites comint-find-source-code.  
+  ;; NB: next binding overwrites comint-find-source-code.
   (define-key map [(meta p)] 'pg-previous-matching-input-from-input)
   (define-key map [(meta n)] 'pg-next-matching-input-from-input)
   ;; Standard binding for completion
@@ -133,8 +133,8 @@ without adjusting window layout."
 
 ;;;###autoload
 (defun proof-menu-define-main ()
-  (easy-menu-define 
-   proof-mode-menu  
+  (easy-menu-define
+   proof-mode-menu
    proof-mode-map
    "The main Proof General menu"
    (proof-main-menu)))
@@ -146,8 +146,8 @@ without adjusting window layout."
 
 ;;;###autoload
 (defun proof-menu-define-specific ()
-  (easy-menu-define 
-    proof-assistant-menu 
+  (easy-menu-define
+    proof-assistant-menu
     proof-mode-map
     (concat "The menu for " proof-assistant)
     (cons proof-assistant
@@ -205,8 +205,8 @@ without adjusting window layout."
 (defvar proof-help-menu
   '("Help"
     ["About PG"        proof-splash-display-screen t]
-    ["PG Info"      	(info "ProofGeneral") t]
-    ["PG Homepage"  	(browse-url proof-general-home-page) t]
+    ["PG Info"	(info "ProofGeneral") t]
+    ["PG Homepage"	(browse-url proof-general-home-page) t]
     ["Send Bug Report" proof-submit-bug-report t])
   "Proof General help menu.")
 
@@ -240,7 +240,7 @@ without adjusting window layout."
 	   (proof-switch-to-buffer proof-response-buffer t)
 	   :active (buffer-live-p proof-response-buffer)]
 	  ;; FIXME: next test doesn't work: menus are loaded before
-	  ;; proof-shell-trace-output-regexp is set (in proof-shell hook).  
+	  ;; proof-shell-trace-output-regexp is set (in proof-shell hook).
 	  ;; Should be better with simplified customization mechanism.
 	  ;; ( if proof-shell-trace-output-regexp ... )
 	  ["Trace"
@@ -250,7 +250,7 @@ without adjusting window layout."
 	   (proof-switch-to-buffer proof-shell-buffer)
 	   :active (buffer-live-p proof-shell-buffer)]))
   "Proof General buffer menu.")
-	  
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -274,17 +274,17 @@ without adjusting window layout."
 (proof-deftoggle proof-keep-response-history)
 
 (proof-eval-when-ready-for-assistant
-  (proof-deftoggle-fn 
+  (proof-deftoggle-fn
    (proof-ass-sym unicode-tokens-enable) 'proof-unicode-tokens-toggle)
-  (proof-deftoggle-fn 
+  (proof-deftoggle-fn
    (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle)
   (proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle))
 
 (defun proof-retract-on-edit-toggle ()
   (interactive)
-  (customize-set-variable 
+  (customize-set-variable
    'proof-strict-read-only
-   (if (eq proof-strict-read-only 'retract) 
+   (if (eq proof-strict-read-only 'retract)
        nil 'retract)))
 
 (defun proof-keep-response-history ()
@@ -296,7 +296,7 @@ without adjusting window layout."
 ;; Here is the menu
 
 (defconst proof-quick-opts-menu
-  (cons 
+  (cons
    "Options"
    `(["Electric Terminator" proof-electric-terminator-toggle
      :style toggle
@@ -311,7 +311,7 @@ without adjusting window layout."
       :style toggle
       :selected proof-full-annotation
       :help "Record full information to decorate scripts (may cause slowdown)"]
-     ["Disppearing Proofs" proof-disappearing-proofs-toggle 
+     ["Disppearing Proofs" proof-disappearing-proofs-toggle
       :style toggle
       :selected proof-disappearing-proofs
       :help "Hide proofs as they are completed"]
@@ -326,44 +326,44 @@ without adjusting window layout."
       :selected (eq proof-strict-read-only 'retract)
       :active (not (eq proof-strict-read-only t))
       :help "Automaticall retract on edit in processed region"]
-     
-     ["Unicode Tokens" 
+
+     ["Unicode Tokens"
       (proof-unicode-tokens-toggle (if (boundp 'unicode-tokens-mode)
 				       (if unicode-tokens-mode 0 1) 1))
       :active (proof-unicode-tokens-support-available)
       :style toggle
-      :selected (and (boundp 'unicode-tokens-mode) 
+      :selected (and (boundp 'unicode-tokens-mode)
 		     unicode-tokens-mode)
       :help "Enable display of tokens as Unicode characters"]
 
-     ["Unicode Maths Menu" 
+     ["Unicode Maths Menu"
       (proof-maths-menu-toggle (if (boundp 'maths-menu-mode)
 				       (if maths-menu-mode 0 1) 1))
       :active (proof-maths-menu-support-available)
       :style toggle
       :selected (and (boundp 'maths-menu-mode) maths-menu-mode)
       :help "Maths menu for inserting Unicode characters"]
- 
+
      ["Multiple Modes" (proof-mmm-toggle (if mmm-mode 0 1))
       :active (proof-mmm-support-available)
       :style toggle
       :selected (and (boundp 'mmm-mode) mmm-mode)
       :help "Allow multiple major modes"]
- 
+
      ["Toolbar" proof-toolbar-toggle
       ;; should really be split into :active & GNU Emacs's :visible
       :active (and (or (featurep 'toolbar) (featurep 'tool-bar))
 			 (boundp 'proof-buffer-type)
 			 ;; only allow toggling of toolbar enable in one
 			 ;; buffer to avoid strange effects because we
-			 ;; only keep one flag.  (Strange effects because 
+			 ;; only keep one flag.  (Strange effects because
 			 ;; we only turn it off in one buffer at a time)
 			 (eq proof-buffer-type 'script))
       :style toggle
       :selected proof-toolbar-enable
       :help "Use the Proof General toolbar"]
 
-;;; TODO: Add this in PG 3.7.1 once; see trac #169 
+;;; TODO: Add this in PG 3.7.1 once; see trac #169
 ;;;      ["Response history" proof-keep-response-history-toggle
 ;;;       :style toggle
 ;;;       :selected proof-keep-response-history]
@@ -413,41 +413,41 @@ without adjusting window layout."
        :style toggle
        :selected proof-colour-locked
        :help "Use decoration of locked region"])
-     ("Follow Mode" 
-      ["Follow Locked Region" 
+     ("Follow Mode"
+      ["Follow Locked Region"
        (customize-set-variable 'proof-follow-mode 'locked)
        :style radio
        :selected (eq proof-follow-mode 'locked)
        :help "Point follows the locked region"]
 ;; Not implemented.  See Trac #187
-;;       ["Follow On Success" 
+;;       ["Follow On Success"
 ;;        (customize-set-variable 'proof-follow-mode 'followsuccess)
 ;;        :style radio
 ;;        :selected (eq proof-follow-mode 'followdown)]
-      ["Follow Locked Region Down" 
+      ["Follow Locked Region Down"
        (customize-set-variable 'proof-follow-mode 'followdown)
        :style radio
        :selected (eq proof-follow-mode 'followdown)
        :help "Point follows the locked region when processsing"]
-      ["Keep Locked Region Displayed" 
+      ["Keep Locked Region Displayed"
        (customize-set-variable 'proof-follow-mode 'follow)
        :style radio
        :selected (eq proof-follow-mode 'follow)
        :help "Scroll to ensure end of lock region is visible"]
-      ["Never Move" 
+      ["Never Move"
        (customize-set-variable 'proof-follow-mode 'ignore)
        :style radio
        :selected (eq proof-follow-mode 'ignore)
        :help "Do not move cursor during processing"])
      ;; Add this because it's a handy one to set (usually to retract)
      ("Deactivate Action"
-      ["Retract" 
-       (customize-set-variable 'proof-auto-action-when-deactivating-scripting 
+      ["Retract"
+       (customize-set-variable 'proof-auto-action-when-deactivating-scripting
 			       'retract)
        :style radio
        :selected (eq proof-auto-action-when-deactivating-scripting 'retract)]
-      ["Process" 
-       (customize-set-variable 'proof-auto-action-when-deactivating-scripting 
+      ["Process"
+       (customize-set-variable 'proof-auto-action-when-deactivating-scripting
 			       'process)
        :style radio
        :selected (eq proof-auto-action-when-deactivating-scripting 'process)]
@@ -456,9 +456,9 @@ without adjusting window layout."
        :style radio
        :selected (null proof-auto-action-when-deactivating-scripting)])
      "----"
-     ["Reset Options" (proof-quick-opts-reset) 
+     ["Reset Options" (proof-quick-opts-reset)
       (proof-quick-opts-changed-from-defaults-p)]
-     ["Save Options" (proof-quick-opts-save) 
+     ["Save Options" (proof-quick-opts-save)
       (proof-quick-opts-changed-from-saved-p)]))
   "Proof General quick options.")
 
@@ -467,9 +467,8 @@ without adjusting window layout."
   (list
    'proof-electric-terminator-enable
    'proof-script-fly-past-comments
-   'proof-disappearing-proofs 
+   'proof-disappearing-proofs
    'proof-full-annotation
-   ;;'proof-output-fontify-enable
    'proof-strict-read-only
    (proof-ass-sym unicode-tokens-enable)
    (proof-ass-sym maths-menu-enable)
@@ -499,7 +498,7 @@ without adjusting window layout."
   t)
 
 
-;; 
+;;
 ;; We have menu items for saving options and reseting them.
 ;; We could just store the settings automatically (no save),
 ;; but then the reset option would have to change to restore
@@ -542,7 +541,7 @@ without adjusting window layout."
   "Advanced sub-menu of script functions and customize.")
 
 
-(defvar proof-menu  
+(defvar proof-menu
   '(["Next Error" proof-next-error
      :active pg-next-error-regexp]
     ["Scripting Active" proof-toggle-active-scripting
@@ -564,7 +563,7 @@ without adjusting window layout."
 ;;;###autoload
 (defun proof-aux-menu ()
   "Construct and return PG auxiliary menu used in non-scripting buffers."
-  (cons proof-general-name 
+  (cons proof-general-name
 	(append
 	 (proof-toolbar-scripting-menu)
 	 proof-config-menu
@@ -584,18 +583,18 @@ without adjusting window layout."
     (while favs
       (setq ents (cons (apply 'proof-def-favourite (car favs)) ents))
       (setq favs (cdr favs)))
-    (setq proof-menu-favourites 
-	  (list 
-	   (cons "Favourites" 
+    (setq proof-menu-favourites
+	  (list
+	   (cons "Favourites"
 		 (append ents
 			 ;; (list "----")  doesn't work for adding before
-			 '(["Add Favourite" 
+			 '(["Add Favourite"
 			    (call-interactively 'proof-add-favourite) t]
-			   ["Delete Favourite" 
+			   ["Delete Favourite"
 			    (call-interactively 'proof-del-favourite) t]
 			   ["Save Favourites"
 			    (proof-save-favourites) t])))))))
-  
+
 ;;; Define stuff from favourites
 
 (defun proof-def-favourite (command inscript menuname &optional key new)
@@ -603,7 +602,7 @@ without adjusting window layout."
 See doc of `proof-add-favourite' for first four arguments.
 Extra NEW flag means that this should be a new favourite, so check
 that function defined is not already bound.
-This function defines a function and returns a menu entry 
+This function defines a function and returns a menu entry
 suitable for adding to the proof assistant menu."
   (let* ((menunames	(split-string (downcase menuname)))
 	 (menuname-sym  (proof-sym (proof-splice-separator "-" menunames)))
@@ -636,46 +635,46 @@ suitable for adding to the proof assistant menu."
   "Delete \"favourite\" command recorded at MENUNAME."
   (interactive
    (list
-    (completing-read "Menu item to delete: " 
+    (completing-read "Menu item to delete: "
 		     (mapcar 'cddr (proof-ass favourites))
 		     nil t)))
   (let*
       ((favs       (proof-ass favourites))
-       (rmfavs	   (remove-if 
+       (rmfavs	   (remove-if
 		    (lambda (f) (string-equal menuname (caddr f)))
 		    favs)))
     (unless (equal favs rmfavs)
-      (easy-menu-remove-item proof-assistant-menu 
+      (easy-menu-remove-item proof-assistant-menu
 			     '("Favourites") menuname)
       (customize-set-variable  (proof-ass-sym favourites) rmfavs))))
-  
+
 (defun proof-read-favourite ()
-  (let* 
+  (let*
       ((guess  (buffer-substring (save-excursion
 				   (beginning-of-line-text)
 				   (point)) (point)))
        (cmd (read-string
-	     (concat "Command to send to " proof-assistant ": ") 
+	     (concat "Command to send to " proof-assistant ": ")
 	     guess
 	     proof-make-favourite-cmd-history))
        (ins (y-or-n-p "Should command be recorded in script? "))
        (men (read-string
-	     "Name of command on menu: " 
+	     "Name of command on menu: "
 	     cmd
 	     proof-make-favourite-menu-history))
        (key (if (y-or-n-p "Set a keybinding for this command? : ")
 		;; FIXME: better validation here would be to check
 		;; this is a new binding, or remove old binding below.
-		 (read-key-sequence 
-		  "Type the key to use (binding will be C-c C-a <key>): " 
+		 (read-key-sequence
+		  "Type the key to use (binding will be C-c C-a <key>): "
 		  nil t))))
     ;; result
     (list cmd ins men key)))
-	  
+
 
 (defun proof-add-favourite (command inscript menuname &optional key)
   "Define and add a \"favourite\" proof-assisant function to the menu bar.
-The favourite function will issue COMMAND to the proof assistant.  
+The favourite function will issue COMMAND to the proof assistant.
 COMMAND is inserted into script (not sent immediately) if INSCRIPT non-nil.
 MENUNAME is the name of the function for the menu.
 KEY is the optional key binding."
@@ -683,15 +682,15 @@ KEY is the optional key binding."
   (let*
       ((menu-entry (proof-def-favourite command inscript menuname key t))
        (favs       (proof-ass favourites))
-       (rmfavs	   (remove-if 
+       (rmfavs	   (remove-if
 		    (lambda (f) (string-equal menuname (caddr f)))
 		    favs))
-       (newfavs    (append 
-		    rmfavs 
+       (newfavs    (append
+		    rmfavs
 		    (list (list command inscript menuname key)))))
     ;; If def succeeds, add to customize var
     (customize-set-variable  (proof-ass-sym favourites) newfavs)
-    (easy-menu-add-item proof-assistant-menu 
+    (easy-menu-add-item proof-assistant-menu
 			'("Favourites") menu-entry "Add Favourite")))
 
 
@@ -707,7 +706,7 @@ KEY is the optional key binding."
   "Return menu generated from `proof-assistant-settings', update `proof-menu-settings'."
   (if proof-assistant-settings
       (let ((save  (list "----"
-			 ["Reset Settings" (proof-settings-reset) 
+			 ["Reset Settings" (proof-settings-reset)
 			  (proof-settings-changed-from-defaults-p)]
 			 ["Save Settings" (proof-settings-save)
 			  (proof-settings-changed-from-saved-p)]))
@@ -715,7 +714,7 @@ KEY is the optional key binding."
 	(mapc (lambda (stg) (add-to-list 'groups (get (car stg) 'pggroup)))
 	      proof-assistant-settings)
 	(dolist (grp (reverse groups))
-	  (let* ((gstgs (mapcan (lambda (stg) 
+	  (let* ((gstgs (mapcan (lambda (stg)
 				  (if (eq (get (car stg) 'pggroup) grp)
 				      (list stg)))
 				proof-assistant-settings))
@@ -724,17 +723,17 @@ KEY is the optional key binding."
 				gstgs)))
 	    (setq ents
 		  (if grp (cons (cons grp cmds) ents)
-		    (append cmds 
+		    (append cmds
 			    (if (> (length groups) 1) '("----"))
 			    ents)))))
 	;; (while setgs
-	;;   (setq ents (cons 
-	;; 	      (apply 'proof-menu-entry-for-setting (car setgs)) ents))
+	;;   (setq ents (cons
+	;;	      (apply 'proof-menu-entry-for-setting (car setgs)) ents))
 	;;   (setq setgs (cdr setgs)))
-	(setq proof-menu-settings 
-	      (list (cons "Settings" 
+	(setq proof-menu-settings
+	      (list (cons "Settings"
 			  (nconc ents save)))))))
-		  
+
 
 (defun proof-menu-entry-name (symbol)
   "Return a nice menu entry name for SYMBOL."
@@ -743,7 +742,7 @@ KEY is the optional key binding."
     (upcase-initials
      (replace-regexp-in-string "-" " "
       ;; strip the group name from the menu entry name.
-      (if grp (replace-regexp-in-string (concat (downcase grp) ":") "" nm) 
+      (if grp (replace-regexp-in-string (concat (downcase grp) ":") "" nm)
 	nm)))))
 
 (defun proof-menu-entry-for-setting (symbol setting type descr)
@@ -751,17 +750,17 @@ KEY is the optional key binding."
 	(pasym	     (proof-ass-symv symbol)))
     (cond
      ((eq type 'boolean)
-      (vector entry-name 
+      (vector entry-name
 	      (proof-deftoggle-fn pasym)
 	      :style 'toggle
 	      :selected pasym
 	      :help descr))
      ((eq type 'integer)
-      (vector entry-name 
+      (vector entry-name
 	      (proof-defintset-fn pasym)
 	      :help descr))
      ((eq type 'string)
-      (vector entry-name 
+      (vector entry-name
 	      (proof-defstringset-fn pasym)
 	      :help descr)))))
 
@@ -794,7 +793,7 @@ KEY is the optional key binding."
   "As for macro `defpacustom' but evaluating arguments."
   (let (newargs setting evalform type descr)
     (while args
-      (cond 
+      (cond
        ((eq (car args) :setting)
 	(setq setting (cadr args))
 	(setq args (cdr args)))
@@ -802,11 +801,11 @@ KEY is the optional key binding."
 	(setq evalform (cadr args))
 	(setq args (cdr args)))
        ((eq (car args) :pgipcmd)
-	;; Construct a function which yields a PGIP string 
-	(setq setting `(lambda (x) 
+	;; Construct a function which yields a PGIP string
+	(setq setting `(lambda (x)
 			  (pg-pgip-string-of-command (proof-assistant-format ,(cadr args) x))))
 	(setq args (cdr args)))
-       ((eq (car args) :pggroup) 
+       ((eq (car args) :pggroup)
 	;; use the group as a prefix to the name, and set a pggroup property on it
 	(setq name (intern (concat (downcase (cadr args)) ":" (symbol-name name))))
 	(put name 'pggroup (cadr args))
@@ -821,15 +820,15 @@ KEY is the optional key binding."
     (setq newargs (reverse newargs))
     (setq descr (car-safe newargs))
     (unless (and type
-		  (or (eq (eval type) 'boolean) 
-		      (eq (eval type) 'integer) 
+		  (or (eq (eval type) 'boolean)
+		      (eq (eval type) 'integer)
 		      (eq (eval type) 'string)))
       (error "defpacustom: missing :type keyword or wrong :type value"))
     ;; Debug message in case a defpacustom is repeated.
     ;; NB: this *may* happen dynamically, but shouldn't: if the
     ;; interface queries the prover for the settings it supports,
     ;; then the internal list should be cleared first.
-    ;; FIXME: for now, we support redefinitions, by calling 
+    ;; FIXME: for now, we support redefinitions, by calling
     ;; pg-custom-undeclare-variable.
     (if (assoc name proof-assistant-settings)
 	(progn
@@ -852,7 +851,7 @@ KEY is the optional key binding."
 	  (proof-assistant-invisible-command-ifposs
 	   (proof-assistant-settings-cmd (quote ,name)))))))
     (setq proof-assistant-settings
-	  (cons (list name setting (eval type) descr) 
+	  (cons (list name setting (eval type) descr)
 		(assq-delete-all name proof-assistant-settings)))))
 
 ;;;###autoload
@@ -881,13 +880,13 @@ evaluate can be provided instead."
   (if (proof-shell-available-p)
       (progn
 	(proof-shell-invisible-command cmd t)
-	;; refresh display, 
+	;; refresh display,
 	;; FIXME: should only do if goals display is active,
-	;; messy otherwise. 
-	;; (we need a new flag for "active goals display").  
+	;; messy otherwise.
+	;; (we need a new flag for "active goals display").
 	;; PG 3.5 (patch 22.04.04):
 	;; Let's approximate that by looking at proof-nesting-depth.
-	(if (and proof-showproof-command 
+	(if (and proof-showproof-command
 		 (> proof-nesting-depth 0))
 	    (proof-shell-invisible-command proof-showproof-command))
 	;;  Could also repeat last command if non-state destroying.
@@ -897,26 +896,26 @@ evaluate can be provided instead."
   "If `proof-use-pgip-askprefs' is non-nil, try to issue <askprefs>"
   (if (and proof-use-pgip-askprefs proof-shell-issue-pgip-cmd)
       (pg-pgip-askprefs)))
-  
+
 
 (defun proof-assistant-settings-cmd (&optional setting)
   "Return string for settings kept in Proof General customizations.
-If SETTING is non-nil, return a string for just that setting. 
+If SETTING is non-nil, return a string for just that setting.
 Otherwise return a string for configuring all settings.
 NB: if no settings are configured, this has no effect."
   (if proof-assistant-settings
       (let
 	  ((evalifneeded (lambda (expr)
 			   (if (and (cadr expr) ;; setting has PA string?
-				    (or (not setting) 
+				    (or (not setting)
 					(eq setting (car expr))))
-			       (proof-assistant-format 
-				(cadr expr) 
+			       (proof-assistant-format
+				(cadr expr)
 				(eval (proof-ass-symv (car expr))))))))
-	(apply 'concat (mapcar evalifneeded 
+	(apply 'concat (mapcar evalifneeded
 			       proof-assistant-settings)))))
 
-(defvar proof-assistant-format-table 
+(defvar proof-assistant-format-table
   (list
    (cons "%b" '(proof-assistant-format-bool curvalue))
    (cons "%i" '(proof-assistant-format-int curvalue))
@@ -940,7 +939,7 @@ Formatting suitable for current proof assistant, controlled by
 Finally, apply `proof-assistant-setting-format' if non-nil.
 Alternatively, STRING can be a function which yields a string when applied
 to the CURVALUE.
-As another special case for boolean settings: the setting STRING 
+As another special case for boolean settings: the setting STRING
 can be a cons cell of two strings, the first one for true (non-nil
 value) and the second for false."
   (let ((setting
diff --git a/generic/proof-mmm.el b/generic/proof-mmm.el
index b1ebf9e7..f937975a 100644
--- a/generic/proof-mmm.el
+++ b/generic/proof-mmm.el
@@ -51,7 +51,7 @@
     ;; make sure MMM obeys the mmm-mode-ext-classes-alist
     (unless (eq mmm-global-mode t)
       (setq mmm-global-mode 'pg-use-mode-ext-classes-alist))))
-  
+
 ;;;###autoload
 (defun proof-mmm-enable ()
   "Turn on or off MMM mode in Proof General script buffer.
diff --git a/generic/proof-script.el b/generic/proof-script.el
index d21af2b6..7ab35069 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -273,7 +273,7 @@ Also clear list of script portions."
   (proof-map-buffers (proof-buffers-in-mode proof-mode-for-script)
    (and (span-live-p proof-locked-span)
     (if proof-colour-locked
-  	   (span-set-property proof-locked-span 'face 'proof-locked-face)
+	   (span-set-property proof-locked-span 'face 'proof-locked-face)
       (span-set-property  proof-locked-span 'face nil)))))
 
 ;; ** Restarting and clearing spans
@@ -746,7 +746,7 @@ to allow other files loaded by proof assistants to be marked read-only."
 ;; complicated for retracting, because we allow a hook function
 ;; to calculate the new included files list.
 
-(defun proof-register-possibly-new-processed-file 
+(defun proof-register-possibly-new-processed-file
   (file &optional informprover noquestions)
   "Register a possibly new FILE as having been processed by the prover.
 
@@ -1178,7 +1178,7 @@ activation is considered to have failed and an error is given."
 	    (set-buffer-modified-p nil)
 	    (unwind-protect
 		(save-some-buffers)
- 	      (set-buffer-modified-p modified))))
+	      (set-buffer-modified-p modified))))
 
       ;; Run hooks with a variable which suggests whether or not
       ;; to block.   NB: The hook function may send commands to the
@@ -2105,12 +2105,12 @@ others)."
 	  (proof-set-queue-end start))
 	;; Try to clean input history (NB: rely on order here)
 ;; PG 3.7 release: disable this, it's not yet robust.
-;; 	(let ((cmds (spans-at-region-prop start end 'cmd))
-;; 	      (fn   (lambda (span)
-;; 		      (unless (eq (span-property span 'type) 'comment)
-;; 			(pg-remove-from-input-history
-;; 			 (span-property span 'cmd))))))
-;; 	  (mapc fn (reverse cmds)))
+;;	(let ((cmds (spans-at-region-prop start end 'cmd))
+;;	      (fn   (lambda (span)
+;;		      (unless (eq (span-property span 'type) 'comment)
+;;			(pg-remove-from-input-history
+;;			 (span-property span 'cmd))))))
+;;	  (mapc fn (reverse cmds)))
 
 	(proof-script-delete-spans start end)
 	(span-delete span)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index c967c58c..9d273f78 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -8,7 +8,7 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Mode for buffer which interacts with proof assistant.
 ;; Includes management of a queue of commands waiting to be sent.
 ;;
@@ -67,12 +67,12 @@ This is the string matched by `proof-shell-annotated-prompt-regexp'.")
   "A symbol denoting the type of the last output string from the proof system.
 Specifically:
 
- 'interrupt   	 An interrupt message
- 'error	      	 An error message
- 'abort	      	 A proof abort message
- 'loopback    	 A command sent from the PA to be inserted into the script
- 'response    	 A response message
- 'goals	      	 A goals (proof state) display
+ 'interrupt	 An interrupt message
+ 'error		 An error message
+ 'abort		 A proof abort message
+ 'loopback	 A command sent from the PA to be inserted into the script
+ 'response	 A response message
+ 'goals		 A goals (proof state) display
  'systemspecific Something specific to a particular system,
 		  -- see `proof-shell-classify-output-system-specific'
 
@@ -97,7 +97,7 @@ to examine `proof-shell-last-output'.")
 
 ;;
 ;; Indicator and fake minor mode for active scripting buffer
-;; 
+;;
 
 (defcustom proof-shell-active-scripting-indicator
   " Scripting"
@@ -141,7 +141,7 @@ of the queue region."
 ;;    mode for current (scripting) buffer.
 ;;
 ;; Also, a new enabler predicate:
-;;  
+;;
 ;;  proof-shell-available
 ;;    returns non-nil if a proof shell is active and not locked.
 ;;
@@ -235,7 +235,7 @@ Does nothing if proof assistant is already running."
       (if (and name proof-prog-name-guess proof-guess-command-line)
 	  (setq proof-prog-name
 		(apply proof-guess-command-line (list name)))))
-    
+
     (if proof-prog-name-ask
 	(save-excursion
 	  (setq proof-prog-name (read-shell-command "Run process: "
@@ -327,7 +327,7 @@ Does nothing if proof assistant is already running."
 
 	(apply 'scomint-make  (append (list proc (car prog-name-list) nil)
 				     (cdr prog-name-list)))
-	
+
 	(setq proof-shell-buffer (get-buffer (concat "*" proc "*")))
 
 	(unless (proof-shell-live-buffer)
@@ -355,7 +355,7 @@ Does nothing if proof assistant is already running."
 	      (proof-regexp-alt goals resp trace thms)))
 
       (with-current-buffer proof-shell-buffer
-	
+
 	(erase-buffer)
 
 	;; Set text representation (see CVS history for comments)
@@ -375,7 +375,7 @@ Does nothing if proof assistant is already running."
 	(set-buffer proof-response-buffer)
 	(proof-shell-set-text-representation)
 	(funcall proof-mode-for-response)
-	
+
 	(proof-with-current-buffer-if-exists proof-trace-buffer
 	  (proof-shell-set-text-representation)
 	  (funcall proof-mode-for-response)
@@ -406,7 +406,7 @@ Does nothing if proof assistant is already running."
 
 (defvar proof-shell-kill-function-hooks nil
   "Functions run from `proof-shell-kill-function'.")
-  
+
 (defun proof-shell-kill-function ()
   "Function run when a proof-shell buffer is killed.
 Try to shut down the proof process nicely and clear locked
@@ -488,12 +488,12 @@ shell buffer, alled by `proof-shell-bail-out' if process exits."
 	  (proof-delete-other-frames))
       ;; Kill buffers associated with shell buffer
       (let ((proof-shell-buffer nil)) ;; fool kill buffer hooks
- 	(dolist (buf '(proof-goals-buffer proof-response-buffer
+	(dolist (buf '(proof-goals-buffer proof-response-buffer
 					  proof-trace-buffer))
- 	  (if (buffer-live-p (symbol-value buf))
- 	      (progn
- 		(kill-buffer (symbol-value buf))
- 		(set buf nil)))))
+	  (if (buffer-live-p (symbol-value buf))
+	      (progn
+		(kill-buffer (symbol-value buf))
+		(set buf nil)))))
       (message "%s exited." bufname))))
 
 (defun proof-shell-clear-state ()
@@ -591,7 +591,7 @@ the output for this command.
 This is a subroutine of `proof-shell-handle-error'."
   (let (start end string)
     (with-current-buffer proof-shell-buffer
-      
+
       ;; NB: it's tempting to use proof-shell-last-output here which
       ;; already contains the text (change suggested by Stefan
       ;; Monnier), but characters have been stripped from that text
@@ -624,7 +624,7 @@ Optional argument PUSH is ignored."
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 
+;;
 ;; Processing error output
 ;;
 
@@ -662,7 +662,7 @@ Runs `proof-shell-error-or-interrupt-action'."
      ;;  (proof-display-and-keep-buffer proof-response-buffer)
      (proof-warning
       "Interrupt: script management may be in an inconsistent state
-           (but it's probably okay)")
+	   (but it's probably okay)")
      (setq proof-shell-interrupt-pending nil)
      (proof-shell-error-or-interrupt-action 'interrupt)))
 
@@ -712,12 +712,12 @@ This is a hook function for proof-shell-handle-delayed-output-hook."
 ;	 (and pos (set-window-point
 ;		   (get-buffer-window proof-goals-buffer t) pos)))))
 
-           
+
 (defsubst proof-shell-string-match-safe (regexp string)
   "Like string-match except returns nil if REGEXP is nil."
   (and regexp (string-match regexp string)))
 
-      
+
 (defun proof-shell-classify-output (cmd string)
   "Process shell output (resulting from CMD) by matching on STRING.
 CMD is the first part of the `proof-action-list' that lead to this
@@ -726,7 +726,7 @@ output.  The result of this function is a pair (SYMBOL NEWSTRING).
 Here is where we classify interrupts, abortions of proofs, errors,
 completions of proofs, and proof step hints (proof by pointing results).
 They are checked for in this order, using
- 
+
   `proof-shell-interrupt-regexp'
   `proof-shell-error-regexp'
   `proof-shell-abort-goal-regexp'
@@ -756,14 +756,14 @@ This function sets variables: `proof-shell-last-output',
    (cond
     ((proof-shell-string-match-safe proof-shell-interrupt-regexp string)
      (setq proof-shell-last-output-kind 'interrupt))
-    
+
     ((proof-shell-string-match-safe proof-shell-error-regexp string)
      (setq proof-shell-last-output-kind 'error))
-    
+
     ((proof-shell-string-match-safe proof-shell-abort-goal-regexp string)
      (proof-clean-buffer proof-goals-buffer)
      (setq proof-shell-last-output-kind 'abort))
-    
+
     ((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
@@ -792,18 +792,18 @@ This function sets variables: `proof-shell-last-output',
        ;;  doesn't markup goals output specially).
 ;; FIXME: try to remove this for PG 4.0
 ;;        (unless (and
-;; 		pg-subterm-first-special-char
-;; 		(not (string-equal
-;; 		      proof-shell-start-goals-regexp
-;; 		      (pg-assoc-strip-subterm-markup
-;; 		       proof-shell-start-goals-regexp))))
+;;		pg-subterm-first-special-char
+;;		(not (string-equal
+;;		      proof-shell-start-goals-regexp
+;;		      (pg-assoc-strip-subterm-markup
+;;		       proof-shell-start-goals-regexp))))
        (setq start (match-beginning 0))
        (setq end (if proof-shell-end-goals-regexp
 		     (string-match proof-shell-end-goals-regexp string start)
 		   (length string)))
        (setq proof-shell-last-output (substring string start end))
        (setq proof-shell-last-output-kind 'goals)))
-    
+
     ;; Test for a proof by pointing command hint
     ((proof-shell-string-match-safe proof-shell-result-start string)
      (let (start end)
@@ -813,7 +813,7 @@ This function sets variables: `proof-shell-last-output',
        ;; Only record the loopback command in the last output message
        (setq proof-shell-last-output (substring string start end)))
      (setq proof-shell-last-output-kind 'loopback))
-    
+
     ;; Hook to tailor proof-shell-classify-output to a specific proof
     ;; system, in the case that all the above matches fail.
     ((and proof-shell-classify-output-system-specific
@@ -873,7 +873,7 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*).
 	  (interrupt-process))
       ;; otherwise, interrupt the queue right here
       (proof-shell-error-or-interrupt-action 'interrupt))))
-      
+
 
 
 
@@ -903,7 +903,7 @@ used in `proof-append-alist' when we start processing a queue, and in
 `proof-shell-exec-loop', to process the next item."
   (with-current-buffer proof-shell-buffer
     (goto-char (point-max))
-    
+
     ;; Hook for munging `string' and other dirty hacks.
     (unless (or (null string)
 		(string-equal string "")
@@ -913,7 +913,7 @@ used in `proof-append-alist' when we start processing a queue, and in
     ;; Replace CRs from string with spaces to avoid spurious prompts.
     (if proof-shell-strip-crs-from-input
 	(setq string (subst-char-in-string ?\n ?\  string)))
-    
+
     (insert (or string ""))  ;; robust against call with nil
 
     ;; Advance the proof-marker, if synchronization has been gained.
@@ -982,7 +982,7 @@ track what happens in the proof queue."
 	  ;; queue processing more tricky.
 	  (>= (+ num (length proof-action-list))
 	     proof-shell-silent-threshold))))
-	      
+
 
 (defsubst proof-shell-invoke-callback (listitem)
   "From a `proof-action-list' entry, invoke the callback on the span."
@@ -1008,7 +1008,7 @@ being processed."
     (if (and (null alist) (null proof-action-list))
 	;; remove the queue (otherwise done in proof-shell-exec-loop)
 	(proof-detach-queue))
-	
+
     (if alist
 	(if proof-action-list
 	    (progn
@@ -1034,7 +1034,7 @@ being processed."
 	    (proof-grab-lock queuemode)
 	    (setq proof-shell-last-output-kind nil)
 	    (if (proof-shell-should-be-silent (length alist))
-		;; 
+		;;
 		(progn
 		  (setq proof-action-list
 			(list (proof-shell-start-silent-item)))
@@ -1087,10 +1087,10 @@ The return value is non-nil if the action list is now empty."
    (save-excursion
      (if proof-script-buffer		      ; switch to active script
 	 (set-buffer proof-script-buffer))
-     
+
      (let ((item  (car proof-action-list))
 	   (flags (nthcdr 3 (car proof-action-list))))
-       
+
        ;; invoke callback on just processed command
        (proof-shell-invoke-callback item)
        (setq proof-action-list (cdr proof-action-list))
@@ -1113,7 +1113,7 @@ The return value is non-nil if the action list is now empty."
 		   (cons (proof-shell-stop-silent-item)
 			 proof-action-list))
 	     (setq item (car proof-action-list))))
-       
+
        ;; deal with pending interrupts (which were sent but caused no prover error)
        (if proof-shell-interrupt-pending
 	   (progn
@@ -1123,14 +1123,14 @@ The return value is non-nil if the action list is now empty."
        (if proof-action-list
 	   ;; send the next command to the process.
 	   (proof-shell-insert (nth 1 item) (nth 2 item) (nth 0 item))
-	 
+
 	 ;; action list is empty, release lock and cleanup
 	 (proof-release-lock)
 	 (proof-detach-queue)
 	 (unless flags ; hint after a batch of scripting
 	   (pg-processing-complete-hint))
 	 (pg-finish-tracing-display))
-       
+
        (null proof-action-list)))))
 
 
@@ -1196,7 +1196,7 @@ MESSAGE should be a string annotated with
       (if (and quit-flag proof-action-list)
 	  (proof-interrupt-process)))
 
-       
+
      ;; CASE processing file: update known files list
      ((and proof-shell-process-file
 	   (string-match (car proof-shell-process-file) message))
@@ -1228,17 +1228,17 @@ MESSAGE should be a string annotated with
 	   ;; Otherwise, active scripting buffer has been retracted.
 	   (t
 	    (setq proof-script-buffer nil))))))
-     
+
      ;; CASE clear response: prover asks PG to clear response buffer
      ((and proof-shell-clear-response-regexp
 	   (string-match proof-shell-clear-response-regexp message))
       (pg-response-maybe-erase nil t t))
-     
+
      ;; CASE clear goals: prover asks PG to clear goals buffer
      ((and proof-shell-clear-goals-regexp
 	   (string-match proof-shell-clear-goals-regexp message))
       (proof-clean-buffer proof-goals-buffer))
-   
+
      ;; 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))
@@ -1254,7 +1254,7 @@ MESSAGE should be a string annotated with
 	       "lisp error when obeying proof-shell-set-elisp-variable: \n"
 	       "setting `" variable "'\n to: \n"
 	       expr "\n"))))))
-     
+
      ;; CASE PGIP message from proof assistant.
      ((and proof-shell-match-pgip-cmd
 	   (string-match proof-shell-match-pgip-cmd message))
@@ -1267,7 +1267,7 @@ MESSAGE should be a string annotated with
       (let
 	  ((parsed-pgip  (pg-xml-parse-string message)))
 	(pg-pgip-process-packet parsed-pgip)))
-     
+
      ;; CASE theorem dependency: prover lists thms used in last proof
      ((and proof-shell-theorem-dependency-list-regexp
 	   (string-match proof-shell-theorem-dependency-list-regexp message))
@@ -1280,7 +1280,7 @@ MESSAGE should be a string annotated with
 	       (split-string deps
 			     proof-shell-theorem-dependency-list-split)))))
 
-	   
+
      (t
       ;; CASE everything else.  We're about to display a message.
       ;; Clear the response buffer this time, but not next, leave window.
@@ -1431,11 +1431,11 @@ is only changed when input is sent in `proof-shell-insert'."
 			(proof-shell-filter-manage-output "")))))
 	  ;; Now we're looking for the end of the piece of output
 	  ;; 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
 	  ;; there's more than one bit there.
-	  
+
 	  (if proof-action-list
 	      ;; We were expecting some output, examine it.
 	      (let ((urgnt    (marker-position
@@ -1678,7 +1678,7 @@ Only works when system timer has microsecond count available."
 	       (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))
 		  pg-fast-tracing-mode-threshold))
 	  ;; quickly consecutive and large tracing outputs: go into slow mode
@@ -1800,7 +1800,7 @@ Error messages are displayed as usual."
   (proof-shell-invisible-command cmd 'waitforit
 				 nil
 				 'no-response-display))
-  
+
 
 
 
@@ -1817,12 +1817,12 @@ Error messages are displayed as usual."
   "proof-shell" "Proof General shell mode class for proof assistant processes"
 
   (setq proof-buffer-type 'shell)
-  
+
   (proof-shell-clear-state)
 
   (buffer-disable-undo)
 
-  ;; scomint customisation. 
+  ;; scomint customisation.
 
   (setq scomint-output-filter-functions '(proof-shell-filter))
 
@@ -1894,7 +1894,7 @@ processing."
 	    (setq proof-action-list nil)
 	    ;; Send main intitialization command and wait for it to be
 	    ;; processed.
-	    
+
 	    ;; First, if the prover supports PGIP and preferences are
 	    ;; not configured, we may configure them.  (NB: this
 	    ;; assumes that PGIP provers are ready-to-go, without
@@ -1902,7 +1902,7 @@ processing."
 	    ;; so that user preferences may be then set sensibly in
 	    ;; the next step.
 	    (proof-maybe-askprefs)
-	    
+
 	    ;; Now send the initialisation commands.
 	    (unwind-protect
 		(progn
diff --git a/generic/proof-site.el b/generic/proof-site.el
index af59ff34..2bbb01f8 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -1,7 +1,7 @@
 ;; proof-site.el -- Loading stubs for Proof General.
 ;;		    Configuration for site and choice of provers.
 ;;
-;; Copyright (C) 1998-2003 LFCS Edinburgh. 
+;; Copyright (C) 1998-2003 LFCS Edinburgh.
 ;; Author:      David Aspinall <David.Aspinall@ed.ac.uk>
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -10,13 +10,13 @@
 ;; NB: Normally users do not need to edit this file.  Developers/installers
 ;; may want to adjust proof-assistant-table-default below.
 ;;
-;; The environment variables PROOFGENERAL_HOME and PROOFGENERAL_ASSISTANTS 
+;; The environment variables PROOFGENERAL_HOME and PROOFGENERAL_ASSISTANTS
 ;; can be set to affect load behaviour; see info documentation.
 ;;
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Master table of supported proof assistants. 
+;; Master table of supported proof assistants.
 ;;
 
 (defconst proof-assistant-table-default
@@ -28,17 +28,17 @@
 
       ;; For the demonstration instance of Proof General,
       ;; uncomment line below and set
-      ;; export PROOFGENERAL_ASSISTANTS=demoisa. 
+      ;; export PROOFGENERAL_ASSISTANTS=demoisa.
       ;; [NB: this is obsolete, only for old Isabelle files]a
       ;; (demoisa    "Isabelle Demo"	"\\.ML$")
-      
+
       ;; The following provers are not fully supported, and have only
       ;; preliminary support written (please help to improve them!)
-      
+
       ;; To use HOL, uncomment the line below.  It's disabled
       ;; by default because of clash with SML mode (same for .ML above).
       ;; (hol98	"HOL"		"\\.sml$")
-      
+
       ;; (acl2	"ACL2"		"\\.acl2$")
       ;; (twelf	"Twelf"		"\\.elf$")
       (plastic	"Plastic"	"\\.lf$")
@@ -57,7 +57,7 @@
   (defconst proof-general-version "Proof General Version 4.0pre090902. Released by da."
     "Version string identifying Proof General release."))
 
-(defconst proof-general-short-version 
+(defconst proof-general-short-version
   (eval-when-compile
     (progn
       (string-match "Version \\([^ ]+\\)\\." proof-general-version)
@@ -93,7 +93,7 @@
   (let ((s (getenv  "PROOFGENERAL_HOME")))
     (if s
 	(if (string-match "/$" s) s (concat s "/"))
-      (let ((curdir 
+      (let ((curdir
 	     (or
 	      (and load-in-progress (file-name-directory load-file-name))
 	      (file-name-directory (buffer-file-name)))))
@@ -102,7 +102,7 @@
 (defcustom proof-home-directory
   (proof-home-directory-fn)
   "Directory where Proof General is installed.  Ends with slash.
-Default value taken from environment variable `PROOFGENERAL_HOME' if set, 
+Default value taken from environment variable `PROOFGENERAL_HOME' if set,
 otherwise based on where the file `proof-site.el' was loaded from.
 You can use customize to set this variable."
   :type 'directory
@@ -139,12 +139,12 @@ You can use customize to set this variable."
       (add-to-list 'Info-default-directory-list proof-info-directory)))
 
 (defcustom proof-assistant-table
-  (apply 
+  (apply
    'append
    (mapcar
     ;; Discard entries whose directories have been removed.
     (lambda (dne)
-      (let ((atts (file-attributes (concat proof-home-directory 
+      (let ((atts (file-attributes (concat proof-home-directory
 					   (symbol-name (car dne))))))
 	(if (and atts (eq 't (car atts)))
 	    (list dne)
@@ -164,7 +164,7 @@ The SYMBOL is used to form the name of the mode for the
 assistant, `SYMBOL-mode', run when files with AUTOMODE-REGEXP
 are visited.  SYMBOL is also used to form the name of the
 directory and elisp file for the mode, which will be
- 
+
     PROOF-HOME-DIRECTORY/SYMBOL/SYMBOL.el
 
 where PROOF-HOME-DIRECTORY is the value of the
@@ -176,10 +176,10 @@ variable `proof-home-directory'."
 (defcustom proof-assistants nil
   (concat
    "*Choice of proof assistants to use with Proof General.
-A list of symbols chosen from:" 
-   (apply 'concat (mapcar (lambda (astnt) 
+A list of symbols chosen from:"
+   (apply 'concat (mapcar (lambda (astnt)
 			    (concat " '" (symbol-name (car astnt))))
-			  proof-assistant-table)) 
+			  proof-assistant-table))
 ".\nIf nil, the default will be ALL available proof assistants.
 
 Each proof assistant defines its own instance of Proof General,
@@ -195,12 +195,13 @@ symbols you want, for example \"lego isa\".  Or you can
 edit the file `proof-site.el' itself.
 
 Note: to change proof assistant, you must start a new Emacs session.")
-  :type (cons 'set 
+  :type (cons 'set
 	      (mapcar (lambda (astnt)
 			(list 'const ':tag (car (cdr astnt)) (car astnt)))
 		      proof-assistant-table))
   :group 'proof-general)
 
+;;;###autoload
 (defun proof-ready-for-assistant (assistantsym &optional assistant-name)
   "Configure PG for symbol ASSISTANTSYM, name ASSISTANT-NAME.
 If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
@@ -208,11 +209,11 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
     (let*
       ((sname		 (symbol-name assistantsym))
        (assistant-name   (or assistant-name
-			     (car-safe 
+			     (car-safe
 			      (cdr-safe (assoc assistantsym
 					       proof-assistant-table)))
 			     sname))
-       (cusgrp-rt	 
+       (cusgrp-rt
 	;; Normalized a bit to remove spaces and funny characters
 	(replace-regexp-in-string "/\\|[ \t]+" "-" (downcase assistant-name)))
        (cusgrp	      (intern cusgrp-rt))
@@ -231,7 +232,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
 		  assistant-name " configuration.")
 	 :group 'proof-general-internals
 	 :prefix ,(concat sname "-"))
-    
+
        ;; Set the proof-assistant configuration variables
        ;; NB: tempting to use customize-set-variable: wrong!
        ;; Here we treat customize as extended docs for these
@@ -240,7 +241,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
        (setq proof-assistant-internals-cusgrp (quote ,cus-internals))
        (setq proof-assistant ,assistant-name)
        (setq proof-assistant-symbol (quote ,assistantsym))
-       ;; define the per-prover settings which depend on above 
+       ;; define the per-prover settings which depend on above
        (require 'pg-custom)
        (setq proof-mode-for-shell (proof-ass-sym shell-mode))
        (setq proof-mode-for-response (proof-ass-sym response-mode))
@@ -253,21 +254,21 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
        (run-hooks 'proof-ready-for-assistant-hook))))))
 
 
-;; Add auto-loads and load-path elements to support the 
+;; Add auto-loads and load-path elements to support the
 ;; proof assistants selected, and define stub major mode functions
 (let ((assistants
        (or (mapcar 'intern (split-string (or (getenv "PROOFGENERAL_ASSISTANTS") "")))
 	   proof-assistants
 	   (mapcar (lambda (astnt) (car astnt)) proof-assistant-table))))
   (while assistants
-    (let*  
+    (let*
 	((assistant (car assistants))	; compiler bogus warning here
-	 (nameregexp			
-	  (or 
-	   (cdr-safe 
+	 (nameregexp
+	  (or
+	   (cdr-safe
 	    (assoc assistant
 		   proof-assistant-table))
-	   (error "Symbol %s is not in proof-assistant-table (in proof-site)" 
+	   (error "Symbol %s is not in proof-assistant-table (in proof-site)"
 		  (symbol-name assistant))))
 	 (assistant-name (car nameregexp))
 	 (regexp	 (car (cdr nameregexp)))
@@ -277,7 +278,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
 	 ;; NB: Mode name for each prover is <symbol name>-mode!
 	 (proofgen-mode  (intern (concat sname "-mode")))
 	 ;; NB: Customization group for each prover is its l.c.'d name!
-	 
+
 	 ;; Stub to initialize and load specific code.
 	 (mode-stub
 	  `(lambda ()
@@ -286,7 +287,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
 	       assistant-name
 	       ".\nThis is a stub which loads the real function.")
 	     (interactive)
-	     ;; Stop loading if proof-assistant is already set: 
+	     ;; Stop loading if proof-assistant is already set:
 	     ;; cannot work for more than one prover.
 	     (cond
 	      ((and (boundp 'proof-assistant)
@@ -294,23 +295,23 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
 	       (or (string-equal proof-assistant ,assistant-name)
 		   ;; If Proof General was partially loaded last time
 		   ;; and mode function wasn't redefined, be silent.
-		   (message 
-		    (concat 
-		     ,assistant-name 
+		   (message
+		    (concat
+		     ,assistant-name
 		     " Proof General error: Proof General already in use for "
 		     proof-assistant))))
 	      (t
 	       ;; prepare variables and load path
 	       (proof-ready-for-assistant (quote ,assistant) ,assistant-name)
-	       ;; load the real mode and invoke it. 
+	       ;; load the real mode and invoke it.
 	       (load-library ,elisp-file)
 	       (,proofgen-mode))))))
-	
-	(setq auto-mode-alist 
+
+	(setq auto-mode-alist
 	      (cons (cons regexp proofgen-mode) auto-mode-alist))
-	
+
 	(fset proofgen-mode mode-stub)
-	
+
 	(setq assistants (cdr assistants)))))
 
 (provide 'proof-site)
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 52db7f79..1a558857 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -1,6 +1,6 @@
 ;; proof-splash.el -- Splash welcome screen for Proof General
 ;;
-;; Copyright (C) 1998-2005 LFCS Edinburgh. 
+;; Copyright (C) 1998-2005 LFCS Edinburgh.
 ;; Author:    David Aspinall
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -11,7 +11,7 @@
 (require 'proof-site)
 
 ;;
-;; Customization of splash screen 
+;; Customization of splash screen
 ;;
 
 (defcustom proof-splash-enable t
@@ -22,7 +22,7 @@
 (defcustom proof-splash-time 3
   "Minimum number of seconds to display splash screen for.
 The splash screen may be displayed for a wee while longer than
-this, depending on how long it takes the machine to initialise 
+this, depending on how long it takes the machine to initialise
 Proof General."
   :type 'number
   :group 'proof-general-internals)
@@ -62,12 +62,12 @@ Proof General."
     )
   "Evaluated to configure splash screen displayed when entering Proof General.
 A list of the screen contents.  If an element is a string or an image
-specifier, it is displayed centred on the window on its own line.  
+specifier, it is displayed centred on the window on its own line.
 If it is nil, a new line is inserted."
   :type 'sexp
   :group 'proof-general-internals)
 
-(defconst proof-splash-startup-msg 
+(defconst proof-splash-startup-msg
   '(if (featurep 'proof-config) nil
      ;; Display additional hint if we guess we're being loaded
      ;; by shell script rather than find-file.
@@ -118,7 +118,7 @@ DEFAULT gives return value in case image not valid."
 Borrowed from startup-center-spaces."
   (let* ((avg-pixwidth     (round (/ (frame-pixel-width) (frame-width))))
 	 (fill-area-width  (* avg-pixwidth (- fill-column left-margin)))
-	 (glyph-pixwidth   (cond ((stringp glyph) 
+	 (glyph-pixwidth   (cond ((stringp glyph)
 				  (* avg-pixwidth (length glyph)))
 				 ((proof-emacs-imagep glyph)
 				  (car (image-size glyph 'inpixels)))
@@ -132,7 +132,7 @@ Borrowed from startup-center-spaces."
   "Remove splash screen and restore window config."
   (let ((splashbuf (get-buffer proof-splash-welcome)))
     (proof-splash-unset-frame-titles)
-    (if (and 
+    (if (and
 	 splashbuf
 	 proof-splash-timeout-conf)
 	(progn
@@ -165,7 +165,7 @@ Borrowed from startup-center-spaces."
 	   (let ((spec (car splash-contents)))
 	     (if (functionp spec)
 		 (setq spec (funcall spec)))
-	     (indent-to (proof-splash-centre-spaces 
+	     (indent-to (proof-splash-centre-spaces
 			 (concat (car spec) (cadr spec))))
 	     (insert (car spec))
 	     (insert-button (cadr spec)
@@ -234,7 +234,7 @@ If TIMEOUT is non-nil, arrange for a time-out to occur outside this function."
 			   (concat proof-assistant " "))
 		       "Proof General")))
     (setq proof-splash-old-frame-title-format frame-title-format)
-    (setq frame-title-format 
+    (setq frame-title-format
 	  (concat instance-name ":   %b"))))
 
 (defun proof-splash-unset-frame-titles ()
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index bd36a7d3..7333a935 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -1,7 +1,7 @@
 ;; proof-syntax.el	Functions for dealing with syntax
 ;;
-;; Copyright (C) 1997-2001 LFCS Edinburgh. 
-;; Authors:   David Aspinall, Healfdene Goguen, 
+;; Copyright (C) 1997-2001 LFCS Edinburgh.
+;; Authors:   David Aspinall, Healfdene Goguen,
 ;;	      Thomas Kleymann, Dilip Sequiera
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -111,7 +111,7 @@ nil if a region cannot be found."
   "Default function for `proof-looking-at-syntactic-context'."
   (or
    (proof-buffer-syntactic-context)
-   (save-match-data 
+   (save-match-data
      (when (proof-looking-at-safe proof-script-comment-start-regexp) 'comment))
    (save-match-data
      (when (proof-looking-at-safe proof-string-start-regexp) 'string))))
@@ -278,7 +278,7 @@ Any other %-prefixed character inserts itself."
   "Splice SEP into list of STRINGS, ignoring nil entries."
   (let (stringsep)
     (while strings
-      (when (car strings) ; suppress nils 
+      (when (car strings) ; suppress nils
 	(setq stringsep (concat stringsep (car strings)))
 	(if (and (cdr strings) (cadr strings))
 	    (setq stringsep
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 1acc62e5..3881493b 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -7,7 +7,7 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; 2. It's a little bit tricky to add prover-specific items:
 ;; presently it must be done before this file is loaded.
 ;; We could improve on that by generating everything on-thy-fly
@@ -30,7 +30,7 @@
 
 ;;
 ;; Function, icon, button names
-;; 
+;;
 
 (defun proof-toolbar-function (token)
   (intern (concat "proof-toolbar-" (symbol-name token))))
@@ -43,7 +43,7 @@
 
 ;;
 ;; Now the toolbar icons and buttons
-;; 
+;;
 
 (defun proof-toolbar-make-icon (tle)
   "Make icon variable and icon list entry from a PA-toolbar-entries entry."
@@ -69,7 +69,7 @@
 		       (list :help tooltip)
 		       (if (fboundp enabler)
 			   (list :enable (list enabler)))
-		       (if visiblep 
+		       (if visiblep
 			   (list :visible visiblep)))))
       (if includep
 	  (apply 'tool-bar-local-item
@@ -222,18 +222,18 @@ to the default toolbar."
 (defalias 'proof-toolbar-command-enable-p 'proof-shell-available-p)
 
 ;; Help  (I was an alias for this)
- 
+
 (defun proof-toolbar-help ()
   (interactive)
   (info "ProofGeneral"))
 
 ;; Find
- 
+
 (defalias 'proof-toolbar-find 'proof-find-theorems)
 (defalias 'proof-toolbar-find-enable-p 'proof-shell-available-p)
 
 ;; Info
- 
+
 (defalias 'proof-toolbar-info 'proof-query-identifier)
 (defalias 'proof-toolbar-info-enable-p 'proof-shell-available-p)
 
diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el
index 414d580c..af327784 100644
--- a/generic/proof-unicode-tokens.el
+++ b/generic/proof-unicode-tokens.el
@@ -8,7 +8,7 @@
 ;;
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Support for Unicode Tokens package: per-prover global enabling, copying
 ;; configuration tables, adding mode hooks to turn on/off.
 ;;
@@ -52,7 +52,7 @@
 	     (proof-ass-symv var))))
   (unicode-tokens-initialise))
 
-  
+
 ;;;###autoload
 (defun proof-unicode-tokens-enable ()
   "Turn on or off Unicode tokens mode in Proof General script buffer.
@@ -87,7 +87,7 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit."
     (proof-buffers-in-mode proof-tokens-extra-modes))
    (unicode-tokens-mode (if flag 1 0)))
   (proof-unicode-tokens-configure-prover))
-  
+
 ;;;
 ;;; Interface to custom to dynamically change tables (via proof-set-value)
 ;;;
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index da97e454..3a5cdaef 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -87,7 +87,7 @@ terminator somewhere nearby.  Electric!"
   "*Whether to display keyboard hints in the minibuffer."
   :type 'boolean
   :group 'proof-user-options)
-  
+
 ;; FIXME: next one could be integer value for catchup delay
 (defcustom proof-trace-output-slow-catchup t
   "*If non-nil, try to redisplay less often during frequent trace output.
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 41988176..90dcf852 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -7,9 +7,9 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Loading note: this file is required immediately from proof.el, so
-;; no autoloads cookies are added here. 
+;; no autoloads cookies are added here.
 ;;
 ;; Compilation note: see etc/development-tips.txt
 ;;
@@ -24,12 +24,12 @@
 ;; This file is loaded early, and may be first compiled file
 ;; loaded if proof-site.el is loaded instead of proof-site.elc.
 ;;
-(eval-and-compile 
+(eval-and-compile
   (defun pg-emacs-version-cookie ()
     (format "GNU Emacs %d.%d"
 	    emacs-major-version emacs-minor-version))
-  
-  (defconst pg-compiled-for 
+
+  (defconst pg-compiled-for
     (eval-when-compile (pg-emacs-version-cookie))
     "Version of Emacs we're compiled for (or running on, if interpreted)."))
 
@@ -39,17 +39,17 @@
     (error "Proof General is not compatible with Emacs %s" emacs-version))
 
 (unless (equal pg-compiled-for (pg-emacs-version-cookie))
-  (error 
+  (error
    "Proof General was compiled for %s but running on %s: please run \"make clean; make\""
    pg-compiled-for (pg-emacs-version-cookie)))
 
 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;  
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 
-(require 'proof-compat)		        ; 
+(require 'proof-compat)		        ;
 (require 'proof-config)			; config vars
-(require 'bufhist)			; bufhist 
+(require 'bufhist)			; bufhist
 (require 'proof-syntax)			; syntax utils
 (require 'proof-autoloads)		; interface fns
 
@@ -88,7 +88,7 @@ Return nil if not a script buffer or if no active scripting buffer."
     ((buffer-live-p proof-script-buffer)
      (with-current-buffer proof-script-buffer
        ,@body))))
-      
+
 (defmacro proof-map-buffers (buflist &rest body)
   "Do BODY on each buffer in BUFLIST, if it exists."
   `(dolist (buf ,buflist)
@@ -193,7 +193,7 @@ Helper for macro `defpgcustom'."
     ;; is nothing similar for values, so we define a new set/get function.
     (eval
      `(defun ,generic-var (&optional newval)
-	,(concat "Set or get value of " (symbol-name sym) 
+	,(concat "Set or get value of " (symbol-name sym)
 		 " for current proof assistant.
 If NEWVAL is present, set the variable, otherwise return its current value.")
 	(if newval
@@ -250,14 +250,14 @@ Usage: (defpgdefault SYM VALUE)"
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Evaluation once proof assistant is known
-;; 
+;;
 
 (defmacro proof-eval-when-ready-for-assistant (&rest body)
   "Evaluate BODY once the proof assistant is determined (possibly now)."
   `(if (and (boundp 'proof-assistant-symbol) proof-assistant-symbol)
        (progn ,@body)
      (add-hook 'proof-ready-for-assistant-hook (lambda () ,@body))))
-    
+
 
 
 
@@ -317,7 +317,7 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
   (mapcar
    (lambda (kbl)
      (let ((k (car kbl)) (f (cdr kbl)))
-         (define-key map k f)))
+	 (define-key map k f)))
    kbl))
 
 
@@ -334,7 +334,7 @@ Leave point at END."
 (defun pg-remove-specials-in-string (string)
   (proof-replace-regexp-in-string pg-special-char-regexp "" string))
 
-  
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -428,17 +428,17 @@ Ensure that point is visible in window."
 	      ;; Ensure point visible.  Again, window may have died
 	      ;; inside shrink to fit, for some reason
 	      (when (window-live-p window)
-                (unless (pos-visible-in-window-p (point) window)
-                  (recenter -1))
-                (with-current-buffer buffer
-                  (if (window-bottom-p window)
-                      (unless (local-variable-p 'mode-line-format)
-                        ;; Don't show any mode line.
-                        (set (make-local-variable 'mode-line-format) nil))
-                    (unless mode-line-format
-                      ;; If the buffer gets displayed elsewhere, re-add
-                      ;; the modeline.
-                      (kill-local-variable 'mode-line-format))))))))))))
+		(unless (pos-visible-in-window-p (point) window)
+		  (recenter -1))
+		(with-current-buffer buffer
+		  (if (window-bottom-p window)
+		      (unless (local-variable-p 'mode-line-format)
+			;; Don't show any mode line.
+			(set (make-local-variable 'mode-line-format) nil))
+		    (unless mode-line-format
+		      ;; If the buffer gets displayed elsewhere, re-add
+		      ;; the modeline.
+		      (kill-local-variable 'mode-line-format))))))))))))
 
 (defun proof-clean-buffer (buffer)
   "Erase buffer and hide from display if proof-delete-empty-windows set.
@@ -493,7 +493,7 @@ No action if BUF is nil or killed."
 	     (display-buffer buf 'not-this-window)
 	   (let ((pop-up-windows t))
 	     (pop-to-buffer buf 'not-this-window 'norecord))))))
-  
+
 
 ;; Originally based on `shrink-window-if-larger-than-buffer', which
 ;; has a pretty weird implementation.
@@ -543,27 +543,27 @@ or if the window is the only window of its frame."
 	  ;;; ((cur-height (window-height window))
 	   ;; Most window is allowed to grow to
 	  ((max-height
-             (/ (frame-height (window-frame window))
-                (if proof-three-window-enable
-                    ;; we're in three-window-mode with
-                    ;; all horizontal splits, so share the height.
-                    3
-                  ;; Otherwise assume a half-and-half split.
-                  2)))
-           ;; I find that I'm willing to use a bit more than the max in
-           ;; those cases where it allows me to see the whole
-           ;; response/goal.  --Stef
-           (absolute-max-height
+	     (/ (frame-height (window-frame window))
+		(if proof-three-window-enable
+		    ;; we're in three-window-mode with
+		    ;; all horizontal splits, so share the height.
+		    3
+		  ;; Otherwise assume a half-and-half split.
+		  2)))
+	   ;; I find that I'm willing to use a bit more than the max in
+	   ;; those cases where it allows me to see the whole
+	   ;; response/goal.  --Stef
+	   (absolute-max-height
 	    (truncate
-             (/ (frame-height (window-frame window))
-                (if proof-three-window-enable
-                    ;; we're in three-window-mode with
-                    ;; all horizontal splits, so share the height.
-                    2
-                  ;; Otherwise assume a half-and-half split.
-                  1.5))))
+	     (/ (frame-height (window-frame window))
+		(if proof-three-window-enable
+		    ;; we're in three-window-mode with
+		    ;; all horizontal splits, so share the height.
+		    2
+		  ;; Otherwise assume a half-and-half split.
+		  1.5))))
 	   ;; If buffer ends with a newline and point is right after it, then
-           ;; add a final empty line (to display the cursor).
+	   ;; add a final empty line (to display the cursor).
 	   (extraline (if (and (eobp) (bolp)) 1 0))
 	   ;; (test-pos (- (point-max) extraline))
 	   ;; Direction of resizing based on whether max position is
@@ -580,10 +580,10 @@ or if the window is the only window of its frame."
 	;; Let's shrink or expand.  Uses new GNU Emacs function.
 	(let ((window-size-fixed nil))
 	  (set-window-text-height window
-                                  ;; As explained earlier: use abs-max-height
-                                  ;; but only if that makes it display all.
-                                  (if (> desired-height absolute-max-height)
-                                      max-height desired-height)))
+				  ;; As explained earlier: use abs-max-height
+				  ;; but only if that makes it display all.
+				  (if (> desired-height absolute-max-height)
+				      max-height desired-height)))
 	(if (window-live-p window)
 	    (progn
 	      (if (>= (window-text-height window) desired-height)
@@ -755,7 +755,7 @@ KEY is added onto proof-assistant map."
   "Save custom vars VARIABLES."
   (dolist (symbol variables)
     (let ((value (get symbol 'customized-value)))
-      ;; See customize-save-customized; adjust properties so 
+      ;; See customize-save-customized; adjust properties so
       ;; that custom-save-all will save the value.
       (when value
 	(put symbol 'saved-value value)
@@ -846,7 +846,7 @@ If optional arg REALLY-WORD is non-nil, it finds just a word."
   "Determine if current point is at beginning or within comment/string context.
 If so, return a symbol indicating this ('comment or 'string).
 This function invokes <PA-syntactic-context> if that is defined, otherwise
-it calls `proof-looking-at-syntactic-context'." 
+it calls `proof-looking-at-syntactic-context'."
   (if (fboundp (proof-ass-sym syntactic-context))
       (funcall (proof-ass-sym syntactic-context))
     (proof-looking-at-syntactic-context-default)))
@@ -862,20 +862,20 @@ it calls `proof-looking-at-syntactic-context'."
 ;;
 ;; (defun proof-buffer-substring-visible (start end)
 ;;   "Return the substring from START to END with no invisible property set."
-;;   (let ((pos start) 
-;; 	(vis (get-text-property start 'invisible))
-;; 	(result "")
-;; 	nextpos)
+;;   (let ((pos start)
+;;	(vis (get-text-property start 'invisible))
+;;	(result "")
+;;	nextpos)
 ;;     (while (and (< pos end)
-;; 		(setq nextpos (next-single-property-change pos 'invisible
-;; 							   nil end)))
+;;		(setq nextpos (next-single-property-change pos 'invisible
+;;							   nil end)))
 ;;       (unless (get-text-property pos 'invisible)
-;; 	(setq result (concat result (buffer-substring-no-properties
-;; 				     pos nextpos))))
+;;	(setq result (concat result (buffer-substring-no-properties
+;;				     pos nextpos))))
 ;;       (setq pos nextpos))
 ;;     (unless (get-text-property end 'invisible)
 ;;       (setq result (concat result (buffer-substring-no-properties
-;; 				   pos end))))))
+;;				   pos end))))))
 
 
 
diff --git a/generic/proof.el b/generic/proof.el
index 13ce9cb6..af065f89 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,4 +1,4 @@
-;;; proof.el --- Proof General loader.  
+;;; proof.el --- Proof General loader.
 ;;
 ;; Copyright (C) 1998-2008 LFCS Edinburgh.
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
@@ -8,7 +8,7 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; This file loads Proof General.  It is required by the
 ;; individual prover modes.  Loading order of PG is:
 ;;
@@ -18,17 +18,18 @@
 ;; 4. stub explicitly loads <PA>/<PA>.el and execute real mode function
 ;; 5. <PA>.el requires this file, rest of PG loaded here
 ;; 6. further modules loaded by autoloads/prover-specific requires.
-;; 
-;; 
+;;
+;;
 ;;; Code:
 
 (require 'proof-site)			; site/prover config, global vars, autoloads
 (require 'proof-compat)			; Emacs and OS compatibility
 (require 'proof-utils)			; utilities
 (require 'proof-config)			; configuration variables
-(require 'proof-auxmodes)		; further autoloads
 
 (proof-splash-message)			; welcome the user now.
 
+(require 'proof-auxmodes)		; Further autoloads
+
 (provide 'proof)
 ;;; proof.el ends here