Many rearrangements for compatibility, efficient/correct compilation, namespaces fixes.

pre-shell-start-hook: remove this, use default names for modes
proof-compat: simplify architecture flags, use standard (featurep 'xemacs).

28 files changed, 1546 insertions, 1893 deletions

diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index d49ccc9e..45dd3cbd 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -1,23 +1,26 @@
-;; pg-assoc.el  Functions for associated buffers
+;;; pg-assoc.el --- Functions for associated buffers
 ;;
-;; Copyright (C) 1994-2002 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)
 ;;
 ;; $Id$
 ;;
-
-;; A sub-module of proof-shell; assumes proof-script loaded.
-(require 'proof-script)
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Defines an empty mode inherited by modes of the associated buffers.
 ;;
 
-(eval-and-compile
-(define-derived-mode proof-universal-keys-only-mode fundamental-mode
+;;; Code:
+
+(eval-when-compile 
+  (require 'proof)				; globals
+  (require 'proof-syntax)			; proof-replace-{string,regexp}
+  (require 'span)
+  (require 'cl))				; incf
+
+(eval-and-compile ; to define proof-universal-keys-only-mode-map at compile time
+  (define-derived-mode proof-universal-keys-only-mode fundamental-mode
     proof-general-name "Universal keymaps only"
     ;; Doesn't seem to supress TAB, RET
     (suppress-keymap proof-universal-keys-only-mode-map 'all)
@@ -108,7 +111,7 @@ If pg-subterm-first-special-char is unset, return STRING unchanged."
 	  
 	 
 (defun pg-assoc-strip-subterm-markup-buf-old (start end)
-  "Remove subterm and pbp annotations from region."
+  "Remove subterm and pbp annotations from region START END."
   (let (c)
     (goto-char start)
     (while (< (point) end)
@@ -131,7 +134,167 @@ If pg-subterm-first-special-char is unset, return STRING unchanged."
 	(forward-char)))
     end))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Subterm and PBP markup (goals and possibly response buffer)
+;;; 
+
+(defun pg-assoc-make-top-span (start end)
+  "Make a top span (goal/hyp area) for mouse active output in START END."
+  (let (span typname)
+    (goto-char start)
+    ;; skip the pg-topterm-regexp itself
+    (if (looking-at pg-topterm-regexp) 
+	(forward-char (- (match-end 0) (match-beginning 0))))
+    ;; typname is expected to be a cons-cell of a type (goal/hyp)
+    ;; with a name, retrieved from the text immediately following
+    ;; the topterm-regexp annotation.
+    (let ((topterm (point))) 
+      (setq typname (funcall pg-topterm-goalhyplit-fn)) ;; should be non-nil!
+      (goto-char topterm))
+    (setq start (point))
+    (if (eq (car-safe typname) 'lit)
+	;; Use length of literal command for end point
+	(forward-char (length (cdr typname)))
+      ;; Otherwise, use start/end of line before next annotation/buffer end
+      (goto-char start)
+      (beginning-of-line)
+      (setq start (point))
+      (goto-char end) ;; next annotation/end of buffer
+      (beginning-of-line)
+      (backward-char))
+    (setq span (span-make start (point)))
+    (span-set-property span 'mouse-face 'highlight)
+    (span-set-property span 'face 'proof-active-area-face)
+    (span-set-property span 'proof-top-element typname)))
+
+(defun pg-assoc-analyse-structure (start end)
+  "Analyse the region between START and END for subterm and PBP markup.
+
+For subterms, we can make nested regions in the concrete syntax into
+active mouse-highlighting regions, each of which can be used to
+communicate a selected term back to the prover.  The output text is
+marked up with the annotation scheme:
+
+ 	 [  <annotation>      |       <subterm/concrete> ] 
+
+         ^                    ^                          ^
+	 |                    |                          |
+pg-subterm-start-char  pg-subterm-sep-char  pg-subterm-end-char
+
+The annotation is intended to indicate a node in the abstract syntax
+tree inside the prover, which can be used to pick out the internal
+representation of the term itself.  We assume that the annotation
+takes the form of a sequence of characters:
+
+   <length of shared prefix previous>  <ann1> <ann2> .. <annN>
+
+Where each element <..> is a character which is *less* than
+pg-subterm-first-special-char, but *greater* than 128.  Each 
+character code has 128 subtracted to yield a number.  The first
+character allows a simple optimisation by sharing a prefix of
+the previous (left-to-right) subterm's annotation.  (See the
+variable `pg-subterm-anns-use-stack' for an alternative 
+optimisation.)
+
+For subterm markup without communication back to the prover, the
+annotation is not needed, but the first character must still be given.
+
+For proof-by-pointing (PBP) oriented markup, `pg-topterm-regexp' and
+`pg-topterm-goalhyplit-fn' should be set.  Together these allow
+further active regions to be defined, corresponding to \"top elements\"
+in the proof-state display.  A \"top element\" is currently assumed
+to be either a hypothesis or a subgoal, and is assumed to occupy 
+a line (or at least a line).  The markup is simply
+  
+                 & <goal or hypthesis line in proof state>
+                 ^
+		 |
+   pg-topterm-regexp
+
+And the function `pg-topterm-goalhyplit-fn' is called to do the
+further analysis, to return an indication of the goal/hyp and
+record a name value.  These values are used to construct PBP
+commands which can be sent to the prover."
+  (if (or pg-subterm-start-char pg-topterm-regexp) ;; markup for topterm alone
+  (let* 
+      ((cur start)
+       (len (- end start))
+       (ann (make-string len ?x)) ; (more than) enough space for longest ann'n
+       (ap  0)
+       c stack topl span)
+
+    (while (< cur end)
+      (setq c (char-after cur))
+      (cond
+       ;; Seen goal regexp: this is the start of a top extent
+       ;; (assumption, goal, literal command)
+       ((save-excursion
+	  (goto-char cur)
+	  (looking-at pg-topterm-regexp))
+	(setq topl (cons cur topl))
+	(setq ap 0))
+
+       ;; Seen subterm start char: it's followed by a char
+       ;; indicating the length of the annotation prefix
+       ;; which can be shared with the previous subterm.
+       ((and pg-subterm-start-char ;; ignore if subterm start not set
+	     (= c pg-subterm-start-char))
+	(incf cur)
+	(if pg-subterm-anns-use-stack
+	    (setq ap (- ap (- (char-after cur) 128)))
+	  (setq ap (- (char-after cur) 128)))
+	(incf cur)
+	;; Now search for a matching end-annotation char, recording the 
+	;; annotation found.
+	(while (not (= (setq c (char-after cur)) pg-subterm-sep-char))
+	  (aset ann ap (- c 128))
+	  (incf ap)
+	  (incf cur))
+	;; Push the buffer pos and annotation
+	(setq stack (cons cur 
+			  (cons (substring ann 0 ap) stack))))
+
+       ;; Seen a subterm end char, terminating an annotated region
+       ;; in the concrete syntax.  We make a highlighting span now.
+       ((and (consp stack) (= c pg-subterm-end-char))
+	;; (consp stack) added to make the code more robust.
+	;; [ Condition violated with lego/example.l and GNU Emacs 20.3 ]
+	(setq span (span-make (car stack) cur))
+	(span-set-property span 'mouse-face 'highlight)
+	(span-set-property span 'goalsave (cadr stack));; FIXME: 'goalsave?
+	;; (span-set-property span 'balloon-help helpmsg)
+	(span-set-property span 'help-echo 'pg-goals-get-subterm-help)
+	(if pg-subterm-anns-use-stack
+	    ;; Pop annotation off stack
+	    (progn
+	      (setq ap 0)
+	      (while (< ap (length (cadr stack)))
+		(aset ann ap (aref (cadr stack) ap))
+		(incf ap))))
+	;; Finish popping annotations
+	(setq stack (cdr (cdr stack)))))
+      ;; On to next char
+      (incf cur))
+    
+    ;; List of topterm beginning positions (goals/hyps) found
+    (setq topl (reverse (cons end topl)))
+    
+    ;; Proof-by-pointing markup assumes "top" elements which define a
+    ;; context for a marked-up (sub)term: we assume these contexts to
+    ;; be either a subgoal to be solved or a hypothesis.  
+    ;; Top element spans are only made if pg-topterm-goalhyplit-fn is set.
+    ;; NB: If we want Coq pbp: (setq coq-current-goal 1) 
+    (if pg-topterm-goalhyplit-fn
+	(while (setq ap (car topl) 
+		     topl (cdr topl))
+	  (pg-assoc-make-top-span ap (car topl))))
+
+    ;; Finally: strip the specials.  This should
+    ;; leave the spans in exactly the right place.
+    (pg-assoc-strip-subterm-markup-buf start end))))
+
 
 
 (provide 'pg-assoc)
-;; pg-assoc.el ends here.
+;;; pg-assoc.el ends here
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index a48027f5..19f6eb32 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -1,4 +1,4 @@
-;; pg-autotest.el: Simple testing framework for Proof General
+;;; pg-autotest.el --- Simple testing framework for Proof General
 ;;
 ;; Copyright (C) 2005 LFCS Edinburgh, David Aspinall.
 ;; Authors:   David Aspinall
@@ -8,7 +8,7 @@
 ;; TODO:
 ;; -- fix failure handling for scriptfile
 ;; -- force re
-;; -- add macros for defining test suites 
+;; -- add macros for defining test suites
 ;; -- add more precise functional tests to check results
 ;; -- add negative tests
 ;; -- output test results to stdout
@@ -18,6 +18,11 @@
 (require 'proof-site)
 (require 'proof-compat)
 
+
+;;; Commentary:
+;; 
+
+;;; Code:
 (defvar pg-autotest-success t)		;; success unless error caught
 
 ;;; Some utilities
@@ -27,7 +32,7 @@
   (let* ((name   (concat proof-home-directory file)))
     (if (file-exists-p name)
 	(find-file name)
-      (error "autotest: requested file %s does not exist" name))))
+      (error (format "autotest: requested file %s does not exist" name)))))
 
 (defun pg-autotest-find-file-restart (file)
   "Find FILE and make ready to script there."
@@ -49,7 +54,7 @@
      (error
       (progn
 	(setq pg-autotest-success nil)
-	(princ (format "Error in test %s: %s" (symbol-name (quote ,fn)) 
+	(princ (format "Error in test %s: %s" (symbol-name (quote ,fn))
 		       err)))))) ;; display-error stdout?
 
 
@@ -84,14 +89,14 @@ An error is signalled if scripting doesn't complete."
   (save-excursion
     (pg-autotest-find-file file)
     (unless (proof-locked-region-full-p)
-      (error "Locked region in file `%s' is not full." file))))
+      (error (format "Locked region in file `%f' is not full" file)))))
 
 (defun pg-autotest-assert-unprocessed (file)
   "Check that FILE has been fully unprocessed."
   (save-excursion
     (pg-autotest-find-file file)
     (unless (proof-locked-region-empty-p)
-      (error "Locked region in file `%f' is not empty."))))
+      (error (format "Locked region in file `%f' is not empty" file)))))
 
 (defun pg-autotest-message (msg)
   "Give message MSG on std out & on display."
@@ -104,7 +109,7 @@ An error is signalled if scripting doesn't complete."
   "Exit prover process."
   (if (buffer-live-p proof-shell-buffer)
 	(kill-buffer proof-shell-buffer)
-    (error "No proof shell buffer to kill!")))
+    (error "No proof shell buffer to kill")))
 
 (defun pg-autotest-finished ()
   "Exit Emacs returning Unix success 0 if all tests succeeded."
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index e726ecdd..f1558217 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -1,6 +1,6 @@
-;; pg-goals.el  Proof General goals buffer mode.
+;; pg-goals.el ---  Proof General goals buffer mode.
 ;;
-;; Copyright (C) 1994-2002 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)
@@ -8,33 +8,36 @@
 ;; $Id$
 ;;
 
-;; A sub-module of proof-shell; assumes proof-script loaded.
-(require 'pg-assoc)
+;;; Code:
+(eval-when-compile
+  (require 'easymenu)			; easy-menu-add, etc
+  (require 'cl)				; incf
+  (require 'span)			; span-*
+  (require 'proof-utils))
+
+
+;;; Commentary:
+;; 
 
+(require 'proof-site)
 (require 'bufhist)
+;(require 'pg-assoc)
 
-;; Nuke some byte compiler warnings.
-(eval-when-compile
-  (require 'easymenu))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Goals buffer mode
 ;;
 
-;;
-;; The mode itself
-;;
-(eval-and-compile			; to define proof-goals-mode-map
+;;;###autload
 (define-derived-mode proof-goals-mode proof-universal-keys-only-mode
-  proof-general-name 
-  "Mode for goals display.  
+  proof-general-name
+  "Mode for goals display.
 May enable proof-by-pointing or similar features.
 \\{proof-goals-mode-map}"
   (setq proof-buffer-type 'goals)
   ;; font-lock-keywords isn't automatically buffer-local in Emacs 21.2
   (make-local-variable 'font-lock-keywords)
-  (make-local-hook 'kill-buffer-hook)
   (add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
   (easy-menu-add proof-goals-mode-menu proof-goals-mode-map)
   (easy-menu-add proof-assistant-menu proof-goals-mode-map)
@@ -42,47 +45,51 @@ May enable proof-by-pointing or similar features.
   (erase-buffer)
   (buffer-disable-undo)
   (if proof-keep-response-history (bufhist-mode)) ; history for contents
-  (set-buffer-modified-p nil)))
+  (set-buffer-modified-p nil))
 
 ;;
-;; Keys for goals buffer
+;; Menu for goals buffer
 ;;
-(define-key proof-goals-mode-map [q] 'bury-buffer)
-(cond 
-(proof-running-on-XEmacs
-(define-key proof-goals-mode-map [(button2)] 'pg-goals-button-action)
-(define-key proof-goals-mode-map [(control button2)] 'proof-undo-and-delete-last-successful-command)
-;; button 2 is a nuisance on 2 button mice, so we'll do 1 as well.
-;; Actually we better hadn't, people like to use it for cut and paste.
-;; (define-key proof-goals-mode-map [(button1)] 'pg-goals-button-action)
-;; (define-key proof-goals-mode-map [(control button1)] 'proof-undo-and-delete-last-successful-command)
-;; C Raffalli: The next key on button3 will be remapped to proof by contextual 
-;; menu by pg-pbrpm.el. In this case, control button3 is mapped to 
-;; 'pg-goals-yank-subterm
-(define-key proof-goals-mode-map [(button3)] 'pg-goals-yank-subterm))
-(t
-(define-key proof-goals-mode-map [mouse-2] 'pg-goals-button-action)
-(define-key proof-goals-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command)
-;; (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
-;; (define-key proof-goals-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command)
-;; C Raffalli: The next key on button3 will be remapped to proof by contextual 
-;; menu by pg-pbrpm.el. In this cans, control button3 is mapped to 
-;; 'pg-goals-yank-subterm
-(define-key proof-goals-mode-map [mouse-3] 'pg-goals-yank-subterm)))
+(proof-eval-when-ready-for-assistant ; proof-aux-menu depends on <PA>
+    (easy-menu-define proof-goals-mode-menu
+      proof-goals-mode-map
+      "Menu for Proof General goals buffer."
+      (proof-aux-menu)))
 
 
 ;;
-;; Menu for goals buffer
+;; Keys for goals buffer
 ;;
-(easy-menu-define proof-goals-mode-menu
-		  proof-goals-mode-map
-		  "Menu for Proof General goals buffer."
-		  proof-aux-menu)
+(define-key proof-goals-mode-map [q] 'bury-buffer)
+
+(cond
+ ((featurep 'xemacs)
+  (define-key proof-goals-mode-map [(button2)] 'pg-goals-button-action)
+  (define-key proof-goals-mode-map [(control button2)] 'proof-undo-and-delete-last-successful-command)
+  ;; button 2 is a nuisance on 2 button mice, so we'll do 1 as well.
+  ;; Actually we better hadn't, people like to use it for cut and paste.
+  ;; (define-key proof-goals-mode-map [(button1)] 'pg-goals-button-action)
+  ;; (define-key proof-goals-mode-map [(control button1)] 'proof-undo-and-delete-last-successful-command)
+  ;; C Raffalli: The next key on button3 will be remapped to proof by contextual
+  ;; menu by pg-pbrpm.el.  In this case, control button3 is mapped to
+  ;; 'pg-goals-yank-subterm
+  (define-key proof-goals-mode-map [(button3)] 'pg-goals-yank-subterm))
+ (t
+  (define-key proof-goals-mode-map [mouse-2] 'pg-goals-button-action)
+  (define-key proof-goals-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command)
+  ;; (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
+  ;; (define-key proof-goals-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command)
+  ;; C Raffalli: The next key on button3 will be remapped to proof by contextual
+  ;; menu by pg-pbrpm.el.  In this case, control button3 is mapped to
+  ;; 'pg-goals-yank-subterm
+  (define-key proof-goals-mode-map [mouse-3] 'pg-goals-yank-subterm)))
+
 
 
 ;;
 ;; The completion of init
 ;;
+;;;###autoload
 (defun proof-goals-config-done ()
   "Initialise the goals buffer after the child has been configured."
   (proof-font-lock-configure-defaults nil)
@@ -110,7 +117,7 @@ and properly fontifies STRING using proof-fontify-region."
     
     ;; Erase the response buffer if need be, maybe removing the
     ;; window.  Indicate it should be erased before the next output.
-    (proof-shell-maybe-erase-response t t)
+    (pg-response-maybe-erase t t)
 
     ;; Erase the goals buffer and add in the new string
     (set-buffer proof-goals-buffer)
@@ -131,7 +138,7 @@ and properly fontifies STRING using proof-fontify-region."
       ;; for special characters 128-255, which is inconsistent with
       ;; UTF-8 interaction.
       (unless proof-shell-unicode
-	(pg-goals-analyse-structure (point-min) (point-max)))
+	(pg-assoc-analyse-structure (point-min) (point-max)))
 
       (unless pg-use-specials-for-fontify
 	;; provers which use ordinary keywords to fontify output must
@@ -139,173 +146,16 @@ and properly fontifies STRING using proof-fontify-region."
 	(proof-fontify-region (point-min) (point-max)))
       
       ;; Record a cleaned up version of output string
-      (setq proof-shell-last-output 
+      (setq proof-shell-last-output
 	    (buffer-substring (point-min) (point-max)))
       
       (set-buffer-modified-p nil)	; nicety
       
-      ;; Keep point at the start of the buffer.  
-      (proof-display-and-keep-buffer 
+      ;; Keep point at the start of the buffer.
+      (proof-display-and-keep-buffer
        proof-goals-buffer (point-min)))))
 
 
-(defun pg-goals-analyse-structure (start end)
-  "Analyse the region between START and END for subterm and PBP markup.
-
-For subterms, we can make nested regions in the concrete syntax into
-active mouse-highlighting regions, each of which can be used to
-communicate a selected term back to the prover.  The output text is
-marked up with the annotation scheme:
-
- 	 [  <annotation>      |       <subterm/concrete> ] 
-
-         ^                    ^                          ^
-	 |                    |                          |
-pg-subterm-start-char  pg-subterm-sep-char  pg-subterm-end-char
-
-The annotation is intended to indicate a node in the abstract syntax
-tree inside the prover, which can be used to pick out the internal
-representation of the term itself.  We assume that the annotation
-takes the form of a sequence of characters:
-
-   <length of shared prefix previous>  <ann1> <ann2> .. <annN>
-
-Where each element <..> is a character which is *less* than
-pg-subterm-first-special-char, but *greater* than 128.  Each 
-character code has 128 subtracted to yield a number.  The first
-character allows a simple optimisation by sharing a prefix of
-the previous (left-to-right) subterm's annotation.  (See the
-variable `pg-subterm-anns-use-stack' for an alternative 
-optimisation.)
-
-For subterm markup without communication back to the prover, the
-annotation is not needed, but the first character must still be given.
-
-For proof-by-pointing (PBP) oriented markup, `pg-topterm-regexp' and
-`pg-topterm-goalhyplit-fn' should be set.  Together these allow
-further active regions to be defined, corresponding to \"top elements\"
-in the proof-state display.  A \"top element\" is currently assumed
-to be either a hypothesis or a subgoal, and is assumed to occupy 
-a line (or at least a line).  The markup is simply
-  
-                 & <goal or hypthesis line in proof state>
-                 ^
-		 |
-   pg-topterm-regexp
-
-And the function `pg-topterm-goalhyplit-fn' is called to do the
-further analysis, to return an indication of the goal/hyp and
-record a name value.  These values are used to construct PBP
-commands which can be sent to the prover."
-  (if (or pg-subterm-start-char pg-topterm-regexp) ;; markup for topterm alone
-  (let* 
-      ((cur start)
-       (len (- end start))
-       (ann (make-string len ?x)) ; (more than) enough space for longest ann'n
-       (ap  0)
-       c stack topl span)
-
-    (while (< cur end)
-      (setq c (char-after cur))
-      (cond
-       ;; Seen goal regexp: this is the start of a top extent
-       ;; (assumption, goal, literal command)
-       ((save-excursion
-	  (goto-char cur)
-	  (looking-at pg-topterm-regexp))
-	(setq topl (cons cur topl))
-	(setq ap 0))
-
-       ;; Seen subterm start char: it's followed by a char
-       ;; indicating the length of the annotation prefix
-       ;; which can be shared with the previous subterm.
-       ((and pg-subterm-start-char ;; ignore if subterm start not set
-	     (= c pg-subterm-start-char))
-	(incf cur)
-	(if pg-subterm-anns-use-stack
-	    (setq ap (- ap (- (char-after cur) 128)))
-	  (setq ap (- (char-after cur) 128)))
-	(incf cur)
-	;; Now search for a matching end-annotation char, recording the 
-	;; annotation found.
-	(while (not (= (setq c (char-after cur)) pg-subterm-sep-char))
-	  (aset ann ap (- c 128))
-	  (incf ap)
-	  (incf cur))
-	;; Push the buffer pos and annotation
-	(setq stack (cons cur 
-			  (cons (substring ann 0 ap) stack))))
-
-       ;; Seen a subterm end char, terminating an annotated region
-       ;; in the concrete syntax.  We make a highlighting span now.
-       ((and (consp stack) (= c pg-subterm-end-char))
-	;; (consp stack) added to make the code more robust.
-	;; [ Condition violated with lego/example.l and GNU Emacs 20.3 ]
-	(setq span (make-span (car stack) cur))
-	(set-span-property span 'mouse-face 'highlight)
-	(set-span-property span 'goalsave (cadr stack));; FIXME: 'goalsave?
-	;; (set-span-property span 'balloon-help helpmsg)
-	(set-span-property span 'help-echo 'pg-goals-get-subterm-help)
-	(if pg-subterm-anns-use-stack
-	    ;; Pop annotation off stack
-	    (progn
-	      (setq ap 0)
-	      (while (< ap (length (cadr stack)))
-		(aset ann ap (aref (cadr stack) ap))
-		(incf ap))))
-	;; Finish popping annotations
-	(setq stack (cdr (cdr stack)))))
-      ;; On to next char
-      (incf cur))
-    
-    ;; List of topterm beginning positions (goals/hyps) found
-    (setq topl (reverse (cons end topl)))
-    
-    ;; Proof-by-pointing markup assumes "top" elements which define a
-    ;; context for a marked-up (sub)term: we assume these contexts to
-    ;; be either a subgoal to be solved or a hypothesis.  
-    ;; Top element spans are only made if pg-topterm-goalhyplit-fn is set.
-    ;; NB: If we want Coq pbp: (setq coq-current-goal 1) 
-    (if pg-topterm-goalhyplit-fn
-	(while (setq ap (car topl) 
-		     topl (cdr topl))
-	  (pg-goals-make-top-span ap (car topl))))
-
-    ;; Finally: strip the specials.  This should
-    ;; leave the spans in exactly the right place.
-    (pg-assoc-strip-subterm-markup-buf start end))))
-
-
-(defun pg-goals-make-top-span (start end)
-  "Make a top span (goal/hyp area) for mouse active output."
-  (let (span typname)
-    (goto-char start)
-    ;; skip the pg-topterm-regexp itself
-    (if (looking-at pg-topterm-regexp) 
-	(forward-char (- (match-end 0) (match-beginning 0))))
-    ;; typname is expected to be a cons-cell of a type (goal/hyp)
-    ;; with a name, retrieved from the text immediately following
-    ;; the topterm-regexp annotation.
-    (let ((topterm (point))) 
-      (setq typname (funcall pg-topterm-goalhyplit-fn)) ;; should be non-nil!
-      (goto-char topterm))
-    (setq start (point))
-    (if (eq (car-safe typname) 'lit)
-	;; Use length of literal command for end point
-	(forward-char (length (cdr typname)))
-      ;; Otherwise, use start/end of line before next annotation/buffer end
-      (goto-char start)
-      (beginning-of-line)
-      (setq start (point))
-      (goto-char end) ;; next annotation/end of buffer
-      (beginning-of-line)
-      (backward-char))
-    (setq span (make-span start (point)))
-    (set-span-property span 'mouse-face 'highlight)
-    (set-span-property span 'face 'proof-active-area-face)
-    (set-span-property span 'proof-top-element typname)))
-
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Commands to prover based on subterm markup (inc PBP).
@@ -322,7 +172,7 @@ This function should be bound to a mouse button in the Proof General
 goals buffer.
 
 The EVENT is used to find the smallest subterm around a point.  The
-subterm is copied to the kill-ring, and immediately yanked (copied)
+subterm is copied to the `kill-ring', and immediately yanked (copied)
 into the current buffer at the current cursor position.
 
 In case the current buffer is the goals buffer itself, the yank
@@ -334,11 +184,11 @@ explicit yank."
       (save-excursion
 	(mouse-set-point event)
 	;; Get either the proof body or whole goalsave
-	(setq span (or 
+	(setq span (or
 		    (span-at (point) 'proof)
 		    (span-at (point) 'goalsave)))
 	(if span (copy-region-as-kill
-		  (span-start span) 
+		  (span-start span)
 		  (span-end span)))))
     (if (and span (not (eq proof-buffer-type 'goals)))
 	(yank))))
@@ -354,7 +204,7 @@ it to construct an appropriate proof command.  The command which is
 constructed will be inserted at the end of the locked region in the
 proof script buffer, and immediately sent back to the proof assistant.
 If it succeeds, the locked region will be extended to cover the
-proof-by-pointing command, just as for any proof command the 
+proof-by-pointing command, just as for any proof command the
 user types by hand."
    (interactive "e")
    (mouse-set-point event)
@@ -366,15 +216,15 @@ user types by hand."
 
 (defun proof-expand-path (string)
   (let ((a 0) (l (length string)) ls)
-    (while (< a l) 
-      (setq ls (cons (int-to-string 
+    (while (< a l)
+      (setq ls (cons (int-to-string
 		      (char-to-int (aref string a)))
 		     (cons " " ls)))
       (incf a))
     (apply 'concat (nreverse ls))))
 
 (defun pg-goals-construct-command ()
-  ;; Examine the goals 
+  "Examine the goals "
   (let* ((span (span-at (point) 'goalsave)) ;; goalsave means subgoal no/name
 	 (top-span (span-at (point) 'proof-top-element))
 	 top-info)
@@ -383,10 +233,10 @@ user types by hand."
       (pop-to-buffer proof-script-buffer)
       (cond
        (span
-	(proof-shell-invisible-command 
-	 (format (if (eq 'hyp (car top-info)) pbp-hyp-command 
+	(proof-shell-invisible-command
+	 (format (if (eq 'hyp (car top-info)) pbp-hyp-command
 		                              pbp-goal-command)
-		 (concat (cdr top-info) (proof-expand-path 
+		 (concat (cdr top-info) (proof-expand-path
 					 (span-property span 'goalsave))))))
        ((eq (car top-info) 'hyp)
 	;; Switch focus to another subgoal; a non-scripting command
@@ -409,21 +259,22 @@ user types by hand."
 	(or (span-property span 'cachedhelp) ;; already got
 	    (progn
 	      (if (proof-shell-available-p)
-		  (let ((result 
-			 (proof-shell-invisible-cmd-get-result 
+		  (let ((result
+			 (proof-shell-invisible-cmd-get-result
 			  (format pg-subterm-help-cmd (span-string span))
 			  'ignorerrors)))
 		    ;; FIXME: generalise, and make output readable
 		    ;; (fontify?  does that work for GNU Emacs?
 		    ;;  how can we do it away from a buffer?)
 		    (setq result
-			  (replace-in-string 
-			   result 
-			   (concat "\n\\|" pg-special-char-regexp) ""))		    
-		    (set-span-property span 'cachedhelp result)
+			  (replace-in-string
+			   result
+			   (concat "\n\\|" pg-special-char-regexp) ""))
+		    (span-set-property span 'cachedhelp result)
 		    result)))))))
 
 
 
 (provide 'pg-goals)
-;; pg-goals.el ends here.
+
+;;; pg-goals.el ends here
diff --git a/generic/pg-metadata.el b/generic/pg-metadata.el
index c6fd5504..86800e2a 100644
--- a/generic/pg-metadata.el
+++ b/generic/pg-metadata.el
@@ -1,14 +1,17 @@
-;; pg-metadata.el   Persistant storage of metadata for proof scripts
+;; pg-metadata.el ---  Persistant storage of metadata for proof scripts
 ;;
-;; Copyright (C) 2001-2 LFCS Edinburgh. 
+;; Copyright (C) 2001-2 LFCS Edinburgh.
 ;; Author:      David Aspinall <David.Aspinall@ed.ac.uk>
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
+
+;;; Commentary:
+;; 
 ;; Status: incomplete; experimental
 ;;
-;; TODO: 
+;; TODO:
 ;;  - add file dependency information to proof scripts individually
 ;;    (can approximate from the transitive closure that is included files list)
 ;;
@@ -16,16 +19,16 @@
 ;; must be added to main dist by editing Makefile.devel
 ;;
 
-(require 'pg-xml)
+;;; Code:
 
-;; Variables
+(require 'pg-xml)
 
 (defcustom pg-metadata-default-directory "~/.proofgeneral/"
   "*Directory for storing metadata information about proof scripts."
   :type 'file
   :group 'proof-user-options)
 
-(defface proof-preparsed-span 
+(defface proof-preparsed-span
   (proof-face-specs
    (:background "lightgoldenrodyellow")
    (:background "darkgoldenrod")
@@ -42,7 +45,7 @@
   ;; Clashes are possible, hopefully unlikely.
   (concat
    (file-name-as-directory pg-metadata-default-directory)
-   (replace-in-string 
+   (replace-in-string
     (file-name-sans-extension filename)
     (regexp-quote (char-to-string directory-sep-char))
     "__")
@@ -63,7 +66,7 @@
 ;	     (span	   (span-at (point-min) 'type))
 ;	     type)
 ;	(pg-xml-begin-write)
-;	(pg-xml-openelt 'script-file 
+;	(pg-xml-openelt 'script-file
 ;			(list (list 'filename scriptfile)
 ;			      (list 'filedate modtime)))
 ;	(pg-xml-closeelt)
@@ -72,7 +75,7 @@
 ;		(name  (span-property span 'name))
 ;		(start (span-start span))
 ;		(end   (span-end span)))
-;	  (pg-xml-openelt 
+;	  (pg-xml-openelt
 ;	   'span
 ;	   (list (list 'type type)
 ;		 (list 'name name)
@@ -106,11 +109,4 @@
 
 
 (provide 'pg-metadata)
-;; pg-metadata.el ends here.
-  
-	
-	  
-
-	  
-		     
-  
+;;; pg-metadata.el ends here
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index 21f0c02f..563f59e5 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -1,4 +1,4 @@
-;; pg-pbrpm.el  Proof General - Proof By Rules Pop-up Menu - mode.
+;; pg-pbrpm.el --- Proof General - Proof By Rules Pop-up Menu - mode.
 ;;
 ;; Copyright (C) 2004 - Universite de Savoie, France.
 ;; Authors:   Jean-Roch SOTTY, Christophe Raffalli
@@ -6,12 +6,9 @@
 ;;
 ;; analysis of the goal buffer
 
-(require 'proof-utils)			;; for proof-face-specs
-
-
-
+;;; Code:
 (defvar pg-pbrpm-use-buffer-menu t
-  "if t, pbrpm will use a menu displayed in a dialog fram instead of a popup menu")
+  "If t, pbrpm will use a menu displayed in a dialog frame instead of a popup menu.")
 (defvar pg-pbrpm-buffer-menu nil)
 (defvar pg-pbrpm-spans nil)
 (defvar pg-pbrpm-goal-description nil)
@@ -20,13 +17,13 @@
 (defun pg-pbrpm-erase-buffer-menu ()
   (save-excursion
     (set-buffer pg-pbrpm-buffer-menu)
-    (mapc 'delete-span pg-pbrpm-spans)
+    (mapc 'span-delete pg-pbrpm-spans)
     (setq pg-pbrpm-spans nil)
     (erase-buffer)))
 
 (defun pg-pbrpm-menu-change-hook (start end len)
   (save-excursion
-    (let ((span (span-at (- start 1) 'editable)))	
+    (let ((span (span-at (- start 1) 'editable)))
       (if (not span) (setq span (span-at start 'editable)))
       (if span
 	  (let ((len (- (span-end span) (span-start span))))
@@ -43,22 +40,23 @@
 
  
 (defun pg-pbrpm-create-reset-buffer-menu ()
-  "Create if necessary and erase all text in the 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)))
       (progn
 	(setq pg-pbrpm-buffer-menu
 	      (generate-new-buffer (generate-new-buffer-name "*proof-menu*")))
 	(set-buffer pg-pbrpm-buffer-menu)
 ; needs to be fixed here, the mode could be some other prover
-	(phox-mode)
-	(make-local-hook 'after-change-functions)
-	(setq after-change-functions (cons 'pg-pbrpm-menu-change-hook after-change-functions)))
-    (pg-pbrpm-erase-buffer-menu))
+;	(phox-mode)
+; da: proof-mode-for-script should do it
+	(funcall 'proof-mode-for-script)
+	(add-hook 'after-change-functions 'pg-pbrpm-menu-change-hook nil t)
+    (pg-pbrpm-erase-buffer-menu)))
   (set-buffer pg-pbrpm-buffer-menu))
 
 (defun pg-pbrpm-analyse-goal-buffer ()
   "This function analyses the goal buffer and produces a table to find goals and hypothesis.
-   If stores, in the variable pg-pbrpm-goal-description, a list with shape
+If stores, in the variable pg-pbrpm-goal-description, a list with shape
 
    (start-goal end-goal goal-name start-concl hyps ...) with 5 elements for each goal:
 
@@ -72,14 +70,13 @@
      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)
      end-hyp: the position of the last char of the hypothesis
-     hyp-name: then name of the hypothesis.
-"
+     hyp-name: then name of the hypothesis."
   (save-excursion
     (set-buffer proof-goals-buffer)
     (goto-char 0)
-    (let 
+    (let
 	((goals nil))
-      (progn 
+      (progn
 	(while (search-forward-regexp pg-pbrpm-start-goal-regexp nil t)
 	  (let
 	      ((hyps nil)
@@ -98,14 +95,14 @@
 			      (search-forward-regexp pg-pbrpm-start-concl-regexp end-goal t)
 			      (match-beginning 0)) 1)))
 		(goto-char start-hyp-text)
-		(setq hyps 
+		(setq hyps
 		      (append
-		       (list start-hyp start-hyp-text end-hyp hyp-name) 
+		       (list start-hyp start-hyp-text end-hyp hyp-name)
 		       hyps))))
 	    
-	    (setq goals 
+	    (setq goals
 		  (append
-		   (list start-goal end-goal goal-num 
+		   (list start-goal end-goal goal-num
 			 (search-forward-regexp pg-pbrpm-start-concl-regexp nil t) hyps)
 		   goals))))
 	  (setq pg-pbrpm-goal-description goals)))))
@@ -130,8 +127,8 @@
 
 (defun pg-pbrpm-eliminate-id (acc l)
   (if (null l) (reverse acc)
-    (if 
-	(pg-pbrpm-exists (lambda (x) 
+    (if
+	(pg-pbrpm-exists (lambda (x)
 			   (string= (car x) (car (car l)))) acc)
 	(pg-pbrpm-eliminate-id acc (cdr l))
       (pg-pbrpm-eliminate-id (cons (car l) acc) (cdr l)))))
@@ -143,9 +140,9 @@ The prover command is processed via pg-pbrpm-run-command."
    (setq click-info (pg-pbrpm-process-click event start end)) ; retrieve click informations
    (if click-info
        (let
-	 ((pbrpm-list 
+	 ((pbrpm-list
 	   (pg-pbrpm-eliminate-id nil (mapcar 'cdr
-					      (sort 
+					      (sort
 					       (proof-pbrpm-generate-menu
 						click-info
 						(pg-pbrpm-process-regions-list))
@@ -180,12 +177,12 @@ The prover command is processed via pg-pbrpm-run-command."
 		   (insert description)
 		   (insert " ") ; hack for renaming of last name
 		   (let ((spans (pg-pbrpm-setup-span pos (point))))
-		     (insert-gui-button (make-gui-button 
+		     (insert-gui-button (make-gui-button
 					 (concat (int-to-string count) ")")
 					 'pg-pbrpm-run-command (list command act spans)) pos))
 		   (insert "\n")))
-		 (insert-gui-button (make-gui-button 
-				   "Cancel" 
+		 (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
 		 (if phox-sym-lock-enabled
@@ -198,20 +195,20 @@ The prover command is processed via pg-pbrpm-run-command."
 
 (defun pg-pbrpm-setup-span (start end)
   "Set up the span in the menu buffer."
-  (save-excursion 
-    (let ((rank 0) (spans nil) (allspan (make-span start end)))
+  (save-excursion
+    (let ((rank 0) (spans nil) (allspan (span-make start end)))
       (while (< start end)
-	(goto-char start)		    
+	(goto-char start)
 	(let ((pos (search-forward "\\[" end 0)) (goalnum 0))
-	  (if pos (progn 
+	  (if pos (progn
 		    (delete-backward-char 2)
 		    (setq end (- end 2))
 		    (setq pos (- pos 2))))
 ;	  (message "make l span %d %d" start (if pos pos end))
-	  (let ((span (make-span start (if pos pos end))))
-	    (set-span-property span 'pglock t)
+	  (let ((span (span-make start (if pos pos end))))
+	    (span-set-property span 'pglock t)
 	    (setq pg-pbrpm-spans (cons span pg-pbrpm-spans)))
-	  (if pos 
+	  (if pos
 	      (progn
 		(search-forward "\\]" end)
 		(delete-backward-char 2)
@@ -226,9 +223,9 @@ The prover command is processed via pg-pbrpm-run-command."
 			  (setq end (- end len))
 			  (setq start (- start len)))
 			(delete-region (match-beginning 0) (match-end 0)))))
-		(let* ((span (make-span pos start))
-		       (str (concat "\\{" (span-string span) 
-				    (if (= goalnum 0) "" 
+		(let* ((span (span-make pos start))
+		       (str (concat "\\{" (span-string span)
+				    (if (= goalnum 0) ""
 				      (concat "\\|" (int-to-string goalnum)))
 				    "\\}"))
 		       (len (- start pos))
@@ -240,20 +237,20 @@ The prover command is processed via pg-pbrpm-run-command."
 		    (delete-region (match-beginning 0) (match-end 0))
 		    (insert (span-string span))
 ;		    (message "span o %d %d"  (match-beginning 0) (+ (match-beginning 0) len))
-		    (setq occurrences (cons (make-span (match-beginning 0) (+ (match-beginning 0) len)) 
+		    (setq occurrences (cons (span-make (match-beginning 0) (+ (match-beginning 0) len))
 					   occurrences))))
 ;		(message "make w span %d %d %s %d" pos start (span-string span) goalnum)
 		(setq spans (cons span spans))
 		(setq rank (+ rank 1))
-		(set-span-property span 'editable t)
-		(set-span-property span 'rank rank)
-		(set-span-property span 'goalnum goalnum)
-		(set-span-property span 'occurrences occurrences)
-		(set-span-property span 'original-text (span-string span))
-		(set-span-property span 'face 'pg-pbrpm-menu-input-face)))
+		(span-set-property span 'editable t)
+		(span-set-property span 'rank rank)
+		(span-set-property span 'goalnum goalnum)
+		(span-set-property span 'occurrences occurrences)
+		(span-set-property span 'original-text (span-string span))
+		(span-set-property span 'face 'pg-pbrpm-menu-input-face)))
 	    (setq start (if pos pos end)))))
-      (cons allspan (sort (reverse spans) (lambda (sp1 sp2) 
-				  (< (span-property sp1 'goalnum) 
+      (cons allspan (sort (reverse spans) (lambda (sp1 sp2)
+				  (< (span-property sp1 'goalnum)
 				     (span-property sp1 'goalnum))))))))
   
 (defun pg-pbrpm-run-command (args)
@@ -264,7 +261,7 @@ The prover command is processed via pg-pbrpm-run-command."
      (if allspan (setq command (concat "(* " (span-string allspan) " *)\n" command ".")))
      ; delete buffer (and its span) after applying "act"
      (pg-pbrpm-erase-regions-list)
-     (if pg-pbrpm-use-buffer-menu 
+     (if pg-pbrpm-use-buffer-menu
 	 (progn
 	   (pg-pbrpm-erase-buffer-menu)
 	   (delete-frame)))
@@ -274,10 +271,10 @@ The prover command is processed via pg-pbrpm-run-command."
        (proof-goto-end-of-locked)
        (proof-activate-scripting)
        (insert (concat "\n" command))
-       (setq span (make-span (proof-locked-end) (point)))
+       (setq span (span-make (proof-locked-end) (point)))
       ; TODO : define the following properties for PBRPM, I don't understand their use ...
-       (set-span-property span 'type 'pbp)
-       (set-span-property span 'cmd command)
+       (span-set-property span 'type 'pbp)
+       (span-set-property span 'cmd command)
        (proof-start-queue (proof-unprocessed-begin) (point)
 			  (list (list span command 'proof-done-advancing))))))
 
@@ -291,7 +288,7 @@ The prover command is processed via pg-pbrpm-run-command."
     s if either the hypothesis name, \"none\" (for the conclusion) of \"whole\" in strange cases"
   (let ((l pg-pbrpm-goal-description)
 	(found nil))
-    (while (and pos l (not found)) 
+    (while (and pos l (not found))
       (setq start-goal (car l))
       (setq end-goal (cadr l))
       (setq goal-name (caddr l))
@@ -302,8 +299,8 @@ The prover command is processed via pg-pbrpm-run-command."
 	  (progn
 	    (setq found t)
 	    (setq the-goal-name goal-name))))
-    (if found 
-	(progn  
+    (if found
+	(progn
 	  (if (<= start-concl pos)
 	      (setq the-click-info "none")
 	    (setq found nil)
@@ -314,7 +311,7 @@ The prover command is processed via pg-pbrpm-run-command."
 	      (setq hyp-name (cadddr hyps))
 	      (setq hyps (cddddr hyps))
 	      (if (and (<= start-hyp pos) (<= pos end-hyp))
-		  (progn 
+		  (progn
 		    (setq found t)
 		    (setq the-click-info hyp-name))))
 	    (if (not found)
@@ -344,7 +341,7 @@ The prover command is processed via pg-pbrpm-run-command."
 	(return-from 'loop "")))))
     
 (defun pg-pbrpm-translate-position (buffer pos)
-  "return pos if buffer is goals-buffer otherwise, return the point position in 
+  "return pos if buffer is goals-buffer otherwise, return the point position in
    the goal buffer"
   (if (eq proof-goals-buffer buffer) pos
     (point proof-goals-buffer)))
@@ -360,9 +357,9 @@ The prover command is processed via pg-pbrpm-run-command."
 	(if r (list
 	       (string-to-number (car r)) ; should not be an int for other prover
 	       (if (eq proof-goals-buffer buffer) (cdr r) (auto-select-arround-pos))
-	       (if (and start end (eq proof-goals-buffer buffer) 
+	       (if (and start end (eq proof-goals-buffer buffer)
 			(<= (marker-position start) pos) (<= pos  (marker-position end)))
-		   (pg-pbrpm-region-expression buffer (marker-position start) 
+		   (pg-pbrpm-region-expression buffer (marker-position start)
 					       (marker-position end))
 		 (auto-select-arround-pos))))))))
 
@@ -373,11 +370,11 @@ The prover command is processed via pg-pbrpm-run-command."
 (defvar pg-pbrpm-regions-list nil)
 
 (defun pg-pbrpm-erase-regions-list ()
-  (mapc (lambda (span) (delete-span span)) pg-pbrpm-regions-list)
+  (mapc (lambda (span) (span-delete span)) pg-pbrpm-regions-list)
   (setq pg-pbrpm-regions-list nil)
   nil)
 
-(add-hook 'mouse-track-drag-up-hook (lambda (event count) 
+(add-hook 'mouse-track-drag-up-hook (lambda (event count)
 				      (if (not (member 'control (event-modifiers event)))
 					  (pg-pbrpm-erase-regions-list))))
 
@@ -386,12 +383,12 @@ The prover command is processed via pg-pbrpm-run-command."
     (setq pg-pbrpm-regions-list nil)
     (mapc (lambda (span) (if (span-live-p span)
 			     (setq pg-pbrpm-regions-list (cons span pg-pbrpm-regions-list))
-			   (delete-span span))) l)))
+			   (span-delete span))) l)))
 
 (defface pg-pbrpm-multiple-selection-face
   (proof-face-specs
    (:background "orange")
-   (:background "darkorange")   
+   (:background "darkorange")
    (:italic t))
   "*Face for showing (multiple) selection."
   :group 'proof-faces)
@@ -399,7 +396,7 @@ The prover command is processed via pg-pbrpm-run-command."
 (defface pg-pbrpm-menu-input-face
   (proof-face-specs
    (:background "Gray80")
-   (:background "Gray65")   
+   (:background "Gray65")
    (:italic t))
   "*Face for showing (multiple) selection."
   :group 'proof-faces)
@@ -407,9 +404,9 @@ The prover command is processed via pg-pbrpm-run-command."
 (defun pg-pbrpm-do-remember-region (start end)
   (pg-pbrpm-filter-regions-list)
    (if (and start end (not (eq start end))) ; if a region is selected
-       (let ((span (make-span start end))
+       (let ((span (span-make start end))
 	     (found nil))
-	 (setq pg-pbrpm-regions-list (reverse (mapcar (lambda (oldspan) 
+	 (setq pg-pbrpm-regions-list (reverse (mapcar (lambda (oldspan)
 		   (let ((oldstart (span-start oldspan))
 			 (oldend (span-end oldspan)))
 		     (if (and (eq (current-buffer) (span-buffer oldspan))
@@ -417,11 +414,11 @@ The prover command is processed via pg-pbrpm-run-command."
 				  (and (<= start oldend) (<= oldend end))))
 			 (progn
 			   (setq found t)
-			   (delete-span oldspan)
-			   span) 
+			   (span-delete oldspan)
+			   span)
 			 oldspan))) pg-pbrpm-regions-list)))
-	 (if (not found) (setq pg-pbrpm-regions-list (cons span pg-pbrpm-regions-list))) 
-	 (set-span-property span 'face 'pg-pbrpm-multiple-selection-face))))
+	 (if (not found) (setq pg-pbrpm-regions-list (cons span pg-pbrpm-regions-list)))
+	 (span-set-property span 'face 'pg-pbrpm-multiple-selection-face))))
 
 ; the follwing are adapted from mouse-track-insert from mouse.el
 
@@ -457,7 +454,7 @@ The prover command is processed via pg-pbrpm-run-command."
 	 (if (eq proof-goals-buffer buffer)
 	     (progn
 	       (setq r (pg-pbrpm-get-region-info start end))
-	       (if r 
+	       (if r
 		   (list
 		    (string-to-number (car r)) ; should not be an int for other prover
 		    (cdr r)
@@ -493,15 +490,16 @@ The prover command is processed via pg-pbrpm-run-command."
 
 ;;--------------------------------------------------------------------------;;
 
-(require 'pg-goals)
-(define-key proof-goals-mode-map [(button3)] 'pg-pbrpm-button-action)
-(define-key proof-goals-mode-map [(control button3)] 'pg-goals-yank-subterm)
-(define-key proof-goals-mode-map [(control button1)] 'pg-pbrpm-remember-region)
-(define-key pg-span-context-menu-keymap [(button3)] 'pg-pbrpm-button-action)
-(define-key pg-span-context-menu-keymap [(control button3)] 'pg-span-context-menu)
-(define-key proof-mode-map [(button3)] 'pg-pbrpm-button-action)
-(define-key proof-mode-map [(control button3)] 'pg-goals-yank-subterm)
-(define-key proof-mode-map [(control button1)] 'pg-pbrpm-remember-region)
+(eval-after-load "pg-goals"
+  '(progn
+     (define-key proof-goals-mode-map [(button3)] 'pg-pbrpm-button-action)
+     (define-key proof-goals-mode-map [(control button3)] 'pg-goals-yank-subterm)
+     (define-key proof-goals-mode-map [(control button1)] 'pg-pbrpm-remember-region)
+     (define-key pg-span-context-menu-keymap [(button3)] 'pg-pbrpm-button-action)
+     (define-key pg-span-context-menu-keymap [(control button3)] 'pg-span-context-menu)
+     (define-key proof-mode-map [(button3)] 'pg-pbrpm-button-action)
+     (define-key proof-mode-map [(control button3)] 'pg-goals-yank-subterm)
+     (define-key proof-mode-map [(control button1)] 'pg-pbrpm-remember-region)))
 
 (provide 'pg-pbrpm)
-;; pg-pbrpm ends here
\ No newline at end of file
+;;; pg-pbrpm ends here
\ No newline at end of file
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index 4b1bbac6..f2a8286e 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -1,6 +1,6 @@
-;; pg-pgip.el	 Functions for processing PGIP for Proof General
+;; pg-pgip.el --- Functions for processing PGIP for Proof General
 ;;
-;; Copyright (C) 2000-2002 LFCS Edinburgh. 
+;; Copyright (C) 2000-2002 LFCS Edinburgh.
 ;; Author:   David Aspinall <David.Aspinall@ed.ac.uk>
 ;; License:  GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -9,7 +9,7 @@
 ;; STATUS: Experimental
 ;;
 ;; Proof General Kit uses PGIP, an XML-message protocol
-;; for interactive proof.  This file contains functions 
+;; for interactive proof.  This file contains functions
 ;; to process PGIP commands sent from the proof assistant
 ;; and to construct PGIP commands to send out.
 ;;
@@ -17,15 +17,21 @@
 ;; useful tracing messages: (setq proof-general-debug t).
 ;;
 ;; TODO NEXT:
-;; -- completion command for completion tables 
+;; -- completion command for completion tables
 ;; -- parsescript input/outputs
 ;; -- guiconfig, some parts of
 ;; -- support fully native PGIP mode
 ;; 
 
+
+;;; Commentary:
+;; 
+
+(require 'cl)				; incf
 (require 'pg-xml)
 (require 'pg-pgip-old)			;; Handle some PGIP 1.X format messages
 
+;;; Code:
 (defalias 'pg-pgip-debug   'proof-debug)
 (defalias 'pg-pgip-error   'error)
 (defalias 'pg-pgip-warning 'pg-internal-warning)
@@ -40,7 +46,7 @@ The list PGIPS may contain one or more PGIP packets, whose contents are processe
   ;; PGIP processing is split into two steps:
   ;; (1) process each command, altering internal data structures
   ;; (2) post-process for each command type, affecting external interface (menus, etc).
-  (mapcar 'pg-pgip-post-process 
+  (mapcar 'pg-pgip-post-process
 	  (reduce 'union (mapcar 'pg-pgip-process-pgip pgips))))
 
 ;; TODO: use id's and sequence numbers to reconstruct streams of messages.
@@ -67,13 +73,13 @@ The list PGIPS may contain one or more PGIP packets, whose contents are processe
       (pg-internal-warning "pg-pgip-process-pgip: expected PGIP element, got %s" name))))
 
 (defun pg-pgip-process-msg (pgipmsg)
-  "Process the PGIP message in the XML node PGIPMSG.  
+  "Process the PGIP message in the XML node PGIPMSG.
 Return a symbol representing the PGIP command processed, or nil."
   (let* ((name        (xml-node-name pgipmsg))
 	 (fname	      (intern (concat "pg-pgip-process-" (symbol-name name)))))
     (if (fboundp fname)
 	(progn
-	  (pg-pgip-debug "Processing PGIP message seq %s, type %s" 
+	  (pg-pgip-debug "Processing PGIP message seq %s, type %s"
 			 (pg-xml-get-attr 'seq pgip 'notreallyoptional) name)
 	  (funcall fname pgipmsg)
 	  name)
@@ -88,7 +94,7 @@ Return a symbol representing the PGIP command processed, or nil."
     (idtable  . pg-pgip-update-idtables)       ;; TODO: not yet implemented
     (addid    . pg-pgip-update-idtables)
     (delid    . pg-pgip-update-idtables))
-  "Table of functions to call after processing PGIP commands")
+  "Table of functions to call after processing PGIP commands.")
 
 (defun pg-pgip-post-process (cmdname)
   "Perform post-processing for a PGIP command type CMDNAME (a symbol)."
@@ -124,10 +130,10 @@ Return a symbol representing the PGIP command processed, or nil."
   ;; we process it by storing a property 'pgml-alt on the elisp symbol.
   (let ((pgmlconfigures (xml-get-children node 'symconfig)))
     (dolist (config pgmlconfigures)
-      (cond 
+      (cond
        ((and (not (stringp config))
 	     (eq (xml-node-name config) "symconfig"))
-	(let 
+	(let
 	    ((symname   (pg-pgip-get-symname node))
 	     (asciialt  (pg-xml-get-attr 'alt node t)))
 	  (put (intern symname)
@@ -172,13 +178,13 @@ Return a symbol representing the PGIP command processed, or nil."
 	 ;; FIXME: this substitution mechanism is not really good enough, we
 	 ;; want to escape XML characters, etc.  Should be possible: turn this
 	 ;; into a function.
-	 (pgipcmd  (concat "<setpref name=\"" name "\" prefcategory=\"" prefcat "\">" 
+	 (pgipcmd  (concat "<setpref name=\"" name "\" prefcategory=\"" prefcat "\">"
 			   subst "</setpref>"))
 	 (symname  (intern name)))
-    (pg-pgip-debug 
+    (pg-pgip-debug
      "haspref calling defpacustom: name:%s default:%s type:%s pgipcmd:%s" symname default type pgipcmd)
     (eval
-     `(defpacustom ,symname ,default 
+     `(defpacustom ,symname ,default
 	(concat descr (if descr "\n")
 		"Setting configured by <haspref> PGIP message")
 	:type (quote ,type)
@@ -231,11 +237,11 @@ Return a symbol representing the PGIP command processed, or nil."
 	     (objtype  (intern (pg-pgip-get-objtype idtable)))
 	     (idents   (mapcar 'pg-xml-get-text-content
 			       (xml-get-children idtable 'identifier)))
-	     (obarray  (or (and (not (eq opn 'setids)) 
+	     (obarray  (or (and (not (eq opn 'setids))
 				(get objtype 'pgsymbols))
 			   ;; new empty obarray for setids or if unset
 			   (put objtype 'pg-symbols (make-vector 31 0)))))
-	(setq proof-assistant-idtables 
+	(setq proof-assistant-idtables
 	      (if (and (null idents) (eq opn 'setids))
 		  (delete objtype proof-assistant-idtables)
 		(adjoin objtype proof-assistant-idtables)))
@@ -245,7 +251,7 @@ Return a symbol representing the PGIP command processed, or nil."
 	 ((eq opn 'delids)
 	  (mapcar (lambda (i) (unintern i obarray)) idents))
 	 (t
-	  (pg-pgip-error "pg-pgip-process-ids: called on wrong node %s" 
+	  (pg-pgip-error "Pg-pgip-process-ids: called on wrong node %s"
 			 (xml-node-name node))))))))
 
 (defun pg-complete-idtable-symbol ()
@@ -258,7 +264,7 @@ Return a symbol representing the PGIP command processed, or nil."
 (defalias 'pg-pgip-process-delids 'pg-pgip-process-ids)
 
 
-(defun pg-pgip-process-idvalue (node) 
+(defun pg-pgip-process-idvalue (node)
   (let ((name     (pg-pgip-get-name node))
 	(objtype  (pg-pgip-get-objtype node))
 	(text     (pg-pgip-get-displaytext node)))
@@ -287,15 +293,15 @@ Return a symbol representing the PGIP command processed, or nil."
 
 (defun pg-pgip-process-cleardisplay (node)
   (let ((area	(pg-pgip-get-area node)))
-    (cond 
+    (cond
      ((equal area "message")
-      (proof-shell-maybe-erase-response nil t t))
+      (pg-response-maybe-erase nil t t))
      ((equal area "display")
       (proof-clean-buffer proof-goals-buffer))
      ((equal area "all")
-      (proof-shell-maybe-erase-response nil t t)
+      (pg-response-maybe-erase nil t t)
       (proof-clean-buffer proof-goals-buffer)
-      ;; TODO: could also erase trace here. 
+      ;; TODO: could also erase trace here.
       ;; [PGIP: Should trace have a separate cat?]
       ))))
 
@@ -326,7 +332,7 @@ Return a symbol representing the PGIP command processed, or nil."
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun pg-pgip-process-informfileloaded (node)
-  (let* ((thyname   (pg-pgip-get-thyname node)) 
+  (let* ((thyname   (pg-pgip-get-thyname node))
 	 (url	    (pg-pgip-get-url node))
 	 (filename  (pg-pgip-get-url-filename url))) ;; FIXME: unimplemented!
     (proof-register-possibly-new-processed-file filename)))
@@ -419,7 +425,7 @@ Also sets local proverid and srcid variables for buffer."
 ;; NB: pgip.rnc v 2.18 only has parsescript sent to prover,
 ;; so if we get here we have a invalid document.
 ;;
-;; Provide parsing functionality for other interfaces (sacrilege!) 
+;; Provide parsing functionality for other interfaces (sacrilege!)
 ;;
   
 (defun pg-pgip-process-parsescript (node)
@@ -452,7 +458,7 @@ Also sets local proverid and srcid variables for buffer."
      ((eq tyname 'pgipbool)	'boolean)
      ((eq tyname 'pgipint) 	'integer) ;; TODO: implement range limits
      ((eq tyname 'pgipstring)	'string)
-     ((eq tyname 'pgipconst)    
+     ((eq tyname 'pgipconst)
       (let ((name	(pg-pgip-get-name node 'optional))
 	    (val	(pg-pgip-get-value node)))
 	(if name
@@ -494,7 +500,7 @@ Also sets local proverid and srcid variables for buffer."
   "Interpret the PGIP value VALUE at (lisp-representation for) TYPE."
   (cond
    ((eq type 'boolean)
-    (cond 
+    (cond
      ((or (string-equal value "true") (string-equal value "1"))  t)
      ((or (string-equal value "false") (string-equal value "0")) nil)
      (t (progn
@@ -521,7 +527,7 @@ Also sets local proverid and srcid variables for buffer."
 	       (string-match "[+-]?[0-9]+$" value))
 	  (setq res (pg-pgip-interpret-value value 'integer)))
 	 ((and (eq type 'boolean)
-	       (or (string-equal value "true") 
+	       (or (string-equal value "true")
 		   (string-equal value "false")
 		   (string-equal value "0")
 		   (string-equal value "1")))
@@ -530,8 +536,8 @@ Also sets local proverid and srcid variables for buffer."
 	  (setq res (pg-pgip-interpret-value value 'string)))))
       (setq choices (cdr choices)))
     (or res
-	(pg-pgip-error 
-	 "pg-pgip-interpret-choice: mismatching value %s for choices %s" 
+	(pg-pgip-error
+	 "pg-pgip-interpret-choice: mismatching value %s for choices %s"
 	 value choices))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -562,9 +568,9 @@ See `pg-pgip-assemble-packet' "
 	  (let ((tm (current-time))) (format "%d.%d" (car tm) (cadr tm))))
   "PGIP Identifier for this Emacs Proof General component.")
 
-(defvar pg-pgip-refseq nil 
+(defvar pg-pgip-refseq nil
   "The sequence number of the received message this reply refers to")
-(defvar pg-pgip-refid nil  
+(defvar pg-pgip-refid nil
   "The identity of the component this message is being sent to")
 
 (defvar pg-pgip-seq 0 "Sequence number of messages sent out.")
@@ -575,8 +581,8 @@ 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
-				     (concat "EmacsPG/" 
-					     proof-general-short-version  
+				     (concat "EmacsPG/"
+					     proof-general-short-version
 					     "/" proof-assistant)))
 	 (id		(pg-xml-attr id pg-pgip-id))
 	 (class		(pg-xml-attr class (or otherclass "pa")))
@@ -593,7 +599,7 @@ This expects a single XML node/string in PGIP, which will have a PGIP
 header attached.  If BLOCK is non-nil, we wait for the response from
 the prover.  For remaining optional args, see doc of
 `pgip-assemble-packet'."
-  (proof-shell-invisible-command 
+  (proof-shell-invisible-command
    (pg-pgip-string-of-command pgip refseq refid otherclass) block))
 
 
@@ -616,13 +622,13 @@ the prover.  For remaining optional args, see doc of
 
 (defun pg-pgip-askids (&optional objtype thyname)
   "Send an <askids> message to the prover."
-  (pg-pgip-issue 
-   (pg-xml-node askids 
+  (pg-pgip-issue
+   (pg-xml-node askids
 		(append
 		 (if thyname
 		     (list (pg-xml-attr 'thyname objtype)))
 		 (if objtype
-		     (list (pg-xml-attr 'objtype objtype)))) 
+		     (list (pg-xml-attr 'objtype objtype))))
 		nil)
    'block))
 
@@ -664,4 +670,4 @@ the prover.  For remaining optional args, see doc of
 
 
 (provide 'pg-pgip)
-;; End of `pg-pgip.el'
+;;; pg-pgip.el ends here
diff --git a/generic/pg-response.el b/generic/pg-response.el
index a1058f18..b9d2e5cc 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -1,19 +1,35 @@
-;; pg-response.el  Proof General response buffer mode.
+;; pg-response.el --- Proof General response buffer mode.
 ;;
-;; Copyright (C) 1994-2004 LFCS Edinburgh. 
-;; Authors:   David Aspinall, Healfdene Goguen, 
+;; Copyright (C) 1994-2008 LFCS Edinburgh.
+;; Authors:   David Aspinall, Healfdene Goguen,
 ;;		Thomas Kleymann and Dilip Sequeira
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
+;;; Commentary:
+;; 
 ;; This mode is used for the response buffer proper, and
-;; also the trace and theorems buffer.
+;; also the trace and theorems buffer. A sub-module of proof-shell.
+;;
 
-;; A sub-module of proof-shell; assumes proof-script loaded.
-(require 'pg-assoc)
+;;; Code:
+
+(eval-when-compile
+  (require 'easymenu)			; easy-menu-add
+  (require 'proof-utils))		; deflocal, proof-eval-when-ready-for-assistant
 
 (require 'bufhist)
+(require 'pg-assoc)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Local variables
+;;
+
+(deflocal pg-response-eagerly-raise t
+  "Non-nil if this buffer will be eagerly raised/displayed on startup.")
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -21,7 +37,7 @@
 ;; Response buffer mode
 ;;
 
-(eval-and-compile
+;;;###autoload
 (define-derived-mode proof-response-mode proof-universal-keys-only-mode
   "PGResp" "Responses from Proof Assistant"
   (setq proof-buffer-type 'response)
@@ -30,7 +46,6 @@
   (define-key proof-response-mode-map [(button2)] 'pg-goals-button-action)
   (define-key proof-response-mode-map [q] 'bury-buffer)
   (define-key proof-response-mode-map [c] 'pg-response-clear-displays)
-  (make-local-hook 'kill-buffer-hook)
   (add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
   (easy-menu-add proof-response-mode-menu proof-response-mode-map)
   (easy-menu-add proof-assistant-menu proof-response-mode-map)
@@ -39,14 +54,15 @@
   (erase-buffer)
   (buffer-disable-undo)
   (if proof-keep-response-history (bufhist-mode)) ; history for contents
-  (set-buffer-modified-p nil)))
-
-(easy-menu-define proof-response-mode-menu
-		  proof-response-mode-map
-		  "Menu for Proof General response buffer."
-		  proof-aux-menu)
+  (set-buffer-modified-p nil))
 
+(proof-eval-when-ready-for-assistant ; proof-aux-menu depends on <PA>
+    (easy-menu-define proof-response-mode-menu
+      proof-response-mode-map
+      "Menu for Proof General response buffer."
+      (proof-aux-menu)))
 
+;;;###autoload
 (defun proof-response-config-done ()
   "Complete initialisation of a response-mode derived buffer."
   (proof-font-lock-configure-defaults nil)
@@ -68,17 +84,17 @@
 ;; "#### Change, not compatible with FSF: This stuff is all so incredibly
 ;; junky anyway that I doubt it makes any difference."
 
-(defvar proof-shell-special-display-regexp nil
-  "Regexp for special-display-regexps for multiple frame use.
+(defvar pg-response-special-display-regexp nil
+  "Regexp for `special-display-regexps' for multiple frame use.
 Internal variable, setting this will have no effect!")
 
 ;; NB: this list uses XEmacs defaults in the non-multiframe case.
-;; We handle specifiers quit crudely, bute (1) to set for the 
+;; We handle specifiers quit crudely, bute (1) to set for the
 ;; frame specifically we'd need to get hold of the frame,
 ;; (2) specifiers have been (still are) quite buggy.
-(defconst proof-multiframe-specifiers 
-  (if proof-running-on-XEmacs
-      (list 
+(defconst proof-multiframe-specifiers
+  (if (featurep 'xemacs)
+      (list
        (list has-modeline-p nil nil) ;; nil even in ordinary case.
        (list menubar-visible-p nil t)
        (list default-gutter-visible-p nil t)
@@ -91,9 +107,10 @@ Internal variable, setting this will have no effect!")
     ;; FIXME: Unfortunately these specifiers seem to get lost very
     ;; easily --- the toolbar, gutter, modeline all come back
     ;; for no good reason.  Can we construct a simple bug example?
-    (set-specifier (car spec) 
-		   (if multiframep (cadr spec) (caddr spec))
-		    locale)))
+    (if (fboundp 'set-specifier) ; nuke compile warning
+	(set-specifier (car spec)
+		       (if multiframep (cadr spec) (caddr spec))
+		       locale))))
 
 (defconst proof-multiframe-parameters
   '((minibuffer . nil)
@@ -105,25 +122,21 @@ Internal variable, setting this will have no effect!")
   "List of GNU Emacs frame parameters for secondary frames.")
 
 (defun proof-multiple-frames-enable ()
-  (if proof-running-on-XEmacs
+  (if (featurep 'xemacs)
       (proof-map-buffers
        (proof-associated-buffers)
        (proof-map-multiple-frame-specifiers proof-multiple-frames-enable
 					    (current-buffer))))
-  (let ((spdres 
-	 (if proof-running-on-XEmacs
-	     proof-shell-special-display-regexp
-	   ;; GNU Emacs uses this to set frame params too, handily
-	   (cons 
-	    proof-shell-special-display-regexp
+  (let ((spdres
+	 (if (featurep 'xemacs)
+	     pg-response-special-display-regexp
+	   (cons ; GNU Emacs uses this to set frame params too, handily
+	    pg-response-special-display-regexp
 	    proof-multiframe-parameters))))
-    (cond
-     (proof-multiple-frames-enable
-      (setq special-display-regexps
-	    (union special-display-regexps (list spdres))))
-     (t
+    (if proof-multiple-frames-enable
+	(add-to-list 'special-display-regexps spdres)
       (setq special-display-regexps
-	    (delete spdres special-display-regexps)))))
+	    (delete spdres special-display-regexps))))
   (proof-layout-windows))
 
 (defun proof-three-window-enable ()
@@ -152,9 +165,9 @@ Internal variable, setting this will have no effect!")
    (or proof-script-buffer (first (buffer-list)))
    ;; Pierre had response buffer first, I think goals
    ;; is a bit nicer though?
-   (if (buffer-live-p proof-goals-buffer) 
+   (if (buffer-live-p proof-goals-buffer)
        proof-goals-buffer (first (buffer-list)))
-   (if (buffer-live-p proof-response-buffer) 
+   (if (buffer-live-p proof-response-buffer)
        proof-response-buffer (first (buffer-list)))
    nohorizontalsplit))
    
@@ -180,7 +193,7 @@ prevent the horizontal split, and result in three windows spanning the
 full width of the Emacs frame.
 
 For multiple frame mode, this function obeys the setting of
-`proof-eagerly-raise', which see."
+`pg-response-eagerly-raise', which see."
   (interactive "P")
   (cond
    (proof-multiple-frames-enable
@@ -188,7 +201,7 @@ For multiple frame mode, this function obeys the setting of
     (if proof-script-buffer
 	(switch-to-buffer proof-script-buffer))
     (proof-map-buffers (proof-associated-buffers)
-      (if proof-eagerly-raise
+      (if pg-response-eagerly-raise
 	  (proof-display-and-keep-buffer (current-buffer))))
     ;; Restore an existing frame configuration (seems buggy, typical)
     (if pg-frame-configuration
@@ -198,7 +211,7 @@ For multiple frame mode, this function obeys the setting of
     (proof-delete-other-frames)
     (set-window-dedicated-p (selected-window) nil)
     (proof-display-three-b nohorizontalsplit))
-   ;; Two-of-three window mode.  
+   ;; Two-of-three window mode.
    ;; Show the response buffer as first in preference order.
    (t
     (proof-delete-other-frames)
@@ -215,17 +228,17 @@ For multiple frame mode, this function obeys the setting of
     ;; frame for the associated buffer, we may delete
     ;; the main frame!!
     (let ((mainframe
-	   (window-frame 
+	   (window-frame
 	    (if proof-script-buffer
 		(proof-get-window-for-buffer proof-script-buffer)
 	      ;; We may lose with just selected window
 	      (selected-window)))))
       (proof-map-buffers (proof-associated-buffers)
-	(let* ((win  
+	(let* ((win
 		;; NB: g-w-f-b will re-display in new frame if
 		;; the buffer isn't selected/visible.  This causes
 		;; new frame to flash up and be deleted if already
-		;; deleted!  
+		;; deleted!
 		;; (proof-get-window-for-buffer (current-buffer))
 		;; This next choice is probably better:
 		(get-buffer-window (current-buffer) 'visible))
@@ -240,9 +253,10 @@ For multiple frame mode, this function obeys the setting of
 
 ;; Flag and function to keep response buffer tidy.
 (defvar pg-response-erase-flag nil
-  "Indicates that the response buffer should be cleared before next message.")
+  "Non-nil means the response buffer should be cleared before next message.")
 
-(defun proof-shell-maybe-erase-response
+;;;###autoload
+(defun pg-response-maybe-erase
   (&optional erase-next-time clean-windows force)
   "Erase the response buffer according to pg-response-erase-flag.
 ERASE-NEXT-TIME is the new value for the flag.
@@ -258,7 +272,7 @@ Returns non-nil if response buffer was cleared."
     (let ((doit (or (and
 		     proof-tidy-response
 		     (not (eq pg-response-erase-flag 'invisible))
-		     pg-response-erase-flag) 
+		     pg-response-erase-flag)
 		    force)))
       (if doit
 	  (if clean-windows
@@ -267,7 +281,7 @@ Returns non-nil if response buffer was cleared."
 	  ;; (erase-buffer proof-response-buffer)
 	    (with-current-buffer proof-response-buffer
 	      (setq pg-response-next-error nil)	; all error msgs lost!
-	      (if (> (buffer-size) 0)		     
+	      (if (> (buffer-size) 0)
 		  (bufhist-checkpoint-and-erase))
 	      (set-buffer-modified-p nil))))
       (setq pg-response-erase-flag erase-next-time)
@@ -278,22 +292,21 @@ Returns non-nil if response buffer was cleared."
   (unless (or proof-shell-unicode
 	      pg-use-specials-for-fontify)
     (setq str (pg-assoc-strip-subterm-markup str)))
-  (proof-shell-maybe-erase-response t nil)
+  (pg-response-maybe-erase t nil)
   ;;(unless (or (string-equal str "") (string-equal str "\n"))
     ;; don't display an empty buffer [ NB: above test repeated below,
     ;; but response-display reused elsewhere ]
   (pg-response-display-with-face str)
   ;; NB: this displays an empty buffer sometimes when it's not
   ;; so useful.  It _is_ useful if the user has requested to
-  ;; see the proof state and there is none 
+  ;; see the proof state and there is none
   ;; (Isabelle/Isar displays nothing: might be better if it did).
   (proof-display-and-keep-buffer proof-response-buffer))
   
-;; FIXME: this function should be combined with
-;; proof-shell-maybe-erase-response-buffer. 
+;; TODO: this function should be combined with
+;; pg-response-maybe-erase-buffer.
 (defun pg-response-display-with-face (str &optional face)
   "Display STR with FACE in response buffer."
-  ;; 3.4: no longer return fontified STR, it wasn't used.
   (cond
    ((string-equal str ""))
    ((string-equal str "\n"))		; quick exit, no display.
@@ -315,7 +328,7 @@ Returns non-nil if response buffer was cleared."
 	;; Do pbp markup here, e.g. for "sendback" commands.
 	;; NB: we might loose if markup has been split between chunks, but this
 	;; will could only happen in cases of huge (spilled) output
-	(pg-goals-analyse-structure start (point-max))
+	(pg-assoc-analyse-structure start (point-max))
 	
 	(proof-fontify-region start (point))
 
@@ -323,7 +336,7 @@ Returns non-nil if response buffer was cleared."
 	;; minor mode: it destroys this hacky property as soon as it's
 	;; made!  (Using the minor mode is much more convenient, tho')
 	(if (and face proof-output-fontify-enable)
-	    (font-lock-append-text-property 
+	    (font-lock-append-text-property
 	     start (point-max) 'face face))
 
 	(set-buffer-modified-p nil))))))
@@ -336,7 +349,7 @@ it becomes overly long.  Particularly useful when `proof-tidy-response'
 is set to nil, so responses are not cleared automatically."
   (interactive)
   (proof-map-buffers (list proof-response-buffer proof-trace-buffer)
-    (if (> (buffer-size) 0)		     
+    (if (> (buffer-size) 0)
 	(bufhist-checkpoint-and-erase))
     (set-buffer-modified-p nil)))
 
@@ -347,16 +360,14 @@ is set to nil, so responses are not cleared automatically."
 ;; Next error function.
 ;;
 
-(defvar pg-response-next-error nil
-  "Error counter in response buffer to count for next error message.")
-
 ;;;###autoload
 (defun proof-next-error (&optional argp)
   "Jump to location of next error reported in the response buffer.
 
 A prefix arg specifies how many error messages to move;
 negative means move back to previous error messages.
-Just C-u as a prefix means reparse the error message buffer
+
+Optional argument ARGP means reparse the error message buffer
 and start at the first error."
   (interactive "P")
   (if (and ;; At least one setting must be configured
@@ -364,7 +375,7 @@ and start at the first error."
        ;; Response buffer must be live
        (or
 	(buffer-live-p proof-response-buffer)
-	(error "proof-next-error: no response buffer to parse!")))
+	(error "Next error: no response buffer to parse!")))
       (let ((wanted-error    (or (and (not (consp argp))
 				      (+ (prefix-numeric-value argp)
 					 (or pg-response-next-error 0)))
@@ -373,7 +384,7 @@ and start at the first error."
 	    line column file errpos)
 	(set-buffer proof-response-buffer)
 	(goto-char (point-min))
-	(if (re-search-forward pg-next-error-regexp 
+	(if (re-search-forward pg-next-error-regexp
 			       nil t wanted-error)
 	    (progn
 	      (setq errpos (save-excursion
@@ -390,25 +401,25 @@ and start at the first error."
 		     ;; Look for the most recently mentioned filename
 		     (re-search-backward
 		      pg-next-error-filename-regexp nil t))
-		    (setq file 
+		    (setq file
 			  (if (file-exists-p (match-string 2))
 			      (match-string 2)
 			    ;; May need post-processing to extract filename
 			    (if pg-next-error-extract-filename
-				(format 
-				 pg-next-error-extract-filename 
+				(format
+				 pg-next-error-extract-filename
 				 (match-string 2))))))
 		;; Now find the other buffer we need to display
 		(let*
-		    ((errbuf	
+		    ((errbuf
 		      (if file
 			  (find-file-noselect file)
-			(or proof-script-buffer 
+			(or proof-script-buffer
 			    ;; We could make more guesses here,
-			    ;; e.g. last script buffer active 
+			    ;; e.g. last script buffer active
 			    ;; (keep a record of it?)
-			    (error 
-			     "proof-next-error: can't guess file for error message"))))
+			    (error
+			     "Next error: can't guess file for error message"))))
 		     (pop-up-windows t)
 		     (rebufwindow
 		      (or (get-buffer-window proof-response-buffer 'visible)
@@ -428,7 +439,7 @@ and start at the first error."
 		  (if (and column (> column 1))
 		      (move-to-column (1- column)))))
 	    (setq pg-response-next-error nil)
-	    (error "proof-next-error: couldn't find a next error.")))))
+	    (error "Next error: couldn't find a next error")))))
 
 ;;;###autoload
 (defun pg-response-has-error-location ()
@@ -463,21 +474,21 @@ See `pg-next-error-regexp'."
 	  (point-min);; in case buffer cleared
 	proof-trace-last-fontify-pos)))
 
-;; An analogue of pg-response-display-with-face 
+;; An analogue of pg-response-display-with-face
 (defun proof-trace-buffer-display (str)
   "Output STR in the trace buffer, moving the pointer downwards.
 We fontify the output only if we're not too busy to do so."
   (with-current-buffer proof-trace-buffer
     (goto-char (point-max))
     (newline)
-    (or proof-trace-last-fontify-pos 
+    (or proof-trace-last-fontify-pos
 	(setq proof-trace-last-fontify-pos (point)))
     (insert str)
     (unless (bolp)
       (newline))
     ;; If tracing output is prolific, we try to avoid
     ;; fontifying every chunk and batch it up instead.
-    (unless pg-tracing-slow-mode
+    (unless pg-tracing-slow-mode ; defined in proof-shell.el
       (let ((fontifystart (proof-trace-fontify-pos)))
 	;; Catch errors here: this is to deal with ugly problem when
 	;; fontification of large output gives error Nesting too deep
@@ -502,19 +513,19 @@ We fontify the output only if we're not too busy to do so."
 ;;
 ;; Theorems buffer
 ;;
-;; New in PG 3.5.  
+;; [ INCOMPLETE ]
 ;;
 ;; Revives an old idea from Isamode: a buffer displaying a bunch
 ;; of theorem names.
 ;;
-
+;; 
 
 (defun pg-thms-buffer-clear ()
   "Clear the theorems buffer."
   (with-current-buffer proof-thms-buffer
     (let (start str)
       (goto-char (point-max))
-      (newline)				
+      (newline)
       (setq start (point))
       (insert str)
       (unless (bolp) (newline))
@@ -522,11 +533,5 @@ We fontify the output only if we're not too busy to do so."
       (set-buffer-modified-p nil))))
 
 
-
-
-
-
-
-
 (provide 'pg-response)
-;; pg-response.el ends here.
+;;; pg-response.el ends here
diff --git a/generic/pg-thymodes.el b/generic/pg-thymodes.el
index a709d0cb..333e8829 100644
--- a/generic/pg-thymodes.el
+++ b/generic/pg-thymodes.el
@@ -1,21 +1,25 @@
-;; pg-thymodes.el  Proof General "theory" modes.
+;; pg-thymodes.el --- Proof General "theory" modes.
 ;;
-;; Copyright (C) 2002 LFCS Edinburgh. 
+;; Copyright (C) 2002 LFCS Edinburgh.
 ;; Author:   David Aspinall
 ;; License:  GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
+;;; Commentary:
+;; 
 ;; Functions for defining "theory" modes, i.e.  modes for
 ;; non-interactive proof assistant files which do not contain proof
 ;; scripts.
 ;;
 ;; STATUS: in progress, experimental; needs macro debugging.
 
+
 (require 'proof)
 
 
 ;;;###autoload
+;;; Code:
 (defmacro pg-defthymode (sym name &rest body)
   "Define a Proof General mode for theory files.
 Mode name is SYM-mode, named NAMED.  BODY is the body of a setq and
@@ -30,7 +34,7 @@ can define a number of variables for the mode, viz:
 All of these settings are optional."
   (progn
     (eval `(setq ,@body))
-    (let* 
+    (let*
 	;; See what was defined
 	((mode	      (intern (concat (symbol-name sym) "-mode")))
 	 (parentmode  (pg-modesymval sym 'parent-mode 'fundamental-mode))
@@ -53,9 +57,9 @@ All of these settings are optional."
 	  (pg-do-unless-null ,syntaxes (mapcar 'modify-syntax-entry ,syntaxes))))
        ;; Define the menu (final value of macro to be evaluated)
        `(pg-do-unless-null ,menu
-			   `(easy-menu-define 
+			   `(easy-menu-define
 			     ,menusym ,keymap
-			     ,(concat "Menu for " 
+			     ,(concat "Menu for "
 				      (symbol-name mode)
 				      " defined by `pg-defthymode'.")
 			     ,menu)))))
@@ -71,7 +75,7 @@ All of these settings are optional."
 
 (defun pg-symval (sym &optional other)
   "Return (symbol-value SYM) or nil/OTHER if SYM unbound."
-  (if (boundp sym) 
+  (if (boundp sym)
       (symbol-value sym)
     other))
 
@@ -90,4 +94,4 @@ All of these settings are optional."
   
 
 (provide 'pg-thymodes)
-;; pg-thymodes.el ends here.
+;;; pg-thymodes.el ends here
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 6b7de5a8..38217689 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1,21 +1,22 @@
-;; pg-user.el   User level commands for Proof General
+;; pg-user.el --- User level commands for Proof General
 ;;
-;; Copyright (C) 2000-2002 LFCS Edinburgh. 
+;; Copyright (C) 2000-2002 LFCS Edinburgh.
 ;; Author:     David Aspinall and others
 ;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
 ;;
+;;; Commentary:
+;; 
 
-(require 'proof-config)			; for proof-follow-mode
-
-
+;;; Code:
 
+(require 'proof-utils)			; deflocal, proof-deftoggle
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; first a couple of helper functions 
+;; first a couple of helper functions
 ;;
 
 (defmacro proof-maybe-save-point (&rest body)
@@ -84,7 +85,7 @@ deleted text."
   ;; when deleting.
   ;; Unfortunately nasty problem with read only flag when
   ;; inserting at (proof-locked-end) sometimes behaves as if
-  ;; point is inside locked region  (prob because span is 
+  ;; point is inside locked region  (prob because span is
   ;;  [ ) and not [ ] -- why??).
   ;; (proof-script-new-command-advance)
   )
@@ -137,7 +138,7 @@ the proof script."
 (defun proof-interrupt-process ()
   "Interrupt the proof assistant.  Warning! This may confuse Proof General.
 This sends an interrupt signal to the proof assistant, if Proof General
-thinks it is busy.  
+thinks it is busy.
 
 This command is risky because when an interrupt is trapped in the
 proof assistant, we don't know whether the last command succeeded or
@@ -150,7 +151,7 @@ handling of interrupt signals."
   (unless proof-shell-busy
     (error "Proof Process Not Active!"))
   (with-current-buffer proof-shell-buffer
-    ;; Just send an interrrupt.  
+    ;; Just send an interrrupt.
     ;; Action on receiving one is triggered in proof-shell
     (comint-interrupt-subjob)
     (run-hooks 'proof-shell-pre-interrupt-hook)))
@@ -166,12 +167,12 @@ handling of interrupt signals."
   (interactive)
   (let* ((cmd (span-at (point) 'type))
 	 (start (if cmd (span-start cmd))))
-    (if start 
+    (if start
 	(progn
 	  ;; BUG: only works for unclosed proofs.
 	  (goto-char start))
       (let ((semis (nth 1 (proof-segment-up-to (point) t))))
-	(if (eq 'unclosed-comment (car-safe semis)) 
+	(if (eq 'unclosed-comment (car-safe semis))
 	    (setq semis (cdr-safe semis)))
 	(if (nth 2 semis) ; fetch end point of previous command
 	      (goto-char (nth 2 semis))
@@ -190,8 +191,8 @@ handling of interrupt signals."
   (let ((cmd (span-at (point) 'type)))
     (if cmd (goto-char (span-end cmd))
 ;      (and (re-search-forward "\\S-" nil t)
-;	   (proof-assert-until-point nil 'ignore-proof-process)) 
-      (proof-assert-next-command nil 
+;	   (proof-assert-until-point nil 'ignore-proof-process))
+      (proof-assert-next-command nil
 				 'ignore-proof-process
 				 'dontmoveforward))
     (skip-chars-backward " \t\n")
@@ -218,7 +219,7 @@ handling of interrupt signals."
   
 
 ;; FIXME da: this is an oddity.  It copies the span, but does not
-;; send it, contrary to it's old name ("proof-send-span").   
+;; send it, contrary to it's old name ("proof-send-span").
 ;; Now made more general to behave like mouse-track-insert
 ;; when not over a span.
 ;; FIXME da: improvement would be to allow selection of part
@@ -246,9 +247,9 @@ If there is no command under the mouse, behaves like mouse-track-insert."
 		;; comments, and supresses leading spaces, at least.
 		;; Odd.
 		(span-property span 'cmd)))))))
-    ;; Insert copied command in original window, 
+    ;; Insert copied command in original window,
     ;; buffer, point position.
-    (if str 
+    (if str
 	(insert str proof-script-command-separator)
       (mouse-track-insert event))))
 
@@ -260,7 +261,7 @@ If there is no command under the mouse, behaves like mouse-track-insert."
 ;;
 
 (defvar proof-minibuffer-history nil
-  "History of proof commands read from the minibuffer")
+  "History of proof commands read from the minibuffer.")
 
 (defun proof-minibuffer-cmd (cmd)
   "Prompt for a command in the minibuffer and send it to proof assistant.
@@ -270,7 +271,7 @@ If a prefix arg is given and there is a selected region, that is
 pasted into the command.  This is handy for copying terms, etc from
 the script.
 
-If `proof-strict-state-preserving' is set, and `proof-state-preserving-p' 
+If `proof-strict-state-preserving' is set, and `proof-state-preserving-p'
 is configured, then the latter is used as a check that the command
 will be safe to execute, in other words, that it won't ruin
 synchronization.  If when applied to the command it returns false,
@@ -281,9 +282,9 @@ WARNING: this command risks spoiling synchronization if the test
 only an approximate test, or if `proof-strict-state-preserving'
 is off (nil)."
   (interactive
-   (list (read-string "Command: " 
+   (list (read-string "Command: "
 		      (if (and current-prefix-arg (region-exists-p))
-			  (replace-in-string 
+			  (replace-in-string
 			   (buffer-substring (region-beginning) (region-end))
 			   "[ \t\n]+" " "))
 		      'proof-minibuffer-history)))
@@ -304,7 +305,7 @@ is off (nil)."
 ;; pear-shaped.
 
 ;; In fact, it's so risky, we'll disable it by default
-(if (if proof-running-on-XEmacs
+(if (if (featurep 'xemacs)
 	(get 'proof-frob-locked-end 'disabled t)
       ;; FSF code more approximate
       (not (member 'disabled (symbol-plist 'proof-frob-locked-end))))
@@ -325,14 +326,14 @@ a proof command."
    (proof-shell-busy
     (error "You can't use this command while %s is busy!" proof-assistant))
    ((not (eq (current-buffer) proof-script-buffer))
-    (error "Must be in the active scripting buffer."))
+    (error "Must be in the active scripting buffer"))
    ;; Sometimes may need to move point forwards, when locked region
    ;; is editable.
    ;; ((> (point) (proof-locked-end))
    ;; (error "You can only move point backwards."))
    ;; FIXME da: should move to a command boundary, really!
-   (t (proof-set-locked-end (point))	
-      (delete-spans (proof-locked-end) (point-max) 'type))))
+   (t (proof-set-locked-end (point))
+      (span-delete-spans (proof-locked-end) (point-max) 'type))))
 
 
 
@@ -379,7 +380,7 @@ a proof command."
 ;;; Non-scripting proof assistant commands.
 ;;;
 
-;;; These are based on defcustom'd settings so that users may 
+;;; These are based on defcustom'd settings so that users may
 ;;; re-configure the system to their liking.
 
 
@@ -407,7 +408,7 @@ a proof command."
   "Give error if a configuration setting VAR is unset, otherwise eval BODY."
   `(if ,var
        (progn ,@body)
-     (error "Proof General not configured for this: set %s" 
+     (error "Proof General not configured for this: set %s"
 	    ,(symbol-name var))))
 
 ;;;###autoload
@@ -415,9 +416,9 @@ a proof command."
   "Define command FN to send string BODY to proof assistant, based on CMDVAR.
 BODY defaults to CMDVAR, a variable."
   `(defun ,fn ()
-     ,(concat doc 
-	      (concat "\nIssues a command to the assistant based on " 
-		      (symbol-name cmdvar) ".") 
+     ,(concat doc
+	      (concat "\nIssues a command to the assistant based on "
+		      (symbol-name cmdvar) ".")
 		"")
      (interactive)
      (proof-if-setting-configured ,cmdvar
@@ -431,14 +432,14 @@ CMDVAR is a variable holding a function or string.  Automatically has history."
      (defvar ,(intern (concat (symbol-name fn) "-history")) nil
        ,(concat "History of arguments for " (symbol-name fn) "."))
      (defun ,fn (arg)
-     ,(concat doc "\nIssues a command based on ARG to the assistant, using " 
+     ,(concat doc "\nIssues a command based on ARG to the assistant, using "
 	      (symbol-name cmdvar) ".\n"
 	      "The user is prompted for an argument.")
       (interactive
        (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))))
@@ -469,15 +470,15 @@ Start up the proof assistant if necessary."
 (proof-define-assistant-command proof-prf
   "Show the current proof state."
   proof-showproof-command
-  (progn 
+  (progn
     (pg-goals-buffers-hint)
     proof-showproof-command))
 
-(proof-define-assistant-command proof-ctxt 
+(proof-define-assistant-command proof-ctxt
   "Show the current context."
   proof-context-command)
 
-(proof-define-assistant-command proof-help 
+(proof-define-assistant-command proof-help
   "Show a help or information message from the proof assistant.
 Typically, a list of syntax of commands available."
   proof-info-command)
@@ -485,7 +486,7 @@ Typically, a list of syntax of commands available."
 (proof-define-assistant-command proof-cd
   "Change directory to the default directory for the current buffer."
   proof-shell-cd-cmd
-  (proof-format-filename proof-shell-cd-cmd 
+  (proof-format-filename proof-shell-cd-cmd
 	  ;; FSF fix: use default-directory rather than fn
 	  default-directory))
 
@@ -493,8 +494,8 @@ Typically, a list of syntax of commands available."
   "If proof-shell-cd-cmd is set, do proof-cd and wait for prover ready.
 This is intended as a value for proof-activate-scripting-hook"
   ;; The hook is set in proof-mode before proof-shell-cd-cmd may be set,
-  ;; so we explicitly test it here.  
-  (if proof-shell-cd-cmd 
+  ;; so we explicitly test it here.
+  (if proof-shell-cd-cmd
       (progn
 	(proof-cd)
 	(proof-shell-wait))))
@@ -518,7 +519,7 @@ This is intended as a value for proof-activate-scripting-hook"
  (let ((proof-one-command-per-line t))   ; Goals always start at a new line
    (proof-issue-new-command arg)))
 
-(proof-define-assistant-command-witharg proof-issue-save 
+(proof-define-assistant-command-witharg proof-issue-save
  "Write a save/qed command in the script, prompting for the theorem name."
  proof-save-command
  "Save as"
@@ -555,7 +556,7 @@ This is intended as a value for proof-activate-scripting-hook"
 Make sure the modeline is updated to display new value for electric terminator."
   (if proof-mode-for-script
       (proof-map-buffers (proof-buffers-in-mode proof-mode-for-script)
-			 (setq proof-electric-terminator 
+			 (setq proof-electric-terminator
 			       proof-electric-terminator-enable)))
   (redraw-modeline))
 
@@ -564,21 +565,21 @@ Make sure the modeline is updated to display new value for electric terminator."
 (defun proof-electric-term-incomment-fn ()
   "Used as argument to proof-assert-until-point."
   ;; CAREFUL: (1) dynamic scoping here  (incomment, ins, mrk)
-  ;;          (2) needs this name to be recognized in 
+  ;;          (2) needs this name to be recognized in
   ;;		  proof-assert-until-point
   (setq incomment t)
   (if ins (backward-delete-char 1))
   (goto-char mrk)
   (insert proof-terminal-string))
 
-;; FIXME da: this function is a mess and needs rewriting.  
+;; FIXME da: this function is a mess and needs rewriting.
 ;;  (proof-assert-until-point process needs cleaning up)
 ;;
-;; What it should do: 
+;; What it should do:
 ;;   * parse FIRST.  If we're inside a comment or string,
 ;;     then insert the terminator where we are.  Otherwise
 ;;     can skip backwards and insert the terminator at the
-;;     command end (perhaps optionally), and look for 
+;;     command end (perhaps optionally), and look for
 ;;     existing terminator.
 
 (defun proof-process-electric-terminator ()
@@ -595,14 +596,14 @@ comment, and insert or skip to the next semi)."
       ;; Otherwise, do other thing.
       ;; Old idea: only shift terminator wildly if we're looking at
       ;; whitespace.  Why?
-      ;; (if (looking-at "\\s-\\|\\'\\|\\w") 
+      ;; (if (looking-at "\\s-\\|\\'\\|\\w")
       (if (proof-only-whitespace-to-locked-region-p)
 	  (error "There's nothing to do!"))
 
       (if (not (= (char-after (point)) proof-terminal-char))
-	  (progn 
+	  (progn
 	    (forward-char) ;; immediately after command end.
-	    (insert proof-terminal-string) 
+	    (insert proof-terminal-string)
 	    (setq ins t)))
       (proof-assert-until-point 'proof-electric-term-incomment-fn)
       (or incomment
@@ -613,7 +614,7 @@ comment, and insert or skip to the next semi)."
 If proof-electric-terminator-enable is non-nil, the command will be
 sent to the assistant."
   (interactive)
-  (if proof-electric-terminator-enable 
+  (if proof-electric-terminator-enable
       (proof-process-electric-terminator)
     (self-insert-command 1)))
 
@@ -628,7 +629,7 @@ sent to the assistant."
 ;; a hand-wavy thing, so we don't make any attempt to maintain
 ;; a precise completion table or anything.
 ;;
-;; New in 3.2.  
+;; New in 3.2.
 ;;
 (defun proof-add-completions ()
   "Add completions from <PA>-completion-table to completion database.
@@ -636,7 +637,7 @@ Uses `add-completion' with a negative number of uses and ancient
 last use time, to discourage saving these into the users database."
   (interactive)
   (require 'completion)
-  (mapcar (lambda (cmpl) 
+  (mapcar (lambda (cmpl)
 	    ;; completion gives error in this case; trapping
 	    ;; the error here is tricky in FSF Emacs so duplicate
 	    ;; the test.
@@ -644,10 +645,10 @@ last use time, to discourage saving these into the users database."
 		(add-completion cmpl -1000 0)))
 	  (proof-ass completion-table)))
 
-;; NB: completion table is expected to be set when proof-script 
+;; NB: completion table is expected to be set when proof-script
 ;; is loaded!  Can call proof-script-add-completions if the table
 ;; is updated.
-(eval-after-load "completion" 
+(eval-after-load "completion"
   '(proof-add-completions))
 
 (defun proof-script-complete (&optional arg)
@@ -692,7 +693,7 @@ last use time, to discourage saving these into the users database."
 	  (insert proof-shell-last-output)
 	  ;; 3.4: add fontification. Questionable since comments will
 	  ;; probably be re-highlighted, so colouration, especially
-	  ;; based on removed specials, will be lost.  
+	  ;; based on removed specials, will be lost.
 	  ;; X-Symbol conversion is useful, but a surprising nuisance
 	  ;; to achieve, mainly because x-symbol doesn't give us back
 	  ;; a useful pointer to end of region after converting, and
@@ -711,8 +712,8 @@ last use time, to discourage saving these into the users database."
 
 (defun pg-copy-span-contents (span)
   "Copy contents of SPAN to kill ring, sans surrounding whitespace."
-  (copy-region-as-kill 
-   (save-excursion 
+  (copy-region-as-kill
+   (save-excursion
      (goto-char (span-start span))
      (skip-chars-forward " \t\n")
      (point))
@@ -729,7 +730,7 @@ last use time, to discourage saving these into the users database."
 (defun pg-numth-span-higher-or-lower (span num &optional noerr)
   "Find NUM'th span after/before SPAN.  NUM is positive for after."
   (unless (and span (<= (span-end span) (proof-unprocessed-begin)))
-    (if noerr 
+    (if noerr
 	nil
       (error "No processed region under point")))
   (let ((downflag (> num 0))
@@ -771,22 +772,22 @@ If NUM is negative, move upwards.  Return new span."
       ;; We're going to move the span to before/after nextspan.
       ;; First make sure inserting there doesn't extend the span.
       (if downflag
-	  (set-span-property nextspan 'end-open t)
-	(set-span-property nextspan 'start-open t))
+	  (span-set-property nextspan 'end-open t)
+	(span-set-property nextspan 'start-open t))
       ;; When we delete the span, we want to duplicate it
       ;; to recreate in the new position.
-      (set-span-property span 'duplicable 't)
+      (span-set-property span 'duplicable 't)
       ;; FIXME: this is faulty: moving span up gives children
       ;; list with single nil element.  Hence liveness test
       (mapcar (lambda (s) (if (span-live-p s)
-			      (set-span-property s 'duplicable 't)))
+			      (span-set-property s 'duplicable 't)))
 	      (span-property span 'children))
       (let* ((start     (span-start span))
 	     (end       (span-end span))
 	     (contents  (buffer-substring start end))
 	     ;; Locked end may move up when we delete
 	     ;; region: we'll make sure to reset it
-	     ;; again later, it shouldn't change.  
+	     ;; again later, it shouldn't change.
 	     ;; NB: (rely on singlethreadedness here, so
 	     ;; lockedend doesn't move while in this code).
 	     (lockedend (span-end proof-locked-span)))
@@ -801,14 +802,14 @@ If NUM is negative, move upwards.  Return new span."
 	    ;; Let XEmacs duplicate extents as needed, then repair
 	    ;; their associations
 	    (insert contents)
-	    (let ((new-span 
+	    (let ((new-span
 		   (span-at insertpos 'type)));should be one we deleted.
-	      (set-span-property 
+	      (span-set-property
 	       new-span 'children
-	       (append 
-		(mapcar-spans 'pg-fixup-children-span 
+	       (append
+		(span-mapcar-spans 'pg-fixup-children-span
 			      insertpos (point) 'type)))
-	      (set-span-end proof-locked-span lockedend)
+	      (span-set-end proof-locked-span lockedend)
 	      (undo-boundary)
 	      new-span)))))))
 
@@ -816,14 +817,14 @@ If NUM is negative, move upwards.  Return new span."
   (if (span-property span 'controlspan)
       (progn
 	;; WARNING: dynamic binding for new-span
-	(set-span-property span 'controlspan new-span)
+	(span-set-property span 'controlspan new-span)
 	(list span))))
       
 (defun pg-move-region-down (&optional num)
   "Move the region under point downwards in the buffer, past NUM spans."
   (interactive "p")
   (let ((span  (span-at (point) 'type)))
-    (and span 
+    (and span
 	 (goto-char (span-start
 		     (pg-move-span-contents span num)))
 	 (skip-chars-forward " \t\n"))))
@@ -835,7 +836,7 @@ If NUM is negative, move upwards.  Return new span."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Dragging regions around 
+;; Dragging regions around
 ;;
 ;; FIXME: unfinished
 
@@ -845,7 +846,7 @@ If NUM is negative, move upwards.  Return new span."
 ;(defun pg-mouse-drag-move-region-function (event click-count dragp)
 ;  (save-excursion
 ;    (let* ((span (span-at (mouse-set-point event) 'type)))
-;      (if span 
+;      (if span
 ;	  (if pg-drag-region-point
 ;	      ;; Move the region at point to region here.
 	      
@@ -866,7 +867,7 @@ If NUM is negative, move upwards.  Return new span."
 		    (and (skip-chars-backward " \t\n")
 			 (> (point) (point-min))
 			 (span-at (1- (point)) 'type))))
-	 (nextspan (and span (pg-numth-span-higher-or-lower 
+	 (nextspan (and span (pg-numth-span-higher-or-lower
 			      (pg-control-span-of span) num 'noerr))))
     (cond
      ((and nextspan (> num 0))
@@ -899,9 +900,9 @@ If NUM is negative, move upwards.  Return new span."
     (let ((map (make-sparse-keymap
 		"Keymap for context-sensitive menus on spans")))
       (cond
-       (proof-running-on-XEmacs
+       ((featurep 'xemacs)
 	(define-key map [button3] 'pg-span-context-menu))
-       (proof-running-on-Emacs21
+       ((not (featurep 'xemacs))
 	(define-key map [down-mouse-3] 'pg-span-context-menu)))
       map))
 
@@ -914,11 +915,11 @@ If NUM is negative, move upwards.  Return new span."
 (defun pg-span-for-event (event)
   "Return span corresponding to position of a mouse click EVENT."
   (cond
-   (proof-running-on-XEmacs
+   ((featurep 'xemacs)
     (select-window (event-window event))
     (span-at (event-point event) 'type))
-   (proof-running-on-Emacs21
-    (with-current-buffer 
+   ((not (featurep 'xemacs))
+    (with-current-buffer
 	(window-buffer (posn-window (event-start event)))
       (span-at  (posn-point (event-start event)) 'type)))))
 
@@ -926,14 +927,14 @@ If NUM is negative, move upwards.  Return new span."
   (interactive "e")
   (let ((span (pg-span-for-event event))
 	cspan)
-    ;; Find controlling span 
+    ;; Find controlling span
     (while (setq cspan (span-property span 'controlspan))
       (setq span cspan))
-    (let*  
+    (let*
 	((idiom (and span (span-property span 'idiom)))
 	 (id    (and span (span-property span 'id))))
-      (popup-menu (pg-create-in-span-context-menu 
-		   span 
+      (popup-menu (pg-create-in-span-context-menu
+		   span
 		   (if idiom (symbol-name idiom))
 		   (if id (symbol-name id)))))))
 
@@ -957,14 +958,14 @@ If NUM is negative, move upwards.  Return new span."
   (append
    (list (pg-span-name span))
    (list (vector
-	  "Show/hide"   
-	  (if idiom (list `pg-toggle-element-visibility idiom name) 
+	  "Show/hide"
+	  (if idiom (list `pg-toggle-element-visibility idiom name)
 	    idiom)
 	  (not (not idiom))))
    (list (vector
 	  "Copy"	(list 'pg-copy-span-contents span) t))
    (list (vector
-	  "Undo"   
+	  "Undo"
 	  (list 'pg-span-undo span) t))
    (if proof-experimental-features
        (list (vector
@@ -976,7 +977,7 @@ If NUM is negative, move upwards.  Return new span."
 	      (pg-numth-span-higher-or-lower (pg-control-span-of span) 1 'noerr))))
    (if proof-script-span-context-menu-extensions
        (funcall proof-script-span-context-menu-extensions span idiom name))
-   (if (and proof-experimental-features 
+   (if (and proof-experimental-features
 	    proof-shell-theorem-dependency-list-regexp)
        (proof-dependency-in-span-context-menu span))))
 
@@ -1036,7 +1037,7 @@ If NUM is negative, move upwards.  Return new span."
   (pg-hint
    (format
     "\\[proof-prf] for goals;%s \\[proof-layout-windows] refreshes"
-    (if (not proof-multiple-frames-enable) ;; and not proof-three-window-enable? 
+    (if (not proof-multiple-frames-enable) ;; and not proof-three-window-enable
 	(format " \\[proof-display-some-buffers] rotates output%s;"
 		(if nextbuf (concat " (next:" nextbuf ")") ""))
       ""))))
@@ -1050,12 +1051,12 @@ If NUM is negative, move upwards.  Return new span."
       (let ((win (get-buffer-window proof-script-buffer)))
 	(unless ;; end of locked already displayed
 	    (and win (pos-visible-in-window-p (proof-unprocessed-begin)))
-	  (save-excursion 
+	  (save-excursion
 	    (set-buffer proof-script-buffer)
 	    (cond
 	     ((proof-locked-region-empty-p)) ;; nothing if empty
 	     ((proof-locked-region-full-p)
-	      (pg-hint 
+	      (pg-hint
 	       (concat "Processing complete in " (buffer-name proof-script-buffer))))
 	     (t ;; partly complete: hint about displaying the locked end
 	      (pg-jump-to-end-hint))))))))
@@ -1077,16 +1078,16 @@ The function `substitute-command-keys' is called on the argument."
 
 ;; FIXME: making the binding globally is perhaps a bit obnoxious, but
 ;; this modifier combination is currently unused.
-(cond 
- (proof-running-on-Emacs21
+(cond
+ ((not (featurep 'xemacs))
   (global-set-key [C-M-mouse-2] 'pg-identifier-under-mouse-query))
- (proof-running-on-XEmacs
+ ((featurep 'xemacs)
   (global-set-key '(control meta button2) 'pg-identifier-under-mouse-query)))
 
 (defun pg-identifier-under-mouse-query (event)
   (interactive "e")
   (if proof-shell-identifier-under-mouse-cmd
-      (let (identifier ctxt oldend) 
+      (let (identifier ctxt oldend)
 	(save-selected-window
 	  (save-selected-frame
 	    (save-excursion
@@ -1099,16 +1100,16 @@ The function `substitute-command-keys' is called on the argument."
 	      (setq identifier
 		    ;; If there's an active region in this buffer, use that
 		    ;; instead of the identifier under point.  Since
-		    ;; region-end moves immediately to new point with 
+		    ;; region-end moves immediately to new point with
 		    ;; zmacs-regions we use oldend instead of current.
 		    (if (region-exists-p)
-			(buffer-substring (region-beginning) 
+			(buffer-substring (region-beginning)
 					  (or oldend (region-end)))
 		     (setq identifier (current-word))))
 	      (setq ctxt (proof-buffer-syntactic-context)))))
 	(unless (or (null identifier)
 		    (string-equal identifier ""))
-	  (proof-shell-invisible-command 
+	  (proof-shell-invisible-command
 	   (if (stringp proof-shell-identifier-under-mouse-cmd)
 	       ;; simple customization
 	       (format proof-shell-identifier-under-mouse-cmd identifier)
@@ -1125,24 +1126,24 @@ The function `substitute-command-keys' is called on the argument."
 
 (eval-after-load "speedbar"
   '(and proof-assistant-symbol ;; *should* be set by now
-	(speedbar-add-supported-extension 
+	(speedbar-add-supported-extension
 	 (nth 2 (assoc proof-assistant-symbol proof-assistant-table)))))
 
 (defun proof-imenu-enable ()
   "Add or remove index menu."
   (if proof-imenu-enable
       (imenu-add-to-menubar "Index")
-    (if proof-running-on-XEmacs
+    (if (featurep 'xemacs)
 	(easy-menu-remove (list "Index" :filter 'imenu-menu-filter))
       (progn
 	(let ((oldkeymap (keymap-parent (current-local-map))))
 	  (if ;; sanity checks in case someone else set local keymap
 	      (and oldkeymap
 		   (lookup-key (current-local-map) [menu-bar index])
-		   (not 
+		   (not
 		    (lookup-key oldkeymap [menu-bar index])))
 	      (use-local-map oldkeymap)))
 	(remove-hook 'menu-bar-update-hook 'imenu-update-menubar)))))
 
 (provide 'pg-user)
-;; pg-user.el ends here.
+;;; pg-user.el ends here
diff --git a/generic/pg-xhtml.el b/generic/pg-xhtml.el
index e7e1e604..1070dfc0 100644
--- a/generic/pg-xhtml.el
+++ b/generic/pg-xhtml.el
@@ -1,6 +1,6 @@
-;; pg-xhtml.el	 XHTML goal display for Proof General
+;; pg-xhtml.el	--- XHTML goal display for Proof General
 ;;
-;; Copyright (C) 2002 LFCS Edinburgh. 
+;; Copyright (C) 2002 LFCS Edinburgh.
 ;; Author:     David Aspinall <David.Aspinall@ed.ac.uk>
 ;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -9,6 +9,13 @@
 ;; NB: THIS FILE NOT YET USED: once required by PG,
 ;; must be added to main dist by editing Makefile.devel
 
+
+;;; Commentary:
+;; 
+
+;;; Code:
+
+(require 'cl)
 (require 'pg-xml)
 
 ;;
@@ -34,7 +41,7 @@
 
 (defun pg-xhtml-next-file ()
   "Return new file name for XHTML storage."
-  (concat 
+  (concat
    (pg-xhtml-dir)
    (int-to-string  (incf pg-xhtml-file-count))
    (if proof-running-on-win32 ".htm" ".html")))
@@ -44,7 +51,7 @@
 ;; Writing an XHMTL file
 ;;
 
-(defvar pg-xhtml-header 
+(defvar pg-xhtml-header
   "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN
 http://www.w3.org/TR/xhtml11/DTD/xhtml11-strict.dtd\">\n
 <!-- This file was automatically generated by Proof General -->\n\n"
@@ -59,7 +66,7 @@ BODY should contain a sequence of pg-xml writing commands."
     (or (eq (car-safe (file-attributes dir)) 't)
 	(if (not (file-attributes dir))
 	    (make-directory (pg-xhtml-dir) t)
-	  (error "Cannot open temp dir %s (in pg-xhtml-write-tempfile)" 
+	  (error "Cannot open temp dir %s (in pg-xhtml-write-tempfile)"
 		 (pg-xhtml-dir))))
     `(with-temp-file ,file
       (pg-xml-begin-write t)
@@ -72,12 +79,12 @@ BODY should contain a sequence of pg-xml writing commands."
   "Cleanup temporary directory used for XHTML files."
   (delete-directory (pg-xhtml-dir)))
     
-(defvar pg-mozilla-prog-name 
+(defvar pg-mozilla-prog-name
   "/usr/bin/mozilla"
   "Command name of browser to use with XHTML display.")
 
 (defun pg-xhtml-display-file-mozilla (file)
-  "Display FILENAME in netscape/mozilla."
+  "Display FILE in netscape/mozilla."
   (shell-command (concat pg-mozilla-prog-name
 			 " -remote \"openURL(" file ")\"")))
 
@@ -94,4 +101,4 @@ BODY should contain a sequence of pg-xml writing commands."
 
 
 (provide 'pg-xhtml)
-;; End of pg-xhtml
+;;; pg-xhtml.el ends here
diff --git a/generic/pg-xml.el b/generic/pg-xml.el
index 0465a6a1..141508ff 100644
--- a/generic/pg-xml.el
+++ b/generic/pg-xml.el
@@ -1,6 +1,6 @@
-;; pg-xml.el	 XML functions for Proof General
+;; pg-xml.el --- XML functions for Proof General
 ;;
-;; Copyright (C) 2000-2002 LFCS Edinburgh. 
+;; Copyright (C) 2000-2002 LFCS Edinburgh.
 ;; Author:     David Aspinall <David.Aspinall@ed.ac.uk>
 ;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -11,9 +11,9 @@
 
 (require 'proof-utils) ;; for pg-internal-warning
 
-(cond 
+(cond
  ;; We want to find a good version of xml.el
- (proof-running-on-XEmacs
+ ((featurep 'xemacs)
   (require 'xml-fixed))			;; XEmacs: used PG bundled fixed version
  (t					;; Otherwise use GNU Emacs distrib version.
   (require 'xml)))
@@ -41,7 +41,7 @@
   "Parse string in ARG, same as pg-xml-parse-buffer."
   (let
       ((tempbuffer (get-buffer-create " *xml-parse*")))
-    (save-excursion 
+    (save-excursion
       (set-buffer tempbuffer)
       (delete-region (point-min) (point-max))
       (insert-string arg)
@@ -75,7 +75,7 @@ Parsing according to `xml-parse-file' of xml.el."
     (or val
 	(if optional
 	    defaultval
-	  (pg-pgip-error "pg-xml-get-attr: Didn't find required %s attribute in %s element" 
+	  (pg-pgip-error "pg-xml-get-attr: Didn't find required %s attribute in %s element"
 		 attribute (xml-node-name node))))))
 
 (defun pg-xml-child-elts (node)
@@ -88,7 +88,7 @@ Parsing according to `xml-parse-file' of xml.el."
   (let ((children (pg-xml-child-elts node)))
     (if (= (length children) 1)
 	(car children)
-      (pg-internal-warning  "pg-xml-child-elt: expected single element child of %s" 
+      (pg-internal-warning  "pg-xml-child-elt: expected single element child of %s"
 			    (xml-node-name node)))))
 
 (defun pg-xml-get-child (child node)
@@ -114,10 +114,10 @@ Parsing according to `xml-parse-file' of xml.el."
 
 (defmacro pg-xml-attr (name val) `(cons (quote ,name) ,val))
 
-(defmacro pg-xml-node (name atts children) 
+(defmacro pg-xml-node (name atts children)
   `(cons (quote ,name) (cons ,atts ,children)))
 
-(defconst pg-xml-header 
+(defconst pg-xml-header
   "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n")
 
 
@@ -126,7 +126,7 @@ Parsing according to `xml-parse-file' of xml.el."
   (let ((insertfn    (lambda (&rest args)
 		       (setq strs (cons (reduce 'concat args) strs))))
 	strs)
-    (dolist (xml xmls) 
+    (dolist (xml xmls)
       (pg-xml-output-internal xml nil insertfn))
     (reduce 'concat (reverse strs))))
 
@@ -227,4 +227,4 @@ Output with indentation INDENT-STRING (or none if nil)."
 
 
 (provide 'pg-xml)
-;; End of `pg-xml.el'
+;;; pg-xml.el ends here
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 9b734dc5..e69a7d1b 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -5,7 +5,7 @@
 
 
 ;;;### (autoloads (bufhist-exit bufhist-init) "bufhist" "../lib/bufhist.el"
-;;;;;;  (18274 23584))
+;;;;;;  (18316 9979))
 ;;; Generated autoloads from ../lib/bufhist.el
 
 (autoload (quote bufhist-init) "bufhist" "\
@@ -26,7 +26,7 @@ Minor mode retaining an in-memory history of the buffer contents.")
 
 ;;;***
 
-;;;### (autoloads (holes-mode) "holes" "../lib/holes.el" (18300 51209))
+;;;### (autoloads (holes-mode) "holes" "../lib/holes.el" (18303 18645))
 ;;; Generated autoloads from ../lib/holes.el
 
 (autoload (quote holes-mode) "holes" "\
@@ -52,8 +52,19 @@ This mode is only useful with a font which can display the maths repertoire.
 
 ;;;***
 
+;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el"
+;;;;;;  (18316 8285))
+;;; Generated autoloads from pg-goals.el
+
+(autoload (quote proof-goals-config-done) "pg-goals" "\
+Initialise the goals buffer after the child has been configured.
+
+\(fn)" nil nil)
+
+;;;***
+
 ;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet)
-;;;;;;  "pg-pgip" "pg-pgip.el" (18300 45960))
+;;;;;;  "pg-pgip" "pg-pgip.el" (18303 28393))
 ;;; Generated autoloads from pg-pgip.el
 
 (autoload (quote pg-pgip-process-packet) "pg-pgip" "\
@@ -75,10 +86,20 @@ Send an <askprefs> message to the prover.
 ;;;***
 
 ;;;### (autoloads (pg-response-has-error-location proof-next-error
-;;;;;;  pg-response-maybe-erase) "pg-response" "pg-response.el" (18301
-;;;;;;  62030))
+;;;;;;  pg-response-maybe-erase proof-response-config-done proof-response-mode)
+;;;;;;  "pg-response" "pg-response.el" (18316 44546))
 ;;; Generated autoloads from pg-response.el
 
+(autoload (quote proof-response-mode) "pg-response" "\
+Responses from Proof Assistant
+
+\(fn)" t nil)
+
+(autoload (quote proof-response-config-done) "pg-response" "\
+Complete initialisation of a response-mode derived buffer.
+
+\(fn)" nil nil)
+
 (autoload (quote pg-response-maybe-erase) "pg-response" "\
 Erase the response buffer according to pg-response-erase-flag.
 ERASE-NEXT-TIME is the new value for the flag.
@@ -98,7 +119,8 @@ Jump to location of next error reported in the response buffer.
 
 A prefix arg specifies how many error messages to move;
 negative means move back to previous error messages.
-Just C-u as a prefix means reparse the error message buffer
+
+Optional argument ARGP means reparse the error message buffer
 and start at the first error.
 
 \(fn &optional ARGP)" t nil)
@@ -112,7 +134,7 @@ See `pg-next-error-regexp'.
 ;;;***
 
 ;;;### (autoloads (pg-defthymode) "pg-thymodes" "pg-thymodes.el"
-;;;;;;  (16513 49231))
+;;;;;;  (18303 28745))
 ;;; Generated autoloads from pg-thymodes.el
 
 (autoload (quote pg-defthymode) "pg-thymodes" "\
@@ -133,7 +155,7 @@ All of these settings are optional.
 ;;;***
 
 ;;;### (autoloads (proof-define-assistant-command-witharg proof-define-assistant-command)
-;;;;;;  "pg-user" "pg-user.el" (18300 51209))
+;;;;;;  "pg-user" "pg-user.el" (18303 28857))
 ;;; Generated autoloads from pg-user.el
 
 (autoload (quote proof-define-assistant-command) "pg-user" "\
@@ -150,8 +172,8 @@ CMDVAR is a variable holding a function or string.  Automatically has history.
 
 ;;;***
 
-;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (18300
-;;;;;;  42609))
+;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (18303
+;;;;;;  28931))
 ;;; Generated autoloads from pg-xml.el
 
 (autoload (quote pg-xml-parse-string) "pg-xml" "\
@@ -180,7 +202,7 @@ Make a portion of a context-sensitive menu showing proof dependencies.
 ;;;***
 
 ;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el"
-;;;;;;  (16513 49231))
+;;;;;;  (18315 59949))
 ;;; Generated autoloads from proof-easy-config.el
 
 (autoload (quote proof-easy-config) "proof-easy-config" "\
@@ -204,7 +226,7 @@ Indent current line of proof script, if indentation enabled.
 ;;;***
 
 ;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-support-available)
-;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (18300 42609))
+;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (18316 3560))
 ;;; Generated autoloads from proof-maths-menu.el
 
 (autoload (quote proof-maths-menu-support-available) "proof-maths-menu" "\
@@ -225,7 +247,7 @@ in future if we have just activated it for this buffer.
 
 ;;;### (autoloads (defpacustom proof-defpacustom-fn proof-aux-menu
 ;;;;;;  proof-menu-define-specific proof-menu-define-main proof-menu-define-keys)
-;;;;;;  "proof-menu" "proof-menu.el" (18301 63081))
+;;;;;;  "proof-menu" "proof-menu.el" (18316 43683))
 ;;; Generated autoloads from proof-menu.el
 
 (autoload (quote proof-menu-define-keys) "proof-menu" "\
@@ -268,7 +290,7 @@ evaluate can be provided instead.
 ;;;***
 
 ;;;### (autoloads (proof-mmm-enable proof-mmm-support-available)
-;;;;;;  "proof-mmm" "proof-mmm.el" (18274 49936))
+;;;;;;  "proof-mmm" "proof-mmm.el" (18316 3588))
 ;;; Generated autoloads from proof-mmm.el
 
 (autoload (quote proof-mmm-support-available) "proof-mmm" "\
@@ -287,10 +309,29 @@ in future if we have just activated it for this buffer.
 
 ;;;***
 
-;;;### (autoloads (proof-shell-invisible-command proof-shell-wait
-;;;;;;  proof-extend-queue proof-start-queue proof-shell-available-p
-;;;;;;  proof-shell-live-buffer proof-shell-ready-prover) "proof-shell"
-;;;;;;  "proof-shell.el" (18301 64250))
+;;;### (autoloads (proof-config-done proof-mode) "proof-script" "proof-script.el"
+;;;;;;  (18316 9094))
+;;; Generated autoloads from proof-script.el
+
+(autoload (quote proof-mode) "proof-script" "\
+Proof General major mode class for proof scripts.
+\\{proof-mode-map}
+
+\(fn)" t nil)
+
+(autoload (quote proof-config-done) "proof-script" "\
+Finish setup of Proof General scripting mode.
+Call this function in the derived mode for the proof assistant to
+finish setup which depends on specific proof assistant configuration.
+
+\(fn)" nil nil)
+
+;;;***
+
+;;;### (autoloads (proof-shell-config-done proof-shell-mode proof-shell-invisible-command
+;;;;;;  proof-shell-wait proof-extend-queue proof-start-queue proof-shell-insert
+;;;;;;  proof-shell-available-p proof-shell-live-buffer proof-shell-ready-prover)
+;;;;;;  "proof-shell" "proof-shell.el" (18316 3097))
 ;;; Generated autoloads from proof-shell.el
 
 (autoload (quote proof-shell-ready-prover) "proof-shell" "\
@@ -313,6 +354,21 @@ No error messages.  Useful as menu or toolbar enabler.
 
 \(fn)" nil nil)
 
+(autoload (quote proof-shell-insert) "proof-shell" "\
+Insert STRING at the end of the proof shell, call `comint-send-input'.
+
+First call `proof-shell-insert-hook'.  The argument ACTION may be
+examined by the hook to determine how to process the STRING variable.
+
+Then strip STRING of carriage returns before inserting it and updating
+`proof-marker' to point to the end of the newly inserted text.
+
+Do not use this function directly, or output will be lost.  It is only
+used in `proof-append-alist' when we start processing a queue, and in
+`proof-shell-exec-loop', to process the next item.
+
+\(fn STRING ACTION)" nil nil)
+
 (autoload (quote proof-start-queue) "proof-shell" "\
 Begin processing a queue of commands in ALIST.
 If START is non-nil, START and END are buffer positions in the
@@ -354,10 +410,22 @@ In case CMD is (or yields) nil, do nothing.
 
 \(fn CMD &optional WAIT)" nil nil)
 
+(autoload (quote proof-shell-mode) "proof-shell" "\
+Proof General shell mode class for proof assistant processes
+
+\(fn)" t nil)
+
+(autoload (quote proof-shell-config-done) "proof-shell" "\
+Initialise the specific prover after the child has been configured.
+Every derived shell mode should call this function at the end of
+processing.
+
+\(fn)" nil nil)
+
 ;;;***
 
 ;;;### (autoloads (proof-splash-message proof-splash-display-screen)
-;;;;;;  "proof-splash" "proof-splash.el" (18301 63625))
+;;;;;;  "proof-splash" "proof-splash.el" (18316 43933))
 ;;; Generated autoloads from proof-splash.el
 
 (autoload (quote proof-splash-display-screen) "proof-splash" "\
@@ -389,7 +457,7 @@ may be a string or sexp evaluated to get a string.
 ;;;***
 
 ;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup)
-;;;;;;  "proof-toolbar" "proof-toolbar.el" (18299 42505))
+;;;;;;  "proof-toolbar" "proof-toolbar.el" (18316 44362))
 ;;; Generated autoloads from proof-toolbar.el
 
 (autoload (quote proof-toolbar-setup) "proof-toolbar" "\
@@ -409,7 +477,7 @@ Menu made from the Proof General toolbar commands.
 
 ;;;### (autoloads (proof-x-symbol-config-output-buffer proof-x-symbol-shell-config
 ;;;;;;  proof-x-symbol-enable proof-x-symbol-support-maybe-available)
-;;;;;;  "proof-x-symbol" "proof-x-symbol.el" (18300 45870))
+;;;;;;  "proof-x-symbol" "proof-x-symbol.el" (18316 43316))
 ;;; Generated autoloads from proof-x-symbol.el
 
 (autoload (quote proof-x-symbol-support-maybe-available) "proof-x-symbol" "\
@@ -442,12 +510,14 @@ Configure the current output buffer (goals/response/trace) for X-Symbol.
 ;;;***
 
 ;;;### (autoloads nil nil ("../lib/holes-load.el" "../lib/local-vars-list.el"
-;;;;;;  "../lib/proof-compat.el" "../lib/span-extent.el" "../lib/span-overlay.el"
-;;;;;;  "../lib/span.el" "../lib/unichars.el" "../lib/xml-fixed.el"
-;;;;;;  "../lib/xmlunicode.el" "pg-assoc.el" "pg-autotest.el" "pg-goals.el"
-;;;;;;  "pg-metadata.el" "pg-pbrpm.el" "pg-pgip-old.el" "pg-xhtml.el"
-;;;;;;  "proof-config.el" "proof-script.el" "proof-site.el" "proof-utils.el"
-;;;;;;  "proof.el" "test-compile.el") (18302 3569 810785))
+;;;;;;  "../lib/pg-dev.el" "../lib/proof-compat.el" "../lib/span-extent.el"
+;;;;;;  "../lib/span-overlay.el" "../lib/span.el" "../lib/unichars.el"
+;;;;;;  "../lib/xml-fixed.el" "../lib/xmlunicode.el" "pg-assoc.el"
+;;;;;;  "pg-autotest.el" "pg-custom.el" "pg-metadata.el" "pg-pbrpm.el"
+;;;;;;  "pg-pgip-old.el" "pg-vars.el" "pg-xhtml.el" "proof-config.el"
+;;;;;;  "proof-site.el" "proof-vars.el" "proof.el" "test-compile.el"
+;;;;;;  "test-mac.el" "test-mac2.el" "test-req.el" "test-req2.el")
+;;;;;;  (18316 44551 721111))
 
 ;;;***
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index d9177015..40d1da52 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1,6 +1,6 @@
 ;;; proof-config.el --- Proof General configuration for proof assistant
 ;;
-;; Copyright (C) 1998-2004 LFCS Edinburgh.
+;; Copyright (C) 1998-2008 LFCS Edinburgh.
 ;; Author:      David Aspinall <David.Aspinall@ed.ac.uk> and others
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -8,6 +8,8 @@
 ;;
 ;; $Id$
 ;;
+;;; Commentary:
+;; 
 ;; This file declares all user options and prover-specific
 ;; configuration variables for Proof General.  The variables
 ;; are used variously by the proof script mode and the
@@ -28,10 +30,8 @@
 ;;     5b. regexps
 ;;     5c. hooks and others
 ;;  6. Goals buffer configuration
-;;  [ 7. Splash screen settings  -- moved to proof-splash.el now ]
-;;  8. X-Symbol support
-;;  9. Prover specific settings
-;; 10. Global constants
+;;  7. X-Symbol support
+;;  8. Global constants
 ;;
 ;; The user options don't need to be set on a per-prover basis,
 ;; and the global constants probably should not be touched.
@@ -55,25 +55,25 @@
 ;;      proof-x-symbol	     :     settings for X-Symbol (8)
 ;;    <Prover name>-config   :  Specific internal settings for a prover
 ;;
-;; ==================================================
+;; ======================================================================
 ;;
 ;; Developers notes:
+;;
 ;;   i. When adding a new configuration variable, please
 ;;       (a) put it in the right customize group, and
-;;       (b) add a magical comment in NewDoc.texi to document it!
+;;       (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
-;;	properly.
+;;    	: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
 ;;
-;; ==================================================
-;; 
+;;
+;; ======================================================================
 
-(require 'proof-utils)			;; Macros used below
+;;; Code:
 
-
 ;;
 ;; 1. User options for proof mode
 ;;
@@ -82,12 +82,47 @@
 ;; *not* normally be touched by prover specific code.
 ;;
 
-;;; Code:
+
+
 (defgroup proof-user-options nil
   "User options for Proof General."
   :group 'proof-general
   :prefix "proof-")
 
+;;
+;; Function for taking action when dynamically adjusting customize
+;; values
+;;
+(defun proof-set-value (sym value)
+  "Set a customize variable using set-default and a function.
+We first call `set-default' to set SYM to VALUE.
+Then if there is a function SYM (i.e. with the same name as the
+variable SYM), it is called to take some dynamic action for the new
+setting.
+
+If there is no function SYM, we try stripping
+proof-assistant-symbol and adding \"proof-\" instead to get
+a function name.  This extends proof-set-value to work with
+generic individual settings.
+
+The dynamic action call only happens when values *change*: as an
+approximation we test whether proof-config is fully-loaded yet."
+  (set-default sym value)
+  (if (featurep 'proof-config)
+      (if (fboundp sym)
+	  (funcall sym)
+	(if (boundp 'proof-assistant-symbol)
+	    (if (> (length (symbol-name sym))
+		   (+ 3 (length (symbol-name proof-assistant-symbol))))
+		(let ((generic
+		       (intern
+			(concat "proof"
+				(substring (symbol-name sym)
+					   (length (symbol-name
+						    proof-assistant-symbol)))))))
+		  (if (fboundp generic)
+		      (funcall generic))))))))
+
 (defcustom proof-electric-terminator-enable nil
   "*If non-nil, use electric terminator mode.
 If electric terminator mode is enabled, pressing a terminator will
@@ -112,30 +147,6 @@ terminator somewhere nearby.  Electric!"
   :set 'proof-set-value
   :group 'proof-user-options)
 
-(defpgcustom x-symbol-enable nil
-  "*Whether to use x-symbol in Proof General for this assistant.
-If you activate this variable, whether or not you really get x-symbol
-support depends on whether your proof assistant supports it and
-whether X-Symbol is installed in your Emacs."
-  :type 'boolean
-  :set 'proof-set-value
-  :group 'proof-user-options)
-
-(defpgcustom maths-menu-enable nil
-  "*Non-nil for Unicode maths menu in Proof General for this assistant."
-  :type 'boolean
-  :set 'proof-set-value
-  :group 'proof-user-options)
-
-(defpgcustom mmm-enable nil
-  "*Whether to use MMM Mode in Proof General for this assistant.
-MMM Mode allows multiple modes to be used in the same buffer.
-If you activate this variable, whether or not you really get MMM
-support depends on whether your proof assistant supports it."
-  :type 'boolean
-  :set 'proof-set-value
-  :group 'proof-user-options)
-
 (defcustom pg-show-hints t
   "*Whether to display keyboard hints in the minibuffer."
   :type 'boolean
@@ -230,26 +241,11 @@ goals and response windows to fit their contents."
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-toolbar-use-button-enablers
-  (not
-   (or
-    ;; Disabled by default for win32 and solaris
-    proof-running-on-win32
-    (and (boundp 'system-configuration)
-	 (string-match "sun-solaris" system-configuration))))
+(defcustom proof-toolbar-use-button-enablers t
   "*If non-nil, toolbars buttons may be enabled/disabled automatically.
 Toolbar buttons can be automatically enabled/disabled according to
 the context.  Set this variable to nil if you don't like this feature
-or if you find it unreliable.
-
-Notes:
-* Toolbar enablers are only available with XEmacs 21 and later.
-* With this variable nil, buttons do nothing when they would
-otherwise be disabled.
-* If you change this variable it will only be noticed when you
-next start Proof General.
-* The default value for XEmacs built for solaris is nil, because
-of unreliabilities with enablers there."
+or if you find it unreliable."
   :type 'boolean
   :group 'proof-user-options)
 
@@ -269,12 +265,9 @@ files which are out of date with respect to the loaded buffers!"
   :type 'boolean
   :group 'proof-user-options)
 
-(defpgcustom script-indent t
-  "*If non-nil, enable indentation code for proof scripts."
-  :type 'boolean
-  :group 'proof-user-options)
 
-;; FIXME: implement it!  Use in indentation code.
+
+;; TODO: implement this!  Use in indentation code.
 (defcustom proof-one-command-per-line
   nil
   "*If non-nil, format for newlines after each proof command in a script.
@@ -333,7 +326,7 @@ This is only useful for PG developers."
 (defcustom proof-experimental-features
   ;; Turn on experimental features for pre-releases.
   ;; (if (string-match "pre" proof-general-version) t)
-  t  ;; Version 3.5: features classed as experimental have
+  t  ;; Version 3.7: features classed as experimental have
      ;; actually been tested for a while, so we enable them.
   "*Whether to enable certain features regarded as experimental.
 Proof General includes a few features designated as \"experimental\".
@@ -366,14 +359,12 @@ If you choose 'ignore, you can find the end of the locked using
 	  (const :tag "Never move" ignore))
   :group 'proof-user-options)
 
-;; TODO: the auto action might be improved a bit: for example,
-;; when scripting is turned off because another buffer is
-;; being retracted, we almost certainly want to retract
-;; the currently edited buffer as well (use case is somebody
-;; realising a change has to made in an ancestor file).
-;; In that case as well (supposing file being unlocked is
-;; an ancestore), it also seems unlikely that we need
-;; to query for saves.
+;; Note: the auto action might be improved a bit: for example, when
+;; scripting is turned off because another buffer is being retracted,
+;; we almost certainly want to retract the currently edited buffer as
+;; well (use case is somebody realising a change has to made in an
+;; ancestor file).  And in that case (supposing file being unlocked is
+;; an ancestor), it seems unlikely that we need to query for saves.
 (defcustom proof-auto-action-when-deactivating-scripting nil
   "*If 'retract or 'process, do that when deactivating scripting.
 
@@ -453,6 +444,34 @@ signals to the remote host."
   :group 'proof-general
   :prefix "proof-")
   
+(defconst pg-defface-window-systems 
+  '(x            ;; bog standard
+    mswindows    ;; Windows
+    gtk          ;; gtk emacs (obsolete?)
+    mac          ;; used by Aquamacs
+    carbon       ;; used by Carbon XEmacs
+    ns           ;; NeXTstep Emacs (Emacs.app)
+    x-toolkit)   ;; possible catch all (but probably not)
+  "A list of possible values for `window-system'.
+If you are on a window system and your value of `window-system' is
+not listed here, you may not get the correct syntax colouring behaviour.")
+
+(defmacro proof-face-specs (bl bd ow)
+  "Return a spec for `defface' with BL for light bg, BD for dark, OW o/w."
+  `(append
+    (apply 'append
+     (mapcar
+     (lambda (ty) (list
+		     (list (list (list 'type ty) '(class color)
+			   (list 'background 'light))
+			   (quote ,bl))
+		     (list (list (list 'type ty) '(class color)
+				 (list 'background 'dark))
+			   (quote ,bd))))
+     ;; NOTE: see proof-compat.el for possible window-system values
+     pg-defface-window-systems))
+    (list (list t (quote ,ow)))))
+
 (defface proof-queue-face
   (proof-face-specs
    (:background "mistyrose") ;; was "darksalmon" in PG 3.4,3.5
@@ -483,14 +502,6 @@ signals to the remote host."
 Exactly what uses this face depends on the proof assistant."
   :group 'proof-faces)
 
-;; FIXME da: are these defconsts still needed now we use defface?
-;; Answer: yes, for GNU Emacs they are.
-
-(defconst proof-declaration-name-face 'proof-declaration-name-face
-  "Expression that evaluates to a face.
-Required so that 'proof-declaration-name-face is a proper facename in
-both XEmacs 20.4 and Emacs 20.2's version of font-lock.")
-
 (defface proof-tacticals-name-face
   (proof-face-specs
    (:foreground "MediumOrchid3")
@@ -500,11 +511,6 @@ both XEmacs 20.4 and Emacs 20.2's version of font-lock.")
 Exactly what uses this face depends on the proof assistant."
   :group 'proof-faces)
 
-(defconst proof-tacticals-name-face 'proof-tacticals-name-face
-  "Expression that evaluates to a face.
-Required so that 'proof-tacticals-name-face is a proper facename in
-both XEmacs 20.4 and Emacs 20.3's version of font-lock.")
-
 (defface proof-tactics-name-face
   (proof-face-specs
    (:foreground "darkblue")
@@ -514,11 +520,6 @@ both XEmacs 20.4 and Emacs 20.3's version of font-lock.")
 Exactly what uses this face depends on the proof assistant."
   :group 'proof-faces)
 
-(defconst proof-tactics-name-face 'proof-tactics-name-face
-  "Expression that evaluates to a face.
-Required so that 'proof-tactics-name-face is a proper facename in
-both XEmacs 20.4 and Emacs 20.3's version of font-lock.")
-
 (defface proof-error-face
   (proof-face-specs
    (:background "indianred1" :bold t)
@@ -536,8 +537,6 @@ both XEmacs 20.4 and Emacs 20.3's version of font-lock.")
 Warning messages can come from proof assistant or from Proof General itself."
   :group 'proof-faces)
 
-(defconst proof-warning-face 'proof-warning-face)
-
 (defface proof-eager-annotation-face
   (proof-face-specs
    (:background "palegoldenrod")
@@ -595,6 +594,23 @@ Warning messages can come from proof assistant or from Proof General itself."
   :group 'proof-faces)
 
 
+;;; Compatibility: these are required for use in GNU Emacs/font-lock-keywords
+(defconst proof-face-compat-doc "Evaluates to a face name, for compatibility.")
+(defconst proof-queue-face 'proof-queue-face proof-face-compat-doc)
+(defconst proof-locked-face 'proof-locked-face proof-face-compat-doc)
+(defconst proof-declaration-name-face 'proof-declaration-name-face proof-face-compat-doc)
+(defconst proof-tacticals-name-face 'proof-tacticals-name-face proof-face-compat-doc)
+(defconst proof-tactics-name-face 'proof-tactics-name-face proof-face-compat-doc)
+(defconst proof-error-face 'proof-error-face proof-face-compat-doc)
+(defconst proof-warning-face 'proof-warning-face proof-face-compat-doc)
+(defconst proof-eager-annotation-face 'proof-eager-annotation-face proof-face-compat-doc)
+(defconst proof-debug-message-face 'proof-debug-message-face proof-face-compat-doc)
+(defconst proof-boring-face 'proof-boring-face proof-face-compat-doc)
+(defconst proof-mouse-highlight-face 'proof-mouse-highlight-face proof-face-compat-doc)
+(defconst proof-highlight-dependent-face 'proof-highlight-dependent-face proof-face-compat-doc)
+(defconst proof-highlight-dependency-face 'proof-highlight-dependency-face proof-face-compat-doc)
+(defconst proof-active-area-face 'proof-active-area-face proof-face-compat-doc)
+
 
 
 ;;
@@ -632,42 +648,18 @@ Warning messages can come from proof assistant or from Proof General itself."
 ;;
 ;; 2. Major modes used by Proof General.
 ;;
-;; The first three settings are used when starting a shell,
-;; so the must be set before a shell is started, so we
-;; know what modes are needed for each of the buffers.
-;; Hence the use of pre-shell-start-hook.
-
-(defcustom proof-mode-for-shell 'proof-shell-mode
-  "Mode for proof shell buffers.
-Usually customised for specific prover.
-Suggestion: this can be set a function called by `proof-pre-shell-start-hook'."
-  :type 'function
-  :group 'prover-config)
-
-(defcustom proof-mode-for-response 'proof-response-mode
-  "Mode for proof response buffer (and trace buffer, if used).
-Usually customised for specific prover.
-Suggestion: this can be set a function called by `proof-pre-shell-start-hook'."
-  :type 'function
-  :group 'prover-config)
-
-(defcustom proof-mode-for-goals 'proof-goals-mode
-  "Mode for proof state display buffers.
-Usually customised for specific prover.
-Suggestion: this can be set a function called by `proof-pre-shell-start-hook'."
-  :type 'function
-  :group 'prover-config)
+;; PG 3.7: the variables setting the major modes have been removed.
+;; They now default to standard names:
+;;
+;; proof-mode-for-shell:    <PA>-shell-mode
+;; proof-mode-for-response  <PA>-response-mode
+;; proof-mode-for-goals:    <PA>-goals-mode
+;; proof-mode-for-script:   <PA>-mode
+;;
+;; These are defined as constants in pg-custom.el
+;;
+;; Prover modes should define aliases for these if not defun'd.
 
-(defcustom proof-mode-for-script 'proof-mode
-  "Mode for proof script buffers.
-This is used by Proof General to find out which buffers
-contain proof scripts.
-The regular name for this is <PA>-mode.  If you use any of the
-convenience macros Proof General provides for defining commands
-etc, then you should stick to this name.
-Suggestion: this can be set in the script mode configuration."
-  :type 'function
-  :group 'prover-config)
 
 (defcustom proof-guess-command-line nil
   "Function to guess command line for proof assistant, given a filename.
@@ -730,58 +722,6 @@ If a function, it should return the command string to insert."
   :type '(choice string function)
   :group 'prover-config)
 
-(defconst proof-toolbar-entries-default
-  `((state	"Display Proof State" "Display the current proof state" t
-				      proof-showproof-command)
-    (context	"Display Context"     "Display the current context" t
-				      proof-context-command)
-;; PG 3.7: disable goal & qed, they're not so useful (& save-command never enabled).
-;;     (goal	"Start a New Proof"   "Start a new proof" t
-;;  				      proof-goal-command)
-    (retract	"Retract Buffer"      "Retract (undo) whole buffer" t)
-    (undo	"Undo Step"           "Undo the previous proof command" t)
-    (delete	"Delete Step"         nil t)
-    (next	"Next Step"           "Process the next proof command" t)
-    (use	"Use Buffer"  	      "Process whole buffer" t)
-    (goto	"Goto Point"	      "Process or undo to the cursor position" t)
-;;     (qed	"Finish Proof"        "Close/save proved theorem" t
-;; 				      proof-save-command)
-    (lockedend  "Goto Locked End"     nil t)
-    (find	"Find Theorems"	      "Find theorems" t proof-find-theorems-command)
-    (command    "Issue Command"	      "Issue a non-scripting command" t)
-    (interrupt  "Interrupt Prover"    "Interrupt the proof assistant" t)
-    (restart	"Restart Scripting"   "Restart scripting (clear all locked regions)" t)
-    (visibility "Toggle Visibility"   nil t)
-; PG 3.6: remove Info item from toolbar; it's not very useful and under PA->Help anyway
-;    (info	nil		      "Show online proof assistant information" t
-;				       proof-info-command)
-; PG 3.7: use Info icon for info
-    (info	nil		      "Proof General manual" t))
-"Example value for proof-toolbar-entries.  Also used to define scripting menu.
-This gives a bare toolbar that works for any prover, providing the
-appropriate configuration variables are set.
-To add/remove prover specific buttons, adjust the `<PA>-toolbar-entries'
-variable, and follow the pattern in `proof-toolbar.el' for
-defining functions, images.")
-
-(defpgcustom toolbar-entries proof-toolbar-entries-default
-  "List of entries for Proof General toolbar and Scripting menu.
-Format of each entry is (TOKEN MENUNAME TOOLTIP DYNAMIC-ENABLER-P ENABLE).
-
-For each TOKEN, we expect an icon with base filename TOKEN,
-a function proof-toolbar-<TOKEN>, and (optionally) a dynamic enabler
-proof-toolbar-<TOKEN>-enable-p.
-
-If ENABLEP is absent, item is enabled; if ENABLEP is present, item
-is only added to menubar and toolbar if ENABLEP is non-null.
-
-If MENUNAME is nil, item will not appear on the scripting menu.
-
-If TOOLTIP is nil, item will not appear on the toolbar.
-
-The default value is `proof-toolbar-entries-default' which contains
-the standard Proof General buttons.")
-
 (defcustom proof-assistant-true-value "true"
   "String for true values in proof assistant, used for setting flags.
 Default is the string \"true\"."
@@ -836,7 +776,7 @@ conversion, etc.  (No changes are done if nil)."
   :prefix "proof-")
 
 (defcustom proof-terminal-char nil
-  "Character which terminates every command sent to proof assistant.  nil if none.
+  "Character that terminates commands sent to prover; nil if none.
 
 To configure command recognition properly, you must set at least one
 of these: `proof-script-sexp-commands', `proof-script-command-end-regexp',
@@ -846,7 +786,7 @@ or `proof-script-parse-function'."
   :group 'prover-config)
 
 (defcustom proof-script-sexp-commands nil
-  "Non-nil if proof script has a LISP-like syntax, and commands are top-level sexps.
+  "Non-nil if script has LISP-like syntax: commands are top-level sexps.
 You should set this variable in script mode configuration.
 
 To configure command recognition properly, you must set at least one
@@ -913,9 +853,7 @@ initial ``goal'' and the final ``save'' command."
   :group 'prover-config)
 
 (defcustom proof-script-fly-past-comments nil
-  "*If non-nil, fly past successive comments when scripting, coalescing into single spans.
-The default setting for this before PG 3.5 was t, now it is nil.  If you
-prefered the old behaviour, customize this variable to t."
+  "*If non-nil, fly past successive comments, coalescing into single spans."
   :type 'boolean
   :group 'proof-user-options)
 
@@ -1019,12 +957,11 @@ It's safe to leave this setting as nil."
   :group 'proof-script)
 
 (defcustom proof-save-with-hole-result 2
-  "String or Int: how to build the theorem name after matching
-with proof-save-with-hole-regexp. If it is an int N use match-string
-to recover the value of the Nth parenthesis matched. If it is a string
-use replace-match. It the later case, proof-save-with-hole-regexp should
-match the entire command"
-
+  "How to build theorem name after matching with `proof-save-with-hole-regexp'.
+String or Int. 
+If an int N use match-string to recover the value of the Nth parenthesis matched. 
+If it is a string use replace-match. In this case, proof-save-with-hole-regexp 
+should match the entire command"
   :type '(choice string int)
   :group 'proof-script)
 
@@ -1051,12 +988,11 @@ It's safe to leave this setting as nil."
   :group 'proof-script)
 
 (defcustom proof-goal-with-hole-result 2
-  "String or Int: how to build the theorem name after matching
-with proof-goal-with-hole-regexp. If it is an int N use match-string
-to recover the value of the Nth parenthesis matched. If it is a string
-use replace-match. It the later case, proof-goal-with-hole-regexp should
-match the entire command"
-
+  "How to build theorem name after matching with `proof-goal-with-hole-regexp'.
+String or Int. 
+If an int N use match-string to recover the value of the Nth parenthesis matched. 
+If it is a string use replace-match. In this case, proof-save-with-hole-regexp 
+should match the entire command"
   :type '(choice string int)
   :group 'proof-script)
 
@@ -1289,7 +1225,7 @@ you only need to set if you use that function (by not customizing
   :group 'proof-script)
 
 (defcustom pg-topterm-goalhyplit-fn nil
-  "Function which returns cons cell if point is at a goal/hypothesis/literal command.
+  "Function to return cons if point is at a goal/hypothesis/literal.
 This is used to parse the proofstate output to mark it up for
 proof-by-pointing or literal command insertion.  It should return a cons or nil.
 First element of the cons is a symbol, 'goal', 'hyp' or 'lit'.
@@ -1495,9 +1431,6 @@ See pg-user.el: pg-create-in-span-context-menu for more hints."
 (defcustom proof-prog-name nil
   "System command to run the proof assistant in the proof shell.
 May contain arguments separated by spaces, but see also `proof-prog-args'.
-Suggestion: this can be set in proof-pre-shell-start-hook from a variable
-which is in the proof assistant's customization group.  This allows
-different proof assistants to coexist \(albeit in separate Emacs sessions).
 
 Remark: if `proof-prog-args' is non-nil, then proof-prog-name is considered
 strictly: it must contain *only* the program name with no option, spaces
@@ -1505,27 +1438,6 @@ are interpreted literally as part of the program name."
   :type 'string
   :group 'proof-shell)
 
-(defpgcustom prog-args nil
-  "Arguments to be passed to `proof-prog-name' to run the proof assistant.
-If non-nil, will be treated as a list of arguments for`proof-prog-name'.
-Otherwise `proof-prog-name' will be split on spaces to form arguments.
-
-Remark: Arguments are interpreted strictly: each one must contain only one
-word, with no space (unless it is the same word). For example if the
-arguments are -x foo -y bar, then the list should be '(\"-x\" \"foo\"
-\"-y\" \"bar\"), notice that '(\"-x foo\" \"-y bar\") is *wrong*"
-
-  :type '(list string)
-  :group 'proof-shell)
-
-(defpgcustom prog-env nil
-  "Modifications to `process-environment' made before running `proof-prog-name'.
-Each element should be a string of the form ENVVARNAME=VALUE.  They will be
-added to the environment before launching the prover (but not pervasively).
-For example for coq on Windows you might need something like:
-(setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
-  :type '(list string)
-  :group 'proof-shell)
 
 (defcustom proof-shell-auto-terminate-commands t
   "Non-nil if Proof General should try to add terminator to every command.
@@ -1714,7 +1626,7 @@ on information from the prover."
   :group 'proof-shell)
 
 (defcustom proof-done-advancing-require-function nil
-  "Invoked from `proof-done-advancing', see `proof-shell-require-command-regexp'.
+  "Used in `proof-done-advancing', see `proof-shell-require-command-regexp'.
 The function is passed the span and the command as arguments."
   :type 'function
   :group 'proof-shell)
@@ -1954,7 +1866,7 @@ The default value is \"\\n\" to match up to the end of the line."
 
 At the moment, this setting is not used in the generic Proof General.
 
-In the future it will be used for a generic implementation for `pg-topterm-goalhyplit-fn',
+Future use may providea generic implementation for `pg-topterm-goalhyplit-fn',
 used to help parse the goals buffer to annotate it for proof by pointing."
   :type '(choice regexp (const :tag "Unset" nil))
   :group 'proof-shell)
@@ -2138,9 +2050,7 @@ response buffer.
 This is intended for unusual debugging output from
 the prover, rather than ordinary output from final proofs.
 
-Set to nil to disable.
-
-Suggestion: this can be set a function called by `proof-pre-shell-start-hook'."
+Set to nil to disable."
   :type '(choice nil regexp)
   :group 'proof-shell)
 
@@ -2160,8 +2070,8 @@ response buffer."
 
 (defcustom proof-shell-unicode t
   ;; true by default for PG 3.7; set to nil for old systems
-  "Tell whether communication between Proof General and the prover
-process is 8bit clean, without using any special non-ASCII characters.
+  "Whether communication between PG and prover is 8bit clean.
+If non-nil, no special non-ASCII characters must be used in markup.
 If so, the process coding system will be set to UTF-8."
   :type 'boolean
   :group 'proof-shell)
@@ -2266,22 +2176,6 @@ into tokens for the proof assistant."
   :type '(repeat function)
   :group 'proof-shell)
 
-(defcustom proof-pre-shell-start-hook nil
-  "Hooks run before proof shell is started.
-Suggestion: set this to a function which configures just these proof
-shell variables:
-
-   proof-prog-name
-   proof-mode-for-shell
-   proof-mode-for-response
-   proof-mode-for-goals
-   proof-shell-trace-output-regexp
-
-This is the bare minimum needed to get a shell buffer and
-its friends configured in the function proof-shell-start."
-  :type '(repeat function)
-  :group 'proof-shell)
-
 (defcustom proof-shell-handle-delayed-output-hook
   '(proof-pbp-focus-on-first-goal)
   "Hooks run after new output has been displayed in goals or response buffer."
@@ -2440,7 +2334,7 @@ the end of the concrete syntax is indicated by pg-subterm-end-char.
 
 If `pg-subterm-start-char' is nil, subterm markup is disabled.
 
-See doc of `pg-goals-analyse-structure' for more details of
+See doc of `pg-assoc-analyse-structure' for more details of
 subterm and proof-by-pointing markup mechanisms.."
   :type '(choice character (const nil))
   :group 'proof-goals)
@@ -2517,7 +2411,7 @@ the current restriction, and must return the final value of (point-max).
 
 
 ;;
-;; 8. X-Symbol configuration
+;; 7. X-Symbol configuration (see also `pg-custom.el')
 ;;
 
 (defgroup proof-x-symbol nil
@@ -2562,60 +2456,13 @@ X-Symbol support is deactivated."
 
 
 
-
-;;
-;; 9. Prover specific settings
-;;
-;; The settings defined here automatically use the current proof
-;; assistant symbol as a prefix, i.e.  isa-favourites, coq-favourites,
-;; or whatever will be defined on evaluation.
-
-(defpgcustom favourites nil
-  "*Favourite commands for this proof assistant.
-A list of lists of the form (COMMAND INSCRIPT MENUNAME KEY),
-arguments for `proof-add-favourite', which see.")
-
-(defpgcustom menu-entries nil
-  "Extra entries for proof assistant specific menu.
-A list of menu items [NAME CALLBACK ENABLER ...].  See the documentation
-of `easy-menu-define' for more details."
-  :type 'sexp
-  :group 'prover-config)
-
-(defpgcustom help-menu-entries nil
-  "Extra entries for help submenu for proof assistant specific help menu.
-A list of menu items [NAME CALLBACK ENABLER ...].  See the documentation
-of `easy-menu-define' for more details."
-  :type 'sexp
-  :group 'prover-config)
-
-(defpgcustom keymap (make-keymap (concat proof-assistant " keymap"))
-  "Proof assistant specific keymap, used under prefix C-c a."
-  :type 'sexp
-  :group 'prover-config)
-
-(defpgcustom completion-table nil
-  "List of identifiers to use for completion for this proof assistant.
-Completion is activated with \\[complete].
-
-If this table is empty or needs adjusting, please make changes using
-`customize-variable' and post suggestions at
-http://proofgeneral.inf.ed.ac.uk/trac"
-  :type '(list string)
-  :group 'prover-config)
-
-;; FIXME: not used yet.
-(defpgcustom tags-program nil
-  "Program to run to generate TAGS table for proof assistant."
-  :type 'file
-  :group 'prover-config)
-
 		     
 
 
 
 ;;
-;; 10. Global constants
+;; 8. Global constants
+;;
 
 (defcustom proof-general-name "Proof-General"
   "Proof General name used internally and in menu titles."
@@ -2636,7 +2483,7 @@ http://proofgeneral.inf.ed.ac.uk/trac"
 
 (defcustom proof-universal-keys
   (cons
-   (if proof-running-on-XEmacs
+   (if (featurep 'xemacs)
        '([(control c) \`] . proof-next-error)
      '("`" . proof-next-error))
    '(([(control c) (control c)]  . proof-interrupt-process)
@@ -2664,9 +2511,5 @@ where `k' is a key binding (vector) and `f' the designated function."
 
 
 
-;; End of proof-config.el
 (provide 'proof-config)
-
-(provide 'proof-config)
-
 ;;; proof-config.el ends here
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 7532a92e..0f1c4eff 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -73,7 +73,7 @@ This is done using `proof-depends-module-name-for-buffer' and
 Called from `proof-done-advancing' when a save is processed and
 proof-last-theorem-dependencies is set."
 
-  (set-span-property gspan 'dependencies
+  (span-set-property gspan 'dependencies
 		     ;; Ancestors of NAME are in the second component.
 		     ;; FIXME: for now we ignore the first component:
 		     ;; NAME may not be enough [Isar allows proof regions
@@ -89,7 +89,7 @@ proof-last-theorem-dependencies is set."
 	 ;; and return resulting list paired up with names.
 	 (depspans    
 	  (apply 'append
-		 (mapcar-spans 
+		 (span-mapcar-spans 
 		  (lambda (depspan)
 		    (let ((dname (span-property depspan 'name)))
 		      (if (and
@@ -97,7 +97,7 @@ proof-last-theorem-dependencies is set."
 			   (member dname samefilenames))
 			  (let ((forwarddeps 
 				 (span-property depspan 'dependents)))
-			    (set-span-property depspan 'dependents
+			    (span-set-property depspan 'dependents
 					       (cons
 						(list name gspan) forwarddeps))
 			    ;; return list of args for menu fun: name and span
@@ -106,7 +106,7 @@ proof-last-theorem-dependencies is set."
 		  (span-start gspan)
 		  'type))))
     
-    (set-span-property gspan 'dependencies-within-file depspans)
+    (span-set-property gspan 'dependencies-within-file depspans)
     (setq proof-last-theorem-dependencies nil)))
 
 
@@ -146,7 +146,7 @@ proof-last-theorem-dependencies is set."
 
 (defun proof-dep-alldeps-menu (span)
   (or (span-property span 'dependencies-menu) ;; cached value
-      (set-span-property span 'dependencies-menu
+      (span-set-property span 'dependencies-menu
 			 (proof-dep-make-alldeps-menu 
 			  (span-property span 'dependencies)))))
 
@@ -229,21 +229,21 @@ This is simply to display the dependency somehow."
   (let ((helpmsg  (concat "This item is a dependency (ancestor) of " name)))
     (while nmspans
       (let ((span (cadar nmspans)))
-	(set-span-property span 'face 'proof-highlight-dependency-face)
-	(set-span-property span 'priority pg-dep-span-priority)
-	(set-span-property span 'mouse-highlight nil)
-	(set-span-property span 'help-echo helpmsg))
+	(span-set-property span 'face 'proof-highlight-dependency-face)
+	(span-set-property span 'priority pg-dep-span-priority)
+	(span-set-property span 'mouse-highlight nil)
+	(span-set-property span 'help-echo helpmsg))
       (setq nmspans (cdr nmspans)))))
 
 (defun proof-highlight-depts (name nmspans)
   (let ((helpmsg  (concat "This item depends on (is a child of) " name)))
     (while nmspans
       (let ((span (cadar nmspans)))
-	(set-span-property span 'face 'proof-highlight-dependent-face)
-	(set-span-property span 'priority pg-dep-span-priority)
-	(set-span-property span 'mouse-highlight nil)
-	(set-span-property span 'help-echo helpmsg)
-	(set-span-property span 'balloon-help helpmsg))
+	(span-set-property span 'face 'proof-highlight-dependent-face)
+	(span-set-property span 'priority pg-dep-span-priority)
+	(span-set-property span 'mouse-highlight nil)
+	(span-set-property span 'help-echo helpmsg)
+	(span-set-property span 'balloon-help helpmsg))
       (setq nmspans (cdr nmspans)))))
 
 (defun proof-dep-unhighlight ()
@@ -255,8 +255,8 @@ This is simply to display the dependency somehow."
     (let ((span (span-at (point-min) 'type)))
       (while span
 	(pg-set-span-helphighlights span 'nohighlight)
-	(set-span-property span 'face 'proof-locked-face)
-	(set-span-property span 'priority pg-ordinary-span-priority)
+	(span-set-property span 'face 'proof-locked-face)
+	(span-set-property span 'priority pg-ordinary-span-priority)
 	(setq span (next-span span 'type))))))
 
 
diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el
index cbc450d9..c93cb641 100644
--- a/generic/proof-easy-config.el
+++ b/generic/proof-easy-config.el
@@ -10,7 +10,6 @@
 ;; interface with customization mechanism so a new prover can be
 ;; configured by editing inside custom buffers.
 ;;
-(require 'proof)
 
 (defconst proof-easy-config-derived-modes-table
   '((""         "script"     proof-mode (proof-config-done))
@@ -30,7 +29,6 @@
 	   (hyphen    (if (string-equal prefixsym "") "" "-"))
 	   (mode      (intern (concat modert hyphen "mode")))
 	   (modename  (concat proof-assistant " " suffixnm))
-	   (varname   (intern (concat "proof-mode-for-" suffixnm)))
 	   ;; FIXME: declare these variables in proof-config:
 	   ;;	proof-{goals,resp,trace}-font-lock-keywords,
 	   ;;   proof-{goals,resp,trace}-syntax-table-entries
@@ -51,10 +49,7 @@
 				      (setq syn (cddr syn))))))
 		       body)))
       (eval
-       `(define-derived-mode ,mode ,parent ,modename nil ,@fullbody))
-      ;; Set proof-mode-for-script and friends
-      ;; NB: top-level, so we don't need proof-pre-shell-start-hook.
-      (set varname mode))))
+       `(define-derived-mode ,mode ,parent ,modename nil ,@fullbody)))))
 
 (defun proof-easy-config-check-setup (sym name)
   "A number of simple checks."
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index c0109c03..df5014cf 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -6,10 +6,6 @@
 ;; $Id$
 ;;
 
-(require 'proof)                        ; loader
-(require 'proof-script)                 ; indent code is for script editing
-
-
 (defun proof-indent-indent ()
   "Determine indentation caused by syntax element at current point."
   (cond
diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el
index 99e46bf2..726668cc 100644
--- a/generic/proof-maths-menu.el
+++ b/generic/proof-maths-menu.el
@@ -18,21 +18,21 @@
 ;; starting Emacs, with (require 'maths-menu).
 ;;
 
-(require 'proof-utils)
+(eval-when-compile
+  (require 'proof-utils)) ; proof-ass, proof-eval-when-ready-for-assistant
+
 
 ;;;###autoload
 (defun proof-maths-menu-support-available ()
   "A test to see whether maths-menu support is available."
   (and
-   (not proof-running-on-XEmacs) ;; not XEmacs compatible
+   (not (featurep 'xemacs)) ;; not XEmacs compatible
    (or (featurep 'maths-menu)
        ;; *should* always succeed unless bundled version broken
        (proof-try-require 'maths-menu))
    ;; Load any optional prover-specific config in <foo>-maths-menu.el
    (or (proof-try-require (proof-ass-sym maths-menu)) t)))
 
-(eval-when-compile
-  (proof-maths-menu-support-available))
 
 (defun proof-maths-menu-set-global (flag)
   "Set global status of maths-menu mode for PG buffers to be FLAG.
@@ -61,10 +61,10 @@ in future if we have just activated it for this buffer."
 ;;
 ;; On start up, adjust automode according to user setting
 ;;
-(if (and (proof-ass maths-menu-enable) 
-	 (proof-maths-menu-support-available))
-    (proof-maths-menu-set-global t))
-
+(proof-eval-when-ready-for-assistant 
+    (if (and (proof-ass maths-menu-enable) 
+	     (proof-maths-menu-support-available))
+	(proof-maths-menu-set-global t)))
 
 (provide 'proof-maths-menu)
 ;; End of proof-maths-menu.el
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 696b55da..b562d31a 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -7,11 +7,9 @@
 ;; $Id$
 ;;
 
-(require 'proof)
-(require 'proof-syntax)
-(require 'proof-toolbar)     ; needed for proof-toolbar-scripting-menu
-
-(require 'proof-maths-menu)  ; for automatic invocation from saved option
+(require 'pg-user)         ; user commands used here
+(require 'proof-utils)     ; proof-deftoggle, proof-eval-when-ready-for-assistant
+(require 'proof-autoloads) ; 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
@@ -80,55 +78,57 @@ without adjusting window layout."
 
 ;;;###autoload
 (defun proof-menu-define-keys (map)
-;; M-a and M-e are usually {forward,backward}-sentence.
-;; Some modes also override these with similar commands
-(define-key map [(meta a)] 'proof-backward-command)
-(define-key map [(meta e)] 'proof-forward-command)
-(define-key map [(meta up)] 'proof-backward-command)
-(define-key map [(meta down)] 'proof-forward-command)
-(define-key map [(control meta a)] 'proof-goto-command-start)
-(define-key map [(control meta e)] 'proof-goto-command-end)
-(define-key map [(control c) (control a)] (proof-ass keymap))
-(define-key map [(control c) (control b)] 'proof-process-buffer)
-;; C-c C-c is proof-interrupt-process in universal-keys
-;; C-c C-f is proof-find-theorems in universal-keys
-(define-key map [(control c) (control h)] 'proof-help)
-;; C-c C-l is proof-layout-windows in universal-keys
-;; C-c C-n is proof-assert-next-command-interactive in universal-keys
-;; C-c C-o is proof-display-some-buffers in universal-keys
-(define-key map [(control c) (control p)] 'proof-prf)
-(define-key map [(control c) (control r)] 'proof-retract-buffer)
-(define-key map [(control c) (control s)] 'proof-toggle-active-scripting)
-(define-key map [(control c) (control t)] 'proof-ctxt)
-;; 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)] '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);; FIXME: FSF??
-(cond ((string-match "XEmacs" emacs-version)
-(define-key map [(control button3)]	  'proof-mouse-goto-point)
-(define-key map [(control button1)]	  'proof-mouse-track-insert)) ; no FSF
-      (t 
-(define-key map [(control mouse-3)]	  'proof-mouse-goto-point)))
- ; FSF
-;; NB: next binding overwrites comint-find-source-code.  
-;; FIXME: not implemented yet 
-;; (define-key map [(meta p)]		  'proof-previous-matching-command)
-;; (define-key map [(meta n)]		  'proof-next-matching-command)
-;; Standard binding for completion
-(define-key map [(control return)] 'proof-script-complete)
-(define-key map [(control c) (control ?\;)] 'pg-insert-last-output-as-comment)
-;;
-;; Experimental: span moving functions
-(if proof-experimental-features (progn
-      (define-key map [(control meta up)] 'pg-move-region-up)
-      (define-key map [(control meta down)] 'pg-move-region-down)))
-;; Add the universal keys bound in all PG buffers.
-;; C-c ` is next-error in universal-keys
-(proof-define-keys map proof-universal-keys))
+  (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.
+  ;; Some modes also override these with similar commands
+  (define-key map [(meta a)] 'proof-backward-command)
+  (define-key map [(meta e)] 'proof-forward-command)
+  (define-key map [(meta up)] 'proof-backward-command)
+  (define-key map [(meta down)] 'proof-forward-command)
+  (define-key map [(control meta a)] 'proof-goto-command-start)
+  (define-key map [(control meta e)] 'proof-goto-command-end)
+  (define-key map [(control c) (control b)] 'proof-process-buffer)
+  ;; C-c C-c is proof-interrupt-process in universal-keys
+  ;; C-c C-f is proof-find-theorems in universal-keys
+  (define-key map [(control c) (control h)] 'proof-help)
+  ;; C-c C-l is proof-layout-windows in universal-keys
+  ;; C-c C-n is proof-assert-next-command-interactive in universal-keys
+  ;; C-c C-o is proof-display-some-buffers in universal-keys
+  (define-key map [(control c) (control p)] 'proof-prf)
+  (define-key map [(control c) (control r)] 'proof-retract-buffer)
+  (define-key map [(control c) (control s)] 'proof-toggle-active-scripting)
+  (define-key map [(control c) (control t)] 'proof-ctxt)
+  ;; 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)] 
+    '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);; FIXME: Emacs binding?
+  (cond ((featurep 'xemacs)
+	 (define-key map [(control button3)] 'proof-mouse-goto-point)
+	 (define-key map [(control button1)] 'proof-mouse-track-insert)) ; no Emacs binding
+	(t 
+	 (define-key map [(control mouse-3)] 'proof-mouse-goto-point)))
+  ;; NB: next binding overwrites comint-find-source-code.  
+  ;; TODO: not implemented yet 
+  ;; (define-key map [(meta p)] 'proof-previous-matching-command)
+  ;; (define-key map [(meta n)] 'proof-next-matching-command)
+  ;; Standard binding for completion
+  (define-key map [(control return)] 'proof-script-complete)
+  (define-key map [(control c) (control ?\;)] 'pg-insert-last-output-as-comment)
+  ;;
+  ;; Experimental: span moving functions
+  (if proof-experimental-features 
+      (progn
+	(define-key map [(control meta up)] 'pg-move-region-up)
+	(define-key map [(control meta down)] 'pg-move-region-down)))
+  ;; Add the universal keys bound in all PG buffers.
+  ;; NB: C-c ` is next-error in universal-keys
+  (proof-define-keys map proof-universal-keys))
 
 
 
@@ -145,7 +145,7 @@ without adjusting window layout."
    proof-mode-menu  
    proof-mode-map
    "The main Proof General menu"
-   proof-main-menu))
+   (proof-main-menu)))
 
 ;; The proof assistant specific menu
 
@@ -154,42 +154,44 @@ without adjusting window layout."
   (easy-menu-define 
     proof-assistant-menu 
     proof-mode-map
-    `(concat "The menu for " proof-assistant)
+    (concat "The menu for " proof-assistant)
     (cons proof-assistant
-	    (append
-	     (proof-ass menu-entries)
-	     '("----")
-	     (or proof-menu-favourites
-		 (proof-menu-define-favourites-menu))
-	     (or proof-menu-settings
-		 (proof-menu-define-settings-menu))
-	     '("----")
-	    (list
-	     (vector
-	      (concat "Start " proof-assistant)
-	      'proof-shell-start
-	      ':active '(not (proof-shell-live-buffer)))
+	  (append
+	   (proof-ass menu-entries)
+	   '("----")
+	   (or proof-menu-favourites
+	       (proof-menu-define-favourites-menu))
+	   (or proof-menu-settings
+	       (proof-menu-define-settings-menu))
+	   '("----")
+	   (list
+	    (vector
+	     (concat "Start " proof-assistant)
+	     'proof-shell-start
+	     ':active '(not (proof-shell-live-buffer)))
 	    (vector
 	     (concat "Exit " proof-assistant)
 	     'proof-shell-exit
 	     ':active '(proof-shell-live-buffer)))
-	    '("----")
-	    (list
-	     (cons "Help"
-		   (append
-		    `([,(concat proof-assistant " information")
-		        (proof-help)
-		       ,menuvisiblep proof-info-command]
-		      [,(concat proof-assistant " web page")
-		        (browse-url proof-assistant-home-page)
-		       ,menuvisiblep proof-assistant-home-page])
-		    (proof-ass help-menu-entries))))))))
+	   '("----")
+	   (list
+	    (cons "Help"
+		  (append
+		   (list
+		    (vector
+		     (concat proof-assistant " information")
+		     'proof-help
+		     menuvisiblep proof-info-command)
+		    (vector
+		     (concat proof-assistant " web page")
+		     '(browse-url proof-assistant-home-page)
+		     menuvisiblep proof-assistant-home-page))
+		   (proof-ass help-menu-entries))))))))
 
 (defun proof-assistant-menu-update ()
   "Update proof assistant menu in scripting buffers."
   (proof-map-buffers (proof-buffers-in-mode proof-mode-for-script)
-    ;; NB: behaviour of easy-menu-remove here is odd in XEmacs, it
-    ;; considerably changes the mode popup menu.  
+    ;; NB: easy-menu-remove is odd in XEmacs, it considerably changes the mode popup menu.  
     ;; In GNU Emacs this first instruction does nothing.
     (easy-menu-remove proof-assistant-menu)
     (proof-menu-define-settings-menu)
@@ -269,11 +271,14 @@ without adjusting window layout."
 (proof-deftoggle proof-strict-read-only)
 
 (proof-deftoggle-fn 'proof-imenu-enable 'proof-imenu-toggle)
-(proof-deftoggle-fn (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle)
-(proof-deftoggle-fn (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle)
-(proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle)
 (proof-deftoggle proof-keep-response-history)
 
+(proof-eval-when-ready-for-assistant
+  (proof-deftoggle-fn (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle)
+  (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-keep-response-history ()
   "Enable associated buffer histories following `proof-keep-response-history'."
   (if proof-keep-response-history
@@ -360,7 +365,7 @@ without adjusting window layout."
       ;; non-Emacs users.  Cf. Gnome usability studies: menus saying
       ;; "Web Browser" more useful to novices than menus saying "Mozilla"!!
       ["Multiple Windows" proof-multiple-frames-toggle
-       :active (pg-window-system)
+       :active (and window-system t)
        :style toggle
        :selected proof-multiple-frames-enable]
       ["Delete Empty Panes" proof-delete-empty-windows-toggle
@@ -495,23 +500,24 @@ without adjusting window layout."
   "The Proof General generic menu for scripting buffers.")
 
 
-(defvar proof-main-menu
+(defun proof-main-menu ()
+  "Construct and return PG main menu used in scripting buffers."
   (cons proof-general-name
 	(append
-	 proof-toolbar-scripting-menu
+	 (proof-toolbar-scripting-menu)
 	 proof-menu
 	 proof-config-menu
 	 (list proof-advanced-menu)
-	 (list proof-help-menu)))
-  "PG main menu used in scripting buffers.")
+	 (list proof-help-menu))))
 
-(defvar proof-aux-menu
+;;;###autoload
+(defun proof-aux-menu ()
+  "Construct and return PG auxiliary menu used in non-scripting buffers."
   (cons proof-general-name 
 	(append
-	 proof-toolbar-scripting-menu
+	 (proof-toolbar-scripting-menu)
 	 proof-config-menu
-	 (list proof-help-menu)))
-  "PG auxiliary menu used in non-scripting buffers.")
+	 (list proof-help-menu))))
 
 
 
@@ -544,44 +550,6 @@ without adjusting window layout."
   
 ;;; Define stuff from favourites
 
-;;;###autoload
-(defmacro proof-defshortcut (fn string &optional key)
-  "Define shortcut function FN to insert STRING, optional keydef KEY.
-This is intended for defining proof assistant specific functions.
-STRING is inserted using `proof-insert', which see.
-KEY is added onto proof-assistant map."
-  `(progn
-     (if ,key
-	 (define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
-     (defun ,fn ()
-       ,(concat "Shortcut command to insert " 
-		(replace-in-string  string "\\\\" "\\\\=") ;; for substitute-command-keys
-		" into the current buffer.\nThis simply calls `proof-insert', which see.")
-       (interactive)
-       (proof-insert ,string))))
-
-;;;###autoload
-(defmacro proof-definvisible (fn string &optional key)
-  "Define function FN to send STRING to proof assistant, optional keydef KEY.
-This is intended for defining proof assistant specific functions.
-STRING is sent using proof-shell-invisible-command, which see.
-STRING may be a string or a function which returns a string.
-KEY is added onto proof-assistant map."
-  `(progn
-     (if ,key
-	 (define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
-     (defun ,fn ()
-       ,(concat "Command to send " 
-		(if (stringp string)
-		    (replace-in-string  
-		     string "\\\\" "\\\\=") ;; for substitute-command-keys
-		  "an instruction")
-		" to the proof assistant.")
-       (interactive)
-       ,(if (stringp string)
-	    (list 'proof-shell-invisible-command string)
-	  (list 'proof-shell-invisible-command (eval string))))))
-
 (defun proof-def-favourite (command inscript menuname &optional key new)
   "Define and a \"favourite\" proof assisant function.
 See doc of `proof-add-favourite' for first four arguments.
@@ -768,7 +736,6 @@ the form of the menu entry for the setting.")
   (interactive)
   (apply 'pg-custom-reset-vars (proof-settings-vars)))
 
-
 ;;; autoload for compiled version: used in macro proof-defpacustom
 ;;;###autoload
 (defun proof-defpacustom-fn (name val args)
@@ -856,6 +823,10 @@ The customization variable is automatically in group `proof-assistant-setting'.
 The function `proof-assistant-format' is used to format VAL.
 If NAME corresponds instead to a PG internal setting, then a form :eval to
 evaluate can be provided instead."
+  (eval-when-compile
+    (if (boundp 'proof-assistant-symbol)
+	;; declare variable to compiler to prevent warnings
+	(eval `(defvar ,(proof-ass-sym name) nil "Dummy for compilation."))))
   `(proof-defpacustom-fn (quote ,name) (quote ,val) (quote ,args)))
 
 (defun proof-assistant-invisible-command-ifposs (cmd)
diff --git a/generic/proof-mmm.el b/generic/proof-mmm.el
index 932af431..e2d9559d 100644
--- a/generic/proof-mmm.el
+++ b/generic/proof-mmm.el
@@ -21,7 +21,10 @@
 ;; Configuration for the prover is expected to reside in <foo>-mmm.el
 ;; It should define an MMM submode class called <foo>.
 
-(require 'proof-utils)
+(eval-when-compile
+  (require 'proof-utils)) ; for proof-ass, proof-eval-when-ready-for-assistant
+
+(require 'proof-site)
 
 ;;;###autoload
 (defun proof-mmm-support-available ()
@@ -39,8 +42,6 @@
    ;; Load prover-specific config in <foo>-mmm.el
    (proof-try-require (proof-ass-sym mmm))))
 
-(eval-when-compile
-  (proof-mmm-support-available))
 
 ;; The following function is called by the menu item for
 ;; MMM-Mode.  It is an attempt at an intuitive behaviour
@@ -83,10 +84,10 @@ in future if we have just activated it for this buffer."
 ;;
 ;; On start up, adjust automode according to user setting
 ;;
-(if (and (proof-ass mmm-enable) 
-	 (proof-mmm-support-available))
-    (proof-mmm-set-global t))
-
+(proof-eval-when-ready-for-assistant 
+    (if (and (proof-ass mmm-enable) 
+	     (proof-mmm-support-available))
+        (proof-mmm-set-global t)))
 
 (provide 'proof-mmm)
 ;; End of proof-mmm.el
diff --git a/generic/proof-script.el b/generic/proof-script.el
index c5f6f57b..1f056116 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -11,23 +11,15 @@
 
 ;;; Code:
 
+(eval-when-compile 
+  (require 'proof-utils))		; for macros
+
+(require 'cl)				; various
 (require 'proof)			; loader
-(require 'proof-syntax)			; utils for manipulating syntax
+(require 'proof-syntax)		        ; utils for manipulating syntax
 (require 'span)				; abstraction of overlays/extents
 (require 'pg-user)			; user-level commands
 (require 'proof-menu)			; menus for script mode
-(require 'proof-x-symbol)		; x-symbol (maybe initialize)
-(require 'proof-mmm)			; mmm (maybe put on automode list)
-
-
-;; Nuke some byte-compiler warnings
-;; NB: eval-when (compile) is different to eval-when-compile!!
-
-(eval-when (compile)
-  (proof-try-require 'func-menu)
-  (require 'comint))
-
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -95,7 +87,7 @@ This uses and updates `proof-element-counters'."
 ;;
 ;; Configuration of function-menu (aka "fume")
 ;;
-;; FIXME: we would like this code only enabled if the user loads
+;; Ideally we would like this code only enabled if the user loads
 ;; func-menu into Emacs.
 ;;
 
@@ -225,23 +217,23 @@ scripting buffer may have an active queue span.")
    
 (defsubst proof-set-queue-endpoints (start end)
   "Set the queue span to be START, END."
-  (set-span-endpoints proof-queue-span start end))
+  (span-set-endpoints proof-queue-span start end))
 
 (defsubst proof-set-locked-endpoints (start end)
   "Set the locked span to be START, END."
-  (set-span-endpoints proof-locked-span start end))
+  (span-set-endpoints proof-locked-span start end))
 
 (defsubst proof-detach-queue ()
   "Remove the span for the queue region."
-  (and proof-queue-span (detach-span proof-queue-span)))
+  (and proof-queue-span (span-detach proof-queue-span)))
 
 (defsubst proof-detach-locked ()
   "Remove the span for the locked region."
-  (and proof-locked-span (detach-span proof-locked-span)))
+  (and proof-locked-span (span-detach proof-locked-span)))
 
 (defsubst proof-set-queue-start (start)
   "Set the queue span to begin at START."
-  (set-span-start proof-queue-span start))
+  (span-set-start proof-queue-span start))
 
 (defsubst proof-set-locked-end (end)
   "Set the end of the locked region to be END.
@@ -250,7 +242,7 @@ Otherwise set the locked region to be from (point-min) to END."
   (if (>= (point-min) end)
       ;; Detach the queue span, otherwise there can be a read-only character at the end.
       (proof-detach-locked)
-    (set-span-endpoints
+    (span-set-endpoints
      proof-locked-span
      (point-min)
      (min (point-max) end) ;; safety: sometimes called with end>point-max(?)
@@ -263,7 +255,7 @@ Otherwise set the locked region to be from (point-min) to END."
   (if (or (>= (point-min) end)
 	  (<= end (span-start proof-queue-span)))
       (proof-detach-queue)
-    (set-span-end proof-queue-span end)))
+    (span-set-end proof-queue-span end)))
 
 
 ;; ** Initialise spans for a buffer
@@ -275,24 +267,24 @@ buffer, so the regions are made empty by this function.
 Also clear list of script portions."
   ;; Initialise queue span, remove it from buffer.
   (unless proof-queue-span
-      (setq proof-queue-span (make-span 1 1))
+      (setq proof-queue-span (span-make 1 1))
       ;; FIXME: span-raise is an GNU hack to make locked span appear.
       ;; overlays still don't work as well as they did/should pre 99.
       (span-raise proof-queue-span))
-  (set-span-property proof-queue-span 'start-closed t)
-  (set-span-property proof-queue-span 'end-open t)
+  (span-set-property proof-queue-span 'start-closed t)
+  (span-set-property proof-queue-span 'end-open t)
   (proof-span-read-only proof-queue-span 'always)
-  (set-span-property proof-queue-span 'face 'proof-queue-face)
-  (detach-span proof-queue-span)
+  (span-set-property proof-queue-span 'face 'proof-queue-face)
+  (span-detach proof-queue-span)
   ;; Initialise locked span, remove it from buffer
   (unless proof-locked-span
-      (setq proof-locked-span (make-span 1 1))
+      (setq proof-locked-span (span-make 1 1))
       (span-raise proof-locked-span))
-  (set-span-property proof-locked-span 'start-closed t)
-  (set-span-property proof-locked-span 'end-open t)
+  (span-set-property proof-locked-span 'start-closed t)
+  (span-set-property proof-locked-span 'end-open t)
   (proof-span-read-only proof-locked-span)
-  (set-span-property proof-locked-span 'face 'proof-locked-face)
-  (detach-span proof-locked-span)
+  (span-set-property proof-locked-span 'face 'proof-locked-face)
+  (span-detach proof-locked-span)
   (setq proof-last-theorem-dependencies nil)
   (setq proof-element-counters nil)
   (pg-clear-script-portions))
@@ -312,8 +304,8 @@ will deactivated."
 	   (with-current-buffer buffer
 	     (if proof-active-buffer-fake-minor-mode
 		 (setq proof-active-buffer-fake-minor-mode nil))
-	     (delete-spans (point-min) (point-max) 'type)  ;; remove top-level spans
-	     (delete-spans (point-min) (point-max) 'idiom) ;; and embedded spans
+	     (span-delete-spans (point-min) (point-max) 'type)  ;; remove top-level spans
+	     (span-delete-spans (point-min) (point-max) 'idiom) ;; and embedded spans
 	     (setq pg-script-portions nil)		   ;; also the record of them
 	     (proof-detach-queue)	                   ;; remove queue and locked
 	     (proof-detach-locked)
@@ -344,7 +336,7 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}."
 	(proof-detach-queue)
 	;; FIXME da: point-max seems a bit excessive here,
 	;; proof-queue-or-locked-end should be enough.
-	(delete-spans (proof-locked-end) (point-max) 'type))))
+	(span-delete-spans (proof-locked-end) (point-max) 'type))))
 
 
 
@@ -569,17 +561,17 @@ NAME does not need to be unique."
       (setq pg-script-portions (cons (cons idiomsym (list idsym))
 				     pg-script-portions)))
     ;; Idiom and ID are stored in the span as symbols; name as a string.
-    (set-span-property span 'idiom idiomsym)
-    (set-span-property span 'id idsym)
-    (set-span-property span 'name name)
-    (set-span-property span 'span-delete-action delfn)
-    (set-span-property span 'invisible visname)
+    (span-set-property span 'idiom idiomsym)
+    (span-set-property span 'id idsym)
+    (span-set-property span 'name name)
+    (span-set-property span 'span-delete-action delfn)
+    (span-set-property span 'invisible visname)
     ;; Bad behaviour if span gets copied: unique ID shouldn't be duplicated.
-    (set-span-property span 'duplicable nil) ;; NB: not supported in Emacs
+    (span-set-property span 'duplicable nil) ;; NB: not supported in Emacs
     ;; Nice behaviour in with isearch: open invisible regions temporarily.
-    (set-span-property span 'isearch-open-invisible
+    (span-set-property span 'isearch-open-invisible
 		       'pg-open-invisible-span)
-    (set-span-property span 'isearch-open-invisible-temporary
+    (span-set-property span 'isearch-open-invisible-temporary
 		       'pg-open-invisible-span)))
 
 (defun pg-open-invisible-span (span &optional invisible)
@@ -621,7 +613,7 @@ NAME does not need to be unique."
 
 (defun pg-redisplay-for-gnuemacs ()
   "GNU Emacs requires redisplay for changes in buffer-invisibility-spec."
-  (if proof-running-on-Emacs21
+  (if (not (featurep 'xemacs))
       ;; GNU Emacs requires redisplay here to see result
       ;; (sit-for 0) not enough
       (redraw-frame (selected-frame))))
@@ -659,10 +651,10 @@ NAME does not need to be unique."
   (let ((proofid   (proof-next-element-id 'proof)))
     (pg-add-element "proof"  proofid span name)
     ;; Set id in controlspan
-    (set-span-property controlspan 'id (intern proofid))
+    (span-set-property controlspan 'id (intern proofid))
     ;; Make a navigable link between the two spans.
-    (set-span-property span 'controlspan controlspan)
-    (set-span-property controlspan 'children
+    (span-set-property span 'controlspan controlspan)
+    (span-set-property controlspan 'children
 		       (cons span (span-property controlspan 'children)))
     (pg-set-span-helphighlights span 'nohighlight)
     (if proof-disappearing-proofs
@@ -692,9 +684,9 @@ NAME does not need to be unique."
 (defun pg-set-span-helphighlights (span &optional nohighlight)
   "Set the help echo message, default highlight, and keymap for SPAN."
   (let ((helpmsg (concat (pg-span-name span) ""))) ;;   " region"
-    (set-span-property span 'balloon-help helpmsg)
+    (span-set-property span 'balloon-help helpmsg)
     (if pg-show-hints ;; only message in minibuf if hints on
-	(set-span-property
+	(span-set-property
 	 span 'help-echo
 	 (substitute-command-keys
 	  (concat
@@ -703,9 +695,9 @@ NAME does not need to be unique."
 	   (if (span-property span 'idiom)
 	       "with point in region, \\[pg-toggle-visibility] to show/hide; ")
 	   "\\[popup-mode-menu] for menu)"))))
-    (set-span-property span 'keymap pg-span-context-menu-keymap)
+    (span-set-property span 'keymap pg-span-context-menu-keymap)
     (unless nohighlight
-      (set-span-property span 'mouse-face 'proof-mouse-highlight-face))))
+      (span-set-property span 'mouse-face 'proof-mouse-highlight-face))))
 
 
 
@@ -735,7 +727,7 @@ to allow other files loaded by proof assistants to be marked read-only."
     (set-buffer buffer)
     (save-excursion ;; prevent point moving if user viewing file
       (if (< (proof-unprocessed-begin) (proof-script-end))
-	(let ((span (make-span (proof-unprocessed-begin)
+	(let ((span (span-make (proof-unprocessed-begin)
 			       (proof-script-end)))
 	      dummycmd)
 	  ;; Reset queue and locked regions.
@@ -743,10 +735,10 @@ to allow other files loaded by proof assistants to be marked read-only."
 	  ;; End of locked region is always end of buffer
 	  (proof-set-locked-end (proof-script-end))
 	  ;; Configure the overlay span
-	  (set-span-property span 'type 'proverproc)
+	  (span-set-property span 'type 'proverproc)
 	  ;; A dummy command for retraction which examines it
 	  ;; FIXME: shouldn't be necessary really
-	  (set-span-property span 'dummycmd "")
+	  (span-set-property span 'dummycmd "")
 	  (pg-set-span-helphighlights span 'nohighlight))))))
 
 
@@ -1361,14 +1353,14 @@ With ARG, turn on scripting iff ARG is positive."
   ;; start/end of comments, rather than comment-start and
   ;; comment-end skip (which assumes comments are nicely formatted).
   ;; 
-  (let ((bodyspan  (make-span
+  (let ((bodyspan  (span-make
 		    (+ (length comment-start) (span-start span))
 		    (- (span-end span) 
 		       (max 1 (length comment-end)))))
 	(id        (proof-next-element-id 'comment)))
     (pg-add-element "comment" id bodyspan)
-    (set-span-property span 'id (intern id))
-    (set-span-property span 'idiom 'comment)
+    (span-set-property span 'id (intern id))
+    (span-set-property span 'idiom 'comment)
     (pg-set-span-helphighlights span)))
 
 
@@ -1415,7 +1407,7 @@ With ARG, turn on scripting iff ARG is positive."
     (setq nestedundos 0)
     (while (and gspan (> lev 0))
       (setq next (prev-span gspan 'type))
-      (delete-span gspan)
+      (span-delete gspan)
       (setq gspan next)
       (if gspan
 	  (progn
@@ -1467,16 +1459,16 @@ With ARG, turn on scripting iff ARG is positive."
 
 (defun proof-make-goalsave (gspan goalend savestart saveend nam &optional nestedundos)
   "Make new goal-save span, using GSPAN. Subroutine of `proof-done-advancing-save'."
-  (set-span-end gspan saveend)
-  (set-span-property gspan 'type 'goalsave)
-  (set-span-property gspan 'idiom 'proof);; links to nested proof element
-  (set-span-property gspan 'name nam)
-  (and nestedundos (set-span-property gspan 'nestedundos nestedundos))
+  (span-set-end gspan saveend)
+  (span-set-property gspan 'type 'goalsave)
+  (span-set-property gspan 'idiom 'proof);; links to nested proof element
+  (span-set-property gspan 'name nam)
+  (and nestedundos (span-set-property gspan 'nestedundos nestedundos))
   (pg-set-span-helphighlights gspan)
   ;; Now make a nested span covering the purported body of the
   ;; proof, and add to buffer-local list of elements.
   (let ((proofbodyspan
-	 (make-span goalend (if proof-script-integral-proofs
+	 (span-make goalend (if proof-script-integral-proofs
 				saveend savestart))))
     (pg-add-proof-element nam proofbodyspan gspan)))
   
@@ -1549,7 +1541,7 @@ With ARG, turn on scripting iff ARG is positive."
       ;; start of the buffer, we make a fake goal-save region.
 
       ;; Delete spans between the previous goal and new command
-      (mapcar 'delete-span dels)
+      (mapcar 'span-delete dels)
 
       ;; Try to set the name from the goal... [as above]
       (setq nam (or (proof-get-name-from-goal gspan)
@@ -1968,16 +1960,16 @@ Set the callback to CALLBACK-FN or 'proof-done-advancing by default."
   (let ((ct (proof-queue-or-locked-end)) span alist semi)
     (while (not (null semis))
       (setq semi (car semis)
-            span (make-span ct (nth 2 semi))
+            span (span-make ct (nth 2 semi))
 	    ct (nth 2 semi))
       (if (eq (car (car semis)) 'cmd)
 	  (progn
-	    (set-span-property span 'type 'vanilla)
-	    (set-span-property span 'cmd (nth 1 semi))
+	    (span-set-property span 'type 'vanilla)
+	    (span-set-property span 'cmd (nth 1 semi))
 	    (setq alist (cons (list span (nth 1 semi)
 				    (or callback-fn 'proof-done-advancing))
 			      alist)))
-	(set-span-property span 'type 'comment)
+	(span-set-property span 'type 'comment)
 	(setq alist (cons (list span proof-no-command 'proof-done-advancing)
 			  alist)))
 	(setq semis (cdr semis)))
@@ -2204,9 +2196,9 @@ appropriate."
     (proof-goto-end-of-locked)
     (insert "\n") ;; could be user opt 
     (insert cmd)
-    (setq span (make-span (proof-locked-end) (point)))
-    (set-span-property span 'type 'pbp)
-    (set-span-property span 'cmd cmd)
+    (setq span (span-make (proof-locked-end) (point)))
+    (span-set-property span 'type 'pbp)
+    (span-set-property span 'cmd cmd)
     (proof-start-queue (proof-unprocessed-begin) (point)
 		       (list (list span cmd 'proof-done-advancing)))))
 
@@ -2250,9 +2242,9 @@ others)."
 	(unless (proof-locked-region-empty-p)
 	  (proof-set-locked-end start)
 	  (proof-set-queue-end start))
-	(delete-spans start end 'type)
-	(delete-spans start end 'idiom)
-	(delete-span span)
+	(span-delete-spans start end 'type)
+	(span-delete-spans start end 'idiom)
+	(span-delete span)
 	(if kill (kill-region start end))))
   ;; State of scripting may have changed now
   (run-hooks 'proof-state-change-hook))
@@ -2262,8 +2254,8 @@ others)."
 Returns retraction action destined for proof shell queue, and make span.
 Action holds PROOF-COMMAND and `proof-done-retracting' callback.
 Span deletion property set to flag DELETE-REGION."
-  (let ((span (make-span start end)))
-    (set-span-property span 'delete-me delete-region)
+  (let ((span (span-make start end)))
+    (span-set-property span 'delete-me delete-region)
     (list (list span proof-command 'proof-done-retracting))))
 
 
@@ -2425,8 +2417,6 @@ command."
 ;; Proof General scripting mode definition, part 1.
 ;;
 
-(eval-and-compile			; to define vars
-;;; NB: autoload tag below doesn't work for d-d-m, autoload is in proof.el
 ;;;###autoload
 (define-derived-mode proof-mode fundamental-mode
   proof-general-name
@@ -2442,7 +2432,7 @@ command."
   ;; breaking regexps using \\s- that rely on that (showed up for Coq).
   ;; In fact it seems to be broken rather more seriously than that:
   ;; default syntax table of fundamental mode is not merged at all!
-  (if (and proof-running-on-XEmacs
+  (if (and (featurep 'xemacs)
 	   ;; hopefully fixed for later versions but we don't know yet
 	   (>= 21 emacs-major-version)
 	   (>= 5 emacs-minor-version))
@@ -2467,15 +2457,11 @@ command."
   ;; that they can be adjusted by prover specific code if need be.
   (proof-script-set-buffer-hooks)
 
-  (make-local-hook 'after-set-visited-file-name-hooks)
-  (add-hook 'after-set-visited-file-name-hooks 'proof-script-set-visited-file-name)
+  (add-hook 'after-set-visited-file-name-hooks 'proof-script-set-visited-file-name nil t)
 
-  (make-local-hook 'proof-activate-scripting-hook)
-  (make-local-hook 'proof-deactivate-scripting-hook)
-  (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t)))
+  (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t))
 
-;; NB: proof-mode-map declared by define-derived-mode above
-(proof-menu-define-keys proof-mode-map)   ;; NB: top-level form
+(proof-menu-define-keys proof-mode-map) ;; NB: proof-mode-map declared above
 
 (defun proof-script-set-visited-file-name ()
   "Called when visited file name is changed.
@@ -2505,10 +2491,8 @@ This hook also gives a warning in case this is the active scripting buffer."
   "Set the hooks for a proof script buffer.
 The hooks set here are cleared by `write-file', so we use this function
 to restore them using `after-set-visited-file-name-hooks'."
-  (make-local-hook 'kill-buffer-hook)
   (add-hook 'kill-buffer-hook 'proof-script-kill-buffer-fn t t)
   ;; Reverting buffer is same as killing it as far as PG is concerned
-  (make-local-hook 'before-revert-hook)
   (add-hook 'before-revert-hook 'proof-script-kill-buffer-fn t t))
 
 (defun proof-script-kill-buffer-fn ()
@@ -2734,6 +2718,8 @@ with something different."
 ;    proof-kill-goal-command		; do
     ))
 
+
+;;;###autoload
 (defun proof-config-done ()
   "Finish setup of Proof General scripting mode.
 Call this function in the derived mode for the proof assistant to
@@ -2756,10 +2742,6 @@ finish setup which depends on specific proof assistant configuration."
   ;; Make X-symbol ignore that we've asked for fixed mode
   (put major-mode 'x-symbol-mode-disable 'ignore)
   
-  ;; Now, define some values if they aren't defined already.
-  (unless proof-mode-for-script
-      (setq proof-mode-for-script major-mode))
-
   (if (and proof-non-undoables-regexp
 	   (not proof-ignore-for-undo-count))
       (setq proof-ignore-for-undo-count
@@ -2789,7 +2771,7 @@ finish setup which depends on specific proof assistant configuration."
   (setq indent-line-function 'proof-indent-line)
 
   ;; Toolbar and scripting menu
-  ;; NB: autloads proof-toolbar, which defines proof-toolbar-scripting-menu.
+  ;; NB: autoloads proof-toolbar, which defines proof-toolbar-scripting-menu.
   (proof-toolbar-setup)
 
   ;; Menus: the Proof-General and the specific menu
@@ -2816,7 +2798,7 @@ finish setup which depends on specific proof assistant configuration."
   ;; Localise the invisibility glyph (XEmacs only):
   (let ((img (proof-get-image "hiddenproof" t "<proof>")))
     (cond
-     ((and img proof-running-on-XEmacs)
+     ((and img (featurep 'xemacs))
       (set-glyph-image invisible-text-glyph img (current-buffer)))))
 
   (if (proof-ass x-symbol-enable)
@@ -2900,9 +2882,6 @@ Choice of function depends on configuration setting."
   ;; wouldn't need "pushnew").
   (if (proof-try-require 'func-menu)
    (progn
-     ;; FIXME: we'd like to let the library load later, but
-     ;; it's a bit tricky: this stuff doesn't seem to work
-     ;; in an eval-after-load body (local vars?).
      (unless proof-script-next-entity-regexps ; unless already set
        ;; Try to calculate a useful default value.
        ;; FIXME: this is rather complicated!  The use of the regexp
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 7b92770f..c36219e9 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -8,8 +8,17 @@
 ;; proof-shell.el,v 8.15 2005/09/30 09:45:36 da Exp
 ;;
 
-(require 'proof-menu)
-(require 'span)
+(eval-when-compile
+  (require 'cl)
+  (require 'span)
+  (require 'comint)
+  (require 'font-lock)
+  (require 'proof-autoloads)
+  (require 'proof-utils))
+
+(require 'pg-response)
+(require 'pg-goals)
+(require 'proof-script)
 
 ;;
 ;; Internal variables used in sub-modules
@@ -20,41 +29,33 @@
   "A record of the last string seen from the proof system.")
 
 
-;; sub-modules
-
-(require 'pg-response)			; buffers for goals/response
-(require 'pg-goals)			; associated output
-
-;; Nuke some byte compiler warnings.
-(eval-when-compile
-  (require 'comint)
-  (require 'font-lock))
 
 
-;; FIXME:
-;; Autoloads for proof-script (added to nuke warnings,
-;; maybe should be 'official' exported functions in proof.el)
-;; This helps see interface between proof-script / proof-shell.
-;; FIXME 2: We can probably assume that proof-script is always
-;; loaded before proof-shell, so just put a require on 
-;; proof-script here.
-(eval-and-compile
-  (mapcar (lambda (f) 
-	    (autoload f "proof-script"))
-	  '(proof-goto-end-of-locked
-	    proof-insert-pbp-command
-	    proof-detach-queue 
-	    proof-locked-end 
-	    proof-set-queue-endpoints
-	    proof-script-clear-queue-spans
-	    proof-file-to-buffer 
-	    proof-register-possibly-new-processed-file
-	    proof-restart-buffers)))
+;; ;; FIXME:
+;; ;; Autoloads for proof-script (added to nuke warnings,
+;; ;; maybe should be 'official' exported functions in proof.el)
+;; ;; This helps see interface between proof-script / proof-shell.
+;; ;; FIXME 2: We can probably assume that proof-script is always
+;; ;; loaded before proof-shell, so just put a require on 
+;; ;; proof-script here.
+;; (eval-and-compile
+;;   (mapcar (lambda (f) 
+;; 	    (autoload f "proof-script"))
+;; 	  '(proof-goto-end-of-locked
+;; 	    proof-insert-pbp-command
+;; 	    proof-detach-queue 
+;; 	    proof-locked-end 
+;; 	    proof-set-queue-endpoints
+;; 	    proof-script-clear-queue-spans
+;; 	    proof-file-to-buffer 
+;; 	    proof-register-possibly-new-processed-file
+;; 	    proof-restart-buffers)))
 
 ;; FIXME:
 ;; Some variables from proof-shell are also used, in particular,
 ;; the menus.  These should probably be moved out to proof-menu.
 
+
 ;; ============================================================
 ;;
 ;; Internal variables used by proof shell
@@ -124,7 +125,7 @@ to examine proof-shell-last-output.")
 ;; 
 
 (defcustom proof-shell-active-scripting-indicator
-  (if proof-running-on-XEmacs
+  (if (featurep 'xemacs)
       (cons (make-extent nil nil) " Scripting ")
     " Scripting")
   "Modeline indicator for active scripting buffer.
@@ -213,7 +214,7 @@ If QUEUEMODE is supplied, set the lock to that value."
   (setq proof-shell-busy (or queuemode t))
   ;; Make modeline indicator follow state (on XEmacs at least)
   (cond
-   (proof-running-on-XEmacs
+   ((featurep 'xemacs)
     (if (extentp (car proof-shell-active-scripting-indicator))
 	(set-extent-properties
 	 (car proof-shell-active-scripting-indicator)
@@ -227,7 +228,7 @@ to err-or-int."
   (setq proof-shell-error-or-interrupt-seen err-or-int)
   (setq proof-shell-busy nil)
   (cond
-   (proof-running-on-XEmacs
+   ((featurep 'xemacs)
     (if (extentp (car proof-shell-active-scripting-indicator))
 	(set-extent-properties
 	 (car proof-shell-active-scripting-indicator)
@@ -247,9 +248,6 @@ present in later versions!"
   :type 'boolean
   :group 'proof-shell)
 
-(deflocal proof-eagerly-raise t
-  "Non-nil if this buffer will be eagerly raised/displayed on startup.")
-
 (defun proof-shell-set-text-representation ()
   "Adjust representation for the current buffer to match `proof-shell-unicode'."
   (if proof-shell-unicode
@@ -271,19 +269,9 @@ Does nothing if proof assistant is already running."
   (interactive)
   (unless (proof-shell-live-buffer)
 
-    ;; This should configure the mode-setting variables
-    ;; proof-mode-for-<blah> so we can set the modes below.
-    ;; <blah>=shell,goals,response.  We also need to set
-    ;; proof-prog-name to start the program!
-    (run-hooks 'proof-pre-shell-start-hook)
-
-    ;; Clear some state [ fixme: should clear more? ]
-    (setq proof-included-files-list nil)
+    (setq proof-included-files-list nil) ; clear some state
 
-    ;; Added 05/99 by Patrick L.
     (let ((name (buffer-file-name (current-buffer))))
-      ;; FIXME : we check that the buffer corresponds to a file,
-      ;; but we do not check that it is in coq- or isa-mode
       (if (and name proof-prog-name-guess proof-guess-command-line)
 	  (setq proof-prog-name
 		(apply proof-guess-command-line (list name)))))
@@ -301,7 +289,7 @@ Does nothing if proof assistant is already running."
 		 ;; If argument list supplied in <PA>-prog-args, use that.
 		  (cons proof-prog-name (proof-ass prog-args))
 		;; Otherwise, cut prog name on spaces
-		(proof-string-to-list proof-prog-name " ")))
+		(split-string proof-prog-name)))
 	     (prog-name-list
 	      ;; Splice in proof-rsh-command if it's non-nil 
 	      (if (and proof-rsh-command
@@ -394,7 +382,7 @@ Does nothing if proof assistant is already running."
 	(if proof-shell-thms-output-regexp
 	    (setq proof-thms-buffer (get-buffer-create thms)))
 	;; Set the special-display-regexps now we have the buffer names
-	(setq proof-shell-special-display-regexp
+	(setq pg-response-special-display-regexp
 	      (proof-regexp-alt goals resp trace thms)))
 
       (with-current-buffer proof-shell-buffer
@@ -448,7 +436,7 @@ Does nothing if proof assistant is already running."
 	(proof-with-current-buffer-if-exists proof-trace-buffer
 	  (proof-shell-set-text-representation)
 	  (funcall proof-mode-for-response)
-	  (setq proof-eagerly-raise nil))
+	  (setq pg-response-eagerly-raise nil))
 
 	(set-buffer proof-goals-buffer)
 	(proof-shell-set-text-representation)
@@ -466,7 +454,7 @@ Does nothing if proof assistant is already running."
 	  ;; Otherwise just try to remove modeline from PG buffers
 	  ;; in XEmacs (FIXME: hope to remove this and just have
 	  ;; previous case)
-	  (if proof-running-on-XEmacs
+	  (if (featurep 'xemacs)
 	      (proof-map-buffers
 		(list proof-goals-buffer proof-response-buffer
 		      proof-trace-buffer proof-thms-buffer)
@@ -690,7 +678,7 @@ This is a subroutine of `proof-shell-handle-error'."
 	(setq string
 	      (pg-assoc-strip-subterm-markup string)))
       ;; Erase if need be, and erase next time round too.
-      (proof-shell-maybe-erase-response t nil)
+      (pg-response-maybe-erase t nil)
       (pg-response-display-with-face string append-face))))
       
   ;; We used to fetch the output from proof-shell-buffer.  I'm not sure what
@@ -703,27 +691,22 @@ This is a subroutine of `proof-shell-handle-error'."
   ;; This breaks Isabelle, for example, because special
   ;; characters have been stripped from proof-shell-last-output,
   ;; but start-regexp may contain them.
-  ;; For now, test _not_ removing specials (see proof-shell-process-output)
-  ;; 
-  ;; Sun Feb 16: test removing of specials again, to see if this
-  ;; fixes PG/Isabelle <^sync> problem.
-  ;;
 
 ;  ;; stef's version:
 ;   (let ((string proof-shell-last-output))
 ;     ;; Strip off start-regexp --- if it matches 
-;     ;; FIXME: if it doesn't we shouldn't be called, but something
+;     ;; NOTE: if it doesn't we shouldn't be called, but something
 ;     ;;  odd happens here now, so add a safety check.
 ;      (if (and start-regexp (string-match start-regexp string))
 ;	  (setq string (substring string (match-beginning 0))))
-;      ;; FIXME: if the shell buffer is x-symbol minor mode,
+;      ;; NOTE: if the shell buffer is x-symbol minor mode,
 ;      ;; this string can contain X-Symbol characters, which
 ;      ;; is not suitable for processing with proof-fontify-region.
 ;      (unless pg-use-specials-for-fontify
 ;	(setq string
 ;	      (pg-assoc-strip-subterm-markup string)))
 ;      ;; Erase if need be, and erase next time round too.
-;      (proof-shell-maybe-erase-response t nil)
+;      (pg-response-maybe-erase t nil)
 ;      (pg-response-display-with-face string append-face)))
 
 
@@ -734,17 +717,10 @@ are not dealt with eagerly during script processing, namely
 'abort, 'response, 'goals outputs."
   ;; NB: this function is important even when called with an empty
   ;; delayed output, since it serves to clear buffers.  
-
-  ;; FIXME: there's a display anomaly here with Isar/shrink mode which
-  ;; is tricky to find.  Error message causes an empty delayed output
-  ;; for goals buffer to split main window in two rather than
-  ;; shrinking to fit.  Running through the debugger the right
-  ;; thing happens (display in a correctly sized window).  Somewhere
-  ;; there is a spurious match not protected too: C-c C-n gives
   (cond
    ;; Response buffer output
    ((eq proof-shell-delayed-output-kind 'abort)
-     ;; Did display our own message "Aborted."  why??
+    ;; Previously we displayed a message here, let the prover do that now.
     (pg-response-display proof-shell-delayed-output))
    ((eq proof-shell-delayed-output-kind 'response)
     (unless proof-shell-no-response-display
@@ -766,7 +742,7 @@ are not dealt with eagerly during script processing, namely
   "If non-nil, do not display errors from the prover. 
 An internal setting used in `proof-shell-invisible-cmd-get-result'.")
 
-;; FIXME: combine next two functions?
+;; TODO: combine next two functions
 
 (defun proof-shell-handle-error (cmd)
   "React on an error message triggered by the prover.
@@ -790,7 +766,7 @@ Then we call `proof-shell-error-or-interrupt-action', which see."
    "React on an interrupt message from the prover.
 Runs `proof-shell-error-or-interrupt-action'."
    (unless proof-shell-no-error-display
-     (proof-shell-maybe-erase-response t t t) ; force cleaned now & next
+     (pg-response-maybe-erase t t t) ; force cleaned now & next
      (proof-shell-handle-output
       (if proof-shell-truncate-before-error proof-shell-interrupt-regexp)
       'proof-error-face)
@@ -815,16 +791,14 @@ Then we call `proof-shell-handle-error-or-interrupt-hook'."
     (setq proof-action-list nil)
     (proof-release-lock err-or-int)
     ;; 
-    (unless proof-shell-no-error-display ;; internal call
-      ;; Give a hint about C-c C-`.
-      ;; FIXME: this is rather approximate,
-      ;; we ought to check whether there is an error location in 
-      ;; the latest message, not just somewhere in the response buffer.
+    (unless proof-shell-no-error-display ; internal call
+      ;; Give a hint about C-c C-`.  NB: this is rather approximate,
+      ;; we ought to check whether there is an error location in the
+      ;; latest message, not just somewhere in the response buffer.
       (if (pg-response-has-error-location) 
 	  (pg-next-error-hint)))
     ;; Make sure that prover is outputting data now.
     ;; FIXME: put something here!
-    ;; New: this is called for interrupts too.
     (run-hooks 'proof-shell-handle-error-or-interrupt-hook)))
 
 (defun proof-goals-pos (span maparg)
@@ -835,7 +809,7 @@ Then we call `proof-shell-handle-error-or-interrupt-hook'."
 (defun proof-pbp-focus-on-first-goal ()
   "If the `proof-goals-buffer' contains goals, bring the first one into view.
 This is a hook function for proof-shell-handle-delayed-output-hook."
-  (and proof-running-on-XEmacs 		;; FIXME: map-extents exists on Emacs21
+  (and (featurep 'xemacs) 		;; FIXME: map-extents exists on Emacs21
        (fboundp 'map-extents)		;; but with different typing
        (let
 	   ((pos (map-extents 'proof-goals-pos proof-goals-buffer
@@ -963,12 +937,13 @@ which see."
 (defvar proof-shell-insert-space-fudge 
   (cond
    ((string-match "21.*XEmacs" emacs-version) " ")
-   (proof-running-on-XEmacs "")
+   ((featurep 'xemacs) "")
    (t " "))
   "String to insert after setting proof marker to prevent it moving.
 Allows for a difference between different versions of comint across
 different Emacs versions.")
 
+;;;###autoload
 (defun proof-shell-insert (string action)
   "Insert STRING at the end of the proof shell, call `comint-send-input'.
 
@@ -1251,9 +1226,9 @@ and indentation.  Assumes proof-script-buffer is active."
 	;; a unit, i.e. sent to the proof assistant together.
 	;; FIXME da: this seems very similar to proof-insert-pbp-command
 	;; in proof-script.el.  Should be unified, I suspect.
-	(setq span (make-span (proof-locked-end) (point)))
-	(set-span-property span 'type 'pbp)
-	(set-span-property span 'cmd cmd)
+	(setq span (span-make (proof-locked-end) (point)))
+	(span-set-property span 'type 'pbp)
+	(span-set-property span 'cmd cmd)
 	(proof-set-queue-endpoints (proof-locked-end) (point))
 	(setq proof-action-list 
 	      (cons (car proof-action-list) 
@@ -1394,7 +1369,7 @@ MESSAGE should be a string annotated with
      ((and proof-shell-clear-response-regexp
 	   (string-match proof-shell-clear-response-regexp message))
       ;; Erase response buffer and possibly its windows.
-      (proof-shell-maybe-erase-response nil t t))
+      (pg-response-maybe-erase nil t t))
      
      ;; CASE clear goals: prover asks PG to clear goals buffer
      ((and proof-shell-clear-goals-regexp
@@ -1462,7 +1437,7 @@ MESSAGE should be a string annotated with
       ;; if necessary, but don't clear it the next time.
       ;; Don't bother remove the window for the response buffer
       ;; because we're about to put a message in it.
-      (proof-shell-maybe-erase-response nil nil)
+      (pg-response-maybe-erase nil nil)
       (let ((stripped (if proof-shell-unicode 
 			  message
 			(pg-remove-specials-in-string
@@ -2014,8 +1989,7 @@ usual, unless NOERROR is non-nil."
 ;; Proof General shell mode definition
 ;;
 
-(eval-and-compile			; to define vars
-;;; NB: autoload tag below doesn't work for d-d-m, autoload is in proof.el
+;(eval-and-compile			; to define vars
 ;;;###autoload
 (define-derived-mode proof-shell-mode comint-mode 
   "proof-shell" "Proof General shell mode class for proof assistant processes"
@@ -2049,7 +2023,7 @@ usual, unless NOERROR is non-nil."
   ;; FIXME: this is a work-around for a nasty GNU Emacs 21.2
   ;; bug which HANGS Emacs sometimes if special characters
   ;; are hidden.  (e.g. try M-x column-number-mode)
-  (unless proof-running-on-Emacs21
+  (unless (not (featurep 'xemacs))
     (proof-shell-dont-show-annotations))
 
   ;; Proof marker is initialised in filter to first prompt found
@@ -2076,12 +2050,11 @@ usual, unless NOERROR is non-nil."
   ;; What actually happens: an obscure infinite loop somewhere
   ;; that can lead to "lisp nesting exceeded" somewhere, when
   ;; shell startup fails.  Ugly, but low priority to fix.
-  ))
+  );)
 
-(easy-menu-define proof-shell-mode-menu
-		  proof-shell-mode-map
-		  "Menu used in Proof General shell mode."
-		  proof-aux-menu)
+(easy-menu-define proof-shell-mode-menu proof-shell-mode-map
+  "Menu used in Proof General shell mode."
+  (proof-aux-menu))
 
 
 ;;
@@ -2093,6 +2066,7 @@ usual, unless NOERROR is non-nil."
     ))
 
 
+;;;###autoload
 (defun proof-shell-config-done ()
   "Initialise the specific prover after the child has been configured.
 Every derived shell mode should call this function at the end of
@@ -2108,7 +2082,6 @@ processing."
 
     (let ((proc (get-buffer-process proof-shell-buffer)))
       ;; Add the kill buffer function and process sentinel
-      (make-local-hook 'kill-buffer-hook)
       (add-hook 'kill-buffer-hook 'proof-shell-kill-function t t)
       (set-process-sentinel proc 'proof-shell-bail-out)
 
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 883298f7..50ac05d8 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -7,30 +7,96 @@
 ;;
 ;; $Id$
 ;;
-;; NB: Normally you will not need to edit this file.  
+;; 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 
+;; can be set to affect load behaviour; see info documentation.
+;;
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Master table of supported proof assistants. 
+;;
+
+(defconst proof-assistant-table-default
+    '((isar   "Isabelle" "\\.thy$")
+      (coq    "Coq"	 "\\.v$\\|\\.v8$\\|\\.v7$")
+      (phox   "PhoX"	 "\\.phx$")
+      ;; (lego   "LEGO"	 "\\.l$")
+      ;; (ccc    "CASL Consistency Checker"  "\\.ccc$")
+
+      ;; For the demonstration instance of Proof General,
+      ;; uncomment line below and set
+      ;; 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$")
+      ;; (lclam    "Lambda-CLAM"   "\\.lcm$")
+      ;; (pgshell	"PG-Shell"	"\\.pgsh$")
+      )
+    "Default value for `proof-assistant-table', which see.")
 
-(if (featurep 'proof-site)	
-    nil					; don't load twice
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Emacs and PG versions
+;;
 
-(if (or  (not (boundp 'emacs-major-version))
-	 (< emacs-major-version 20))
+(eval-and-compile 
+  (defun pg-emacs-version-cookie ()
+    (format (if (string-match "XEmacs" emacs-version) ; (featurep 'xemacs) gets optimised!
+		"XEmacs %d.%d" "GNU Emacs %d.%d")
+	    emacs-major-version emacs-minor-version))
+  
+  (defconst pg-compiled-for (eval-when-compile (pg-emacs-version-cookie))
+    "Version of Emacs we're compiled for (or running on, if interpreted)."))
+
+(if (or (not (boundp 'emacs-major-version))
+	(< emacs-major-version 21))
     (error "Proof General is not compatible with Emacs %s" emacs-version))
 
+(unless (equal pg-compiled-for (pg-emacs-version-cookie))
+  (error 
+   (format 
+    "Proof General was compiled for %s but running on %s: please run \"make clean; make\""
+    pg-compiled-for (pg-emacs-version-cookie))))
+  
+(eval-and-compile
+;; WARNING: do not edit next line (constant is edited in Makefile.devel)
+  (defconst proof-general-version "Proof General Version 3.7pre071214."
+    "Version string identifying Proof General release."))
+
+(defconst proof-general-short-version 
+  (eval-when-compile
+    (progn
+      (string-match "Version \\([^ ]+\\)\\." proof-general-version)
+      (match-string 1 proof-general-version))))
+
+(defconst proof-general-version-year "2008")
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Top-level customization groups
+;;
+
 (defgroup proof-general nil
   "Customization of Proof General."
   :group 'applications
   :prefix "proof-")
 
-
-;; This customization group gathers together
-;; the internals of Proof General which control
-;; configuration to different proof assistants.
-;; This is for development purposes rather than
-;; user-level customization, so this group does
-;; not belong to 'proof-general (or any other group).
 (defgroup proof-general-internals nil
-  "Customization of Proof General internals."
+  "Customization of Proof General internals for proof assistant configuration."
   :group 'applications
   :group 'proof-general
   :prefix "proof-")
@@ -38,10 +104,12 @@
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Directories
+;; Directories. Set at load time so compiled files can be relocated.
+;; Load path must be extended manually during compilation.
 ;;
+
 (defun proof-home-directory-fn ()
-  "Used to set proof-home-directory"
+  "Used to set proof-home-directory."
   (let ((s (getenv  "PROOFGENERAL_HOME")))
     (if s
 	(if (string-match "/$" s) s (concat s "/"))
@@ -53,7 +121,7 @@
 
 (defcustom proof-home-directory
   (proof-home-directory-fn)
-  "Directory where Proof General is installed. Ends with slash.
+  "Directory where Proof General is installed.  Ends with slash.
 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."
@@ -62,79 +130,54 @@ You can use customize to set this variable."
 
 (defcustom proof-images-directory
   (concat proof-home-directory "images/")
-    "Where Proof General image files are installed. Ends with slash."
+    "Where Proof General image files are installed.  Ends with slash."
   :type 'directory
   :group 'proof-general-internals)
 
 (defcustom proof-info-directory
   (concat proof-home-directory "doc/")
-  "Where Proof General Info files are installed. Ends with slash."
+  "Where Proof General Info files are installed.  Ends with slash."
   :type 'directory
   :group 'proof-general-internals)
 
-;; Add the info directory to the end of Emacs Info path if need be.
+;; Extend load path for the generic and library files.
+(add-to-list 'load-path (concat proof-home-directory "generic/"))
+(add-to-list 'load-path (concat proof-home-directory "lib/"))
+
+;; Declare some global variables
+(require 'pg-vars)
+
+;; Add the info directory to the Info path
 (if ;; NB: proof-info-directory is bogus in RPM distrib.
     (file-exists-p proof-info-directory)
     (if (and (boundp 'Info-directory-list) (consp Info-directory-list))
 	;; Info is already initialized.  Update its variables.
-	;; This probably never happens.  -stef
-	;; da: actually it does in XEmacs.
+	;; This probably never happens in Emacs, but does in XEmacs.
 	(if (not (member proof-info-directory Info-directory-list))
 	    (progn
-	      (setq Info-directory-list
-		    (cons proof-info-directory Info-directory-list))
+	      (add-to-list 'Info-directory-list proof-info-directory)
 	      (setq Info-dir-contents nil)))
       ;; Info is not yet initialized.  Change its default.
-      ;; da: NB: Emacs 21.2.1 still uses Info-default-directory-list
-      ;; although XEmacs complains about it being obsolete here.
-      (if (not (member proof-info-directory Info-default-directory-list))
-	  (setq Info-default-directory-list
-		(cons proof-info-directory Info-default-directory-list)))))
+      ;; Emacs uses Info-default-directory-list but it's deprecated in XEmacs
+      (add-to-list 'Info-default-directory-list proof-info-directory)))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Master table of supported proof assistants. 
-;;
 (defcustom proof-assistant-table
   (apply 
    'append
    (mapcar
-   ;; Discard entries whose directories have been removed.
+    ;; Discard entries whose directories have been removed.
     (lambda (dne)
       (let ((atts (file-attributes (concat proof-home-directory 
 					   (symbol-name (car dne))))))
 	(if (and atts (eq 't (car atts)))
 	    (list dne)
 	  nil)))
-   '(
-;;
-;; To Use HOL, uncomment the line below.  It's disabled
-;; by default because of clash with SML mode (same for .ML).
-;;
-;; For the demonstration instance of Proof General,
-;; uncomment first line below and set
-;; export PROOFGENERAL_ASSISTANTS=demoisa. 
-;;
-;;    (demoisa    "Isabelle Demo"	"\\.ML$")
-    (isar       "Isabelle"      "\\.thy$")
-    (lego	"LEGO"		"\\.l$")
-    (coq	"Coq"		"\\.v$\\|\\.v8$\\|\\.v7$")
-    (phox	"PhoX"		"\\.phx$")
-    (ccc        "CASL Consistency Checker"  "\\.ccc$")
-    ;; The following provers are not fully supported, and have only
-    ;; preliminary support written (please volunteer to improve them!)
-
-;;    (hol98	"HOL"		"\\.sml$")
-    (acl2	"ACL2"		"\\.acl2$")
-    ;; (twelf	"Twelf"		"\\.elf$")
-    ;; The following provers have experimental support, WIP
-    (plastic	"Plastic"	"\\.lf$")
-    (lclam      "Lambda-CLAM"   "\\.lcm$")
-    ;; Finally, the next instance isn't a prover at all!
-    (pgshell	"PG-Shell"	"\\.pgsh$")
-    )))
+    proof-assistant-table-default))
   "*Proof General's table of supported proof assistants.
-Extend this table to add a new proof assistant.
+This is copied from `proof-assistant-table-default' at load time,
+removing any entries that do not have a corresponding directory
+under `proof-home-directory'.
+
 Each entry is a list of the form
 
     (SYMBOL NAME AUTOMODE-REGEXP)
@@ -147,32 +190,12 @@ 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
-variable proof-home-directory."
+where PROOF-HOME-DIRECTORY is the value of the
+variable `proof-home-directory'."
   :type '(repeat (list symbol string string))
   :group 'proof-general-internals)
 
 
-
-
-
-;; A utility function.  Is there an alternative?
-(defun proof-string-to-list (s separator) 
-  "Return the list of words in S separated by SEPARATOR.
-If S is nil, return empty list."
-  (if s
-      (let ((end-of-word-occurence (string-match (concat separator "+") s)))
-	(if (not end-of-word-occurence)
-	    (if (string= s "") 
-		nil
-	      (list s))
-	  (cons (substring s 0 end-of-word-occurence) 
-		(proof-string-to-list 
-		 (substring s
-			    (string-match (concat "[^" separator "]")
-					  s end-of-word-occurence)) 
-		 separator))))))
-
 (defcustom proof-assistants nil
   (concat
    "*Choice of proof assistants to use with Proof General.
@@ -180,7 +203,7 @@ A list of symbols chosen from:"
    (apply 'concat (mapcar (lambda (astnt) 
 			    (concat " '" (symbol-name (car astnt))))
 			  proof-assistant-table)) 
-".\nIf nil, the default will be ALL proof assistants.
+".\nIf nil, the default will be ALL available proof assistants.
 
 Each proof assistant defines its own instance of Proof General,
 providing session control, script management, etc.  Proof General
@@ -201,22 +224,22 @@ Note: to change proof assistant, you must start a new Emacs session.")
 		      proof-assistant-table))
   :group 'proof-general)
 
-
-;; Extend load path for the generic and library files.
-(let ((addpath (lambda (p)
-		 (or (member p load-path)
-		     (setq load-path (cons p load-path))))))
-  (funcall addpath (concat proof-home-directory "generic/"))
-  (funcall addpath (concat proof-home-directory "lib/")))
-
-(defun proof-ready-for-assistant (assistant-name assistantsym)
-  "Configure PG for ASSISTANT-NAME, symbol ASSISTANTSYM."
+(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'."
   (let*
       ((sname		 (symbol-name assistantsym))
+       (assistant-name   (or assistant-name
+			     (car-safe 
+			      (cdr-safe (assoc assistantsym
+					       proof-assistant-table)))
+			     sname))
        (cusgrp-rt	 
 	;; Normalized a bit to remove spaces and funny characters
 	;; FIXME UGLY compatibility hack  
 	;; (can use cl macro `substitute' but want to avoid cl here)
+	;; NOTE: GNU Emacs 22/XEmacs 21.5 both have replace-regexp-in-string
+	;; PG 3.8: move version forward here.
 	(if (fboundp 'replace-in-string) 
 	    ;; XEmacs
 	    (replace-in-string (downcase assistant-name) "/\\|[ \t]+" "-")
@@ -225,11 +248,10 @@ Note: to change proof assistant, you must start a new Emacs session.")
 	   ?/ ?\- 
 	   (subst-char-in-string ?\ ?\- (downcase assistant-name)))))
 	;; END compatibility hack
-       (cusgrp	 (intern cusgrp-rt))
-       (cus-internals  (intern (concat cusgrp-rt "-config")))
-       ;; NB: Dir name for each prover is the same as its symbol name!
-       (elisp-dir    sname)
-       (loadpath-elt (concat proof-home-directory elisp-dir "/")))
+       (cusgrp	      (intern cusgrp-rt))
+       (cus-internals (intern (concat cusgrp-rt "-config")))
+       (elisp-dir     sname)		; NB: dirname same as symbol name!
+       (loadpath-elt  (concat proof-home-directory elisp-dir "/")))
     (eval `(progn
        ;; Make a customization group for this assistant
        (defgroup ,cusgrp nil
@@ -251,16 +273,23 @@ Note: to change proof assistant, you must start a new Emacs session.")
        (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 
+       (require 'pg-custom)
+       (setq proof-mode-for-shell (proof-ass-sym shell-mode))
+       (setq proof-mode-for-response (proof-ass-sym response-mode))
+       (setq proof-mode-for-goals (proof-ass-sym goals-mode))
+       (setq proof-mode-for-script (proof-ass-sym mode))
        ;; Extend the load path if necessary
        (if (not (member ,loadpath-elt load-path))
-	   (setq load-path (cons ,loadpath-elt load-path)))))))
+	   (setq load-path (cons ,loadpath-elt load-path)))
+       ;; Run hooks for late initialisation
+       (run-hooks 'proof-ready-for-assistant-hook)))))
+
 
-;; Now add auto-loads and load-path elements to support the 
-;; proof assistants selected, and define a stub 
+;; Add auto-loads and load-path elements to support the 
+;; proof assistants selected, and define stub major mode functions
 (let ((assistants
-       (or (mapcar 'intern
-		   (proof-string-to-list
-		    (getenv "PROOFGENERAL_ASSISTANTS") " "))
+       (or (mapcar 'intern (split-string (or (getenv "PROOFGENERAL_ASSISTANTS") "")))
 	   proof-assistants
 	   (mapcar (lambda (astnt) (car astnt)) proof-assistant-table))))
   (while assistants
@@ -281,103 +310,43 @@ Note: to change proof assistant, you must start a new Emacs session.")
 	 ;; 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 do some automatic initialization and load
 	 ;; the specific code.
 	 (mode-stub
-	   `(lambda ()
-	      ,(concat
-		 "Major mode for editing scripts for proof assistant "
-		 assistant-name
-		 ".\nThis is a stub which loads the real function.")
-	      (interactive)
-	      ;; Give a message and stop loading if proof-assistant is
-	      ;; already set: things go wrong if proof general is
-	      ;; loaded for more than one prover.
-	      (cond
-	       ((and (boundp 'proof-assistant)
-		     (not (string-equal proof-assistant "")))
-		(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 
-		      " Proof General error: Proof General already in use for "
-		      proof-assistant))))
-	       (t
-		;; prepare variables and load path
-		(proof-ready-for-assistant ,assistant-name 
-					   (quote ,assistant))
-		;; load the real mode and invoke it. 
-		(load-library ,elisp-file)
-		(,proofgen-mode))))))
-
-      (setq auto-mode-alist 
-	    (cons (cons regexp proofgen-mode) auto-mode-alist))
-
-      (fset proofgen-mode mode-stub)
-      
-      (setq assistants (cdr assistants))
-      )))
-
-;; WARNING: do not edit below here (the next constant is set automatically)
-(defconst proof-general-version "Proof General Version 3.7pre071214. Released by da."
- "Version string identifying Proof General release.")
-
-(defconst proof-general-short-version 
-  (progn
-    (string-match "Version \\([^ ]+\\)\\." proof-general-version)
-    (match-string 1 proof-general-version)))
-
-(defconst proof-general-version-year "2007")
-
-;; Now define a few autoloads and basic variables.
-
-;; 1.8.01: add a dummy package-provide command so proof-autoloads
-;; is compatible with FSF Emacs.  Needed for next require
-;; (otherwise would be in proof-compat.el).
-(or (fboundp 'package-provide)
-    (defun package-provide (name &rest attributes)
-      "Dummy version of XEmacs function for FSF compatibility."))
-
-
-(require 'proof-autoloads)		; autoloaded functions
-
-(defcustom 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 
-proof-assistant-table."
-  :type 'sexp
-  :group 'prover-config)
-
-(defcustom 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 
-stub defined in proof-site, from the name given in
-proof-assistant-table."
-  :type 'sexp
-  :group 'prover-config)
-
-(defcustom proof-assistant ""
-  "Name of the proof assistant Proof General is using.
-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."
-  :type 'string
-  :group 'prover-config)
-
-(defcustom proof-assistant-symbol nil
-  "Symbol for the proof assistant Proof General is using.
-Used for automatic configuration based on standard variable names.
-Settings will be found by looking for names beginning with this
-symbol as a prefix.
-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."
-  :type 'sexp
-  :group 'prover-config)
+	  `(lambda ()
+	     ,(concat
+	       "Major mode for editing scripts for proof assistant "
+	       assistant-name
+	       ".\nThis is a stub which loads the real function.")
+	     (interactive)
+	     ;; Give a message and stop loading if proof-assistant is
+	     ;; already set: things go wrong if proof general is
+	     ;; loaded for more than one prover.
+	     (cond
+	      ((and (boundp 'proof-assistant)
+		    (not (string-equal proof-assistant "")))
+	       (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 
+		     " 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-library ,elisp-file)
+	       (,proofgen-mode))))))
+	
+	(setq auto-mode-alist 
+	      (cons (cons regexp proofgen-mode) auto-mode-alist))
+	
+	(fset proofgen-mode mode-stub)
+	
+	(setq assistants (cdr assistants)))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
@@ -385,7 +354,7 @@ proof-assistant-table."
 ;;;
 
 (if (and
-     (string-match "XEmacs" emacs-version) 
+     (featurep 'xemacs)
      (not (featurep 'x-symbol-hooks)) ;; unless already loaded
      (file-exists-p (concat proof-home-directory ;; or our version removed
 			    "x-symbol/lisp/"))
@@ -397,5 +366,5 @@ proof-assistant-table."
 			 (string-match "x-symbol" pkg))
 		       ad-return-value))))
 
-(provide 'proof-site))
+(provide 'proof-site)
 ;; proof-site.el ends here
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index de0350ed..d4fe8695 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -8,8 +8,6 @@
 ;;
 ;;
 
-(require 'proof-compat)			;; for Emacs version flags
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Customization of splash screen (was in proof-config)
 
@@ -44,10 +42,7 @@ Proof General."
     nil
     nil
 "    Please report problems at http://proofgeneral.inf.ed.ac.uk/trac
-    Visit the Proof General wiki at http://proofgeneral.inf.ed.ac.uk/wiki"
-    nil
-    (unless (or proof-running-on-XEmacs proof-running-on-Emacs21)
-     "For a better Proof General experience, please use GNU Emacs 21 or XEmacs"))
+    Visit the Proof General wiki at http://proofgeneral.inf.ed.ac.uk/wiki")
   "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.  
@@ -72,14 +67,15 @@ If it is nil, a new line is inserted."
 
 
 ;; Compatibility between Emacs/XEmacs.
-(if (string-match "XEmacs" emacs-version)
-  ;; Constant nil function
-  (defun proof-emacs-imagep (img)
-    "See if IMG is an Emacs 21 image descriptor (returns nil since not E21)."
-    nil)
-  (defun proof-emacs-imagep (img)
-    "See if IMG is an Emacs 21 image descriptor."
-    (and (listp img) (eq (car img) 'image))))
+(eval-and-compile
+  (if (featurep 'xemacs)
+      ;; Constant nil function
+      (defsubst proof-emacs-imagep (img)
+	"See if IMG is an Emacs image descriptor (returns nil here on XEmacs)."
+	nil)
+    (defsubst proof-emacs-imagep (img)
+      "See if IMG is an Emacs image descriptor."
+      (and (listp img) (eq (car img) 'image)))))
 
 
 (defun proof-get-image (name &optional nojpeg default)
@@ -93,21 +89,20 @@ DEFAULT gives return value in case image not valid."
 	(gif (vector 'gif :file
 		     (concat proof-images-directory ".gif")))
 	(validfn (lambda (inst)
-		   (and (valid-instantiator-p inst 'image)
+		   (and (featurep 'xemacs)
+			(valid-instantiator-p inst 'image)
 			(file-readable-p (aref inst 2)))))
 	img)
   (cond
-   ((and proof-running-on-XEmacs 
-	 (pg-window-system) 
+   ((and (featurep 'xemacs) window-system
 	 (featurep 'jpeg) (not nojpeg)
 	 (funcall validfn jpg))
     jpg)
-   ((and proof-running-on-XEmacs (pg-window-system)
+   ((and (featurep 'xemacs) window-system
 	 (featurep 'gif) (funcall validfn gif))
     gif)
    ((and
-     proof-running-on-Emacs21
-     (pg-window-system)
+     (not (featurep 'xemacs)) window-system
      (setq img 
 	   (find-image
 	    (list
@@ -132,7 +127,7 @@ Borrowed from startup-center-spaces."
 	 (fill-area-width  (* avg-pixwidth (- fill-column left-margin)))
 	 (glyph-pixwidth   (cond ((stringp glyph) 
 				  (* avg-pixwidth (length glyph)))
-				 ((and (fboundp 'glyphp)
+				 ((and (featurep 'xemacs)
 				       (glyphp glyph))
 				  (glyph-width glyph))
 				 ((proof-emacs-imagep glyph)
@@ -166,7 +161,7 @@ Borrowed from startup-center-spaces."
 	      (progn
 		(if (cdr proof-splash-timeout-conf)
 		    (set-window-configuration (cdr proof-splash-timeout-conf)))
-		(if proof-running-on-XEmacs
+		(if (featurep 'xemacs)
 		    (redraw-frame nil t))))
 	  ;; Indicate removed splash screen; disable timeout
 	  (disable-timeout (car proof-splash-timeout-conf))
@@ -222,7 +217,7 @@ Otherwise, timeout inside this function after 10 seconds or so."
       (while splash-contents
 	(setq s (car splash-contents))
 	(cond
-	 ((and proof-running-on-XEmacs
+	 ((and (featurep 'xemacs)
 	       (vectorp s)
 	       (valid-instantiator-p s 'image))
 	  (let ((gly (make-glyph s)))
@@ -271,7 +266,7 @@ Otherwise, timeout inside this function after 10 seconds or so."
 (defun proof-splash-message ()
   "Make sure the user gets welcomed one way or another."
   (interactive)
-  (unless (or proof-splash-seen (noninteractive))
+  (unless (or proof-splash-seen noninteractive)
     (if proof-splash-enable
 	(proof-splash-display-screen (not (interactive-p)))
       ;; Otherwise, a message
@@ -282,17 +277,16 @@ Otherwise, timeout inside this function after 10 seconds or so."
   "Wait for proof-splash-timeout or input, then remove self from hook."
   (while (and proof-splash-timeout-conf ;; timeout still active
 	      (not (input-pending-p)))
-    (if proof-running-on-XEmacs
+    (if (featurep 'xemacs)
 	(sit-for 0 t)			; XEmacs: wait without redisplay
       ; (sit-for 1 0 t)))		; FSF: NODISP arg seems broken
       (sit-for 0)))
   (if proof-splash-timeout-conf         ;; not removed yet
       (proof-splash-remove-screen))
-  (if (and (input-pending-p)
-	   (fboundp 'next-command-event)) ; 3.3: this function
-					  ; disappeared from emacs, sigh
-      (setq unread-command-events
-	    (cons (next-command-event) unread-command-events)))
+  (if (fboundp 'next-command-event) ; 3.3: Emacs removed this
+      (if (input-pending-p)
+	  (setq unread-command-events
+		(cons (next-command-event) unread-command-events))))
   (remove-hook 'proof-mode-hook 'proof-splash-timeout-waiter))
 
 (defvar proof-splash-old-frame-title-format nil)
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 4fa9a6c3..5a96ec05 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -9,7 +9,6 @@
 ;;
 
 (require 'font-lock)
-(require 'proof-config)
 
 ;; FIXME da: would regexp-opt be better here?  Or maybe
 ;;  (concat "\\<" (regexp-opt l) "\\>")
@@ -122,17 +121,17 @@ If so, return non-nil."
 
 ;; Replacing matches
 
-(defun proof-replace-string (string to-string)
+(defsubst proof-replace-string (string to-string)
   "Non-interactive `replace-string', using `proof-case-fold-search'."
   (while (proof-search-forward string nil t)
     (replace-match to-string nil t)))
 
-(defun proof-replace-regexp (regexp to-string)
+(defsubst proof-replace-regexp (regexp to-string)
   "Non-interactive `replace-regexp', using `proof-case-fold-search'."
   (while (proof-re-search-forward regexp nil t)
     (replace-match to-string nil nil)))
 
-(defun proof-replace-regexp-nocasefold (regexp to-string)
+(defsubst proof-replace-regexp-nocasefold (regexp to-string)
   "Non-interactive `replace-regexp', forcing `case-fold-search' to nil."
   (let ((case-fold-search nil))
     (while (proof-re-search-forward regexp nil t)
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 36333bce..b00ffa72 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -6,7 +6,6 @@
 ;;
 ;; $Id$
 ;;
-;; TODO (minor things):
 ;;
 ;; 1. edit-toolbar cannot edit proof toolbar (even in a proof mode)
 ;; Need a variable containing  a specifier or similar.
@@ -23,25 +22,14 @@
 ;; 3. We could consider automatically disabling buttons which are
 ;; not configured for the prover, e.g. if proof-info-command is
 ;; not set, then the Info button should not be shown. 
-
-
-;;; IMPORT declaration  (only to suppress warnings for byte compile)
-;;; NB: can't put require proof-script here: leads to circular
-;;; requirement via proof-menu.
-;; (require 'proof-script)
-;; (autoload 'proof-shell-live-buffer "proof-shell")
-;; (autoload 'proof-shell-restart "proof-shell")
-
-
-(require 'proof-config)			; for <PA>-toolbar-entries
-
 ;;
-;; See `proof-toolbar-entries-default' and
-;;     `<PA>-toolbar-entries' in proof-config
-;; for the default generic toolbar and 
+;; See `proof-toolbar-entries-default' and `<PA>-toolbar-entries' 
+;; in pg-custom for the default generic toolbar and 
 ;; the per-prover toolbar contents variable.
 ;;
 
+(eval-when-compile
+  (require 'proof-utils))
 ;;
 ;; Function, icon, button names
 ;; 
@@ -107,7 +95,7 @@
 		     (message "Button \"%s\" disabled" ,menuname))))
 	  buttonfnwe)))
     (if tooltip	;; no tooltip means menu-only item
-	(if proof-running-on-XEmacs
+	(if (featurep 'xemacs)
 	    (list (vector icon actualfn enableritem tooltip))
 	  (list (append (list icon actualfn token
 			      :help tooltip)
@@ -133,25 +121,24 @@ If `proof-toolbar-enable' is nil, change the current buffer toolbar
 to the default toolbar."
   (interactive)
   (if
-   (and ;; Check toolbar support in Emacs
+   (and ;; Check toolbar support...
+    window-system
     (or (and (featurep 'tool-bar)	; GNU Emacs tool-bar library
-	     (member 'xpm image-types))	; and XPM support
+	     (or (image-type-available-p 'xpm)   ;; and XPM
+		 (image-type-available-p 'png))) ;; or PNG
 	(and (featurep 'toolbar)	; or XEmacs toolbar library
-	     (featurep 'xpm)))		; and XPM support
-    ;; Check we're running in a windowing system
-    (pg-window-system))
+	     (featurep 'xpm))))		; and XPM support
 
       ;; Toolbar support is possible.  
       (progn
 	;; Check the toolbar has been built.
 	(or proof-toolbar (proof-toolbar-build))
 
-	;; Now see if user wants toolbar
-	;; or not (this can be changed dyamically).
+	;; Now see if user wants toolbar (this can be changed dyamically).
 	(if proof-toolbar-enable
 
 	    ;; Enable the toolbar in this buffer
-	    (if proof-running-on-Emacs21
+	    (if (not (featurep 'xemacs))
 		;; For GNU Emacs, we make a local tool-bar-map
 		(set (make-local-variable 'tool-bar-map) proof-toolbar)
 	      
@@ -161,7 +148,7 @@ to the default toolbar."
 	      (proof-toolbar-setup-refresh))
 
 	  ;; Disable the toolbar in this buffer
-	  (if proof-running-on-Emacs21
+	  (if (not (featurep 'xemacs))
 	      ;; For GNU Emacs, we remove local value of tool-bar-map
 	      (kill-local-variable 'tool-bar-map)
 	    ;; For XEmacs, we remove specifier and disable refresh.
@@ -193,7 +180,7 @@ to the default toolbar."
 	(append
 	 (apply 'append (mapcar 'proof-toolbar-make-toolbar-item 
 				(proof-ass toolbar-entries)))
-	 (if proof-running-on-XEmacs
+	 (if (featurep 'xemacs)
 	     (list [:style 3d])))))
 
     ;; First set the button variables to glyphs (bit long-windedly).  
@@ -206,7 +193,7 @@ to the default toolbar."
 				name
 				icontype)) (cdr buttons))))
 	 (set var 
-	      (if proof-running-on-XEmacs
+	      (if (featurep 'xemacs)
 		  ;; On XEmacs, icon variable holds a list of glyphs
 		  (toolbar-make-button-list iconfiles)
 		;; On GNU Emacs, it holds a filename for the icon,
@@ -215,7 +202,7 @@ to the default toolbar."
 		(concat "epg-" (eval (cadr buttons)))))))
      proof-toolbar-icon-list)
 
-    (if proof-running-on-XEmacs
+    (if (featurep 'xemacs)
 	;; For XEmacs, we evaluate the specifier.
 	(setq proof-toolbar (mapcar 'eval proof-toolbar-button-list))
 
@@ -237,6 +224,8 @@ to the default toolbar."
 
 ;; Action to take after altering proof-toolbar-enable
 (defalias 'proof-toolbar-enable 'proof-toolbar-setup)
+
+;;;###autoload (autoload 'proof-toolbar-toggle "proof-toolbar")
 (proof-deftoggle proof-toolbar-enable proof-toolbar-toggle)
 
 
@@ -558,14 +547,16 @@ changed state."
 	    (list menuname fnval)
 	    (if enablep 
 		(list ':active (list (proof-toolbar-enabler token))))))))))
-   
-(defconst proof-toolbar-scripting-menu
-  ;; Toolbar contains commands to manipulate script and
-  ;; other handy stuff.  
+
+;;;###autoload
+(defun proof-toolbar-scripting-menu ()
+  "Menu made from the Proof General toolbar commands."
+  ;; Prevent evaluation too early here, otherwise this is called
+  ;; during compilation when loading files with expanded easy-menu-define
+  ;; (e.g. pg-response/proof-aux-menu call)
   (apply 'append
-	  (mapcar 'proof-toolbar-make-menu-item 
-		  (proof-ass toolbar-entries)))
-  "Menu made from the Proof General toolbar commands.")
+	 (mapcar 'proof-toolbar-make-menu-item 
+		 (proof-ass toolbar-entries))))
 
  
 ;; 
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 1cb372fb..89f0b433 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -1,21 +1,29 @@
-;; proof-utils.el   Proof General utility functions
+;; proof-utils.el --- Proof General utility functions and macros
 ;;
-;; Copyright (C) 1998-2002 LFCS Edinburgh. 
+;; Copyright (C) 1998-2002 LFCS Edinburgh.
 ;; Author:      David Aspinall <David.Aspinall@ed.ac.uk> and others
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
-;;
+;;; Commentary:
+;; 
 ;; Loading note: this file is required immediately from proof.el, so
-;; no autoloads are used here.
+;; no autoloads cookies are added here. To expand macros during
+;; compilation, use (eval-when-compile (require 'proof-utils)).  
+;; This needs care: it is safe for e.g., deflocal, but not for
+;; macros which evaluate proof-assistant symbol, e.g. proof-ass,
+;; unless proof-ready-for-assistant has been run.
+;;
 
-(require 'proof-compat)			;; for pg-defface-window-systems
+(require 'proof-site)			; basic vars
+(require 'proof-compat)		        ; for pg-defface-window-systems
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Handy macros
 
+;;; Code:
 (defmacro deflocal (var value &optional docstring)
   "Define a buffer local variable VAR with default value VALUE."
  `(progn
@@ -29,6 +37,9 @@
        (with-current-buffer ,buf
 	 ,@body)))
 
+(deflocal proof-buffer-type nil
+  "Symbol for the type of this buffer: 'script, 'shell, 'goals, or 'response.")
+
 ;; Slightly specialized version of above.  This is used in commands
 ;; which work from different PG buffers (goals, response), typically
 ;; bound to toolbar commands.
@@ -53,29 +64,13 @@ Return nil if not a script buffer or if no active scripting buffer."
  `(intern (concat (symbol-name proof-assistant-symbol) "-" ,string)))
 
 
-(defun proof-try-require (symbol)
+(defsubst proof-try-require (symbol)
   "Try requiring SYMBOL.  No error if the file for SYMBOL isn't found."
   (condition-case ()
       (require symbol)
     (file-error nil))
   (featurep symbol))
 
-(defmacro proof-face-specs (bl bd ow)
-  "Return a spec for `defface' with BL for light bg, BD for dark, OW o/w."
-  `(append
-    (apply 'append
-     (mapcar 
-     (lambda (ty) (list
-		     (list (list (list 'type ty) '(class color)
-			   (list 'background 'light))
-			   (quote ,bl))
-		     (list (list (list 'type ty) '(class color)
-				 (list 'background 'dark))
-			   (quote ,bd))))
-     ;; NOTE: see proof-compat.el for possible window-system values
-     pg-defface-window-systems))
-    (list (list t (quote ,ow)))))
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -102,39 +97,6 @@ Return nil if not a script buffer or if no active scripting buffer."
    buffers))
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Function for taking action when dynamically adjusting customize values
-;;
-(defun proof-set-value (sym value)
-  "Set a customize variable using set-default and a function.
-We first call `set-default' to set SYM to VALUE.
-Then if there is a function SYM (i.e. with the same name as the
-variable SYM), it is called to take some dynamic action for the new
-setting.  
-
-If there is no function SYM, we try stripping 
-proof-assistant-symbol and adding \"proof-\" instead to get
-a function name.  This extends proof-set-value to work with
-generic individual settings.
-
-The dynamic action call only happens when values *change*: as an
-approximation we test whether proof-config is fully-loaded yet."
-  (set-default sym value)
-  (if (featurep 'proof-config)
-      (if (fboundp sym)
-	  (funcall sym)
-	(if (> (length (symbol-name sym)) 
-	       (+ 3 (length (symbol-name proof-assistant-symbol))))
-	    (let ((generic  
-		   (intern
-		    (concat "proof"
-			    (substring (symbol-name sym)
-				       (length (symbol-name
-						proof-assistant-symbol)))))))
-	      (if (fboundp generic)
-		  (funcall generic)))))))
-
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -154,7 +116,7 @@ approximation we test whether proof-config is fully-loaded yet."
 ;; previous approach.  It is also a big change to move all settings.
 ;;
 ;; NB: this mechanism is work in progress in 3.2.  It will
-;; be expanded, although we may leave most low-level 
+;; be expanded, although we may leave most low-level
 ;; settings to use the current mechanism.
 ;;
 ;; Notes:
@@ -163,40 +125,43 @@ approximation we test whether proof-config is fully-loaded yet."
 ;;
 ;; (proof-ass name)   or (proof-assistant-name)
 ;;
-;; Later is more efficient, though defining function
-;; for each setting seems wasteful?
-
-(defun proof-ass-symv (sym)
-  "Return the symbol for SYM for the current prover.  SYM is evaluated."
-  (intern (concat (symbol-name proof-assistant-symbol) "-" 
-		  (symbol-name sym))))
 
 (defmacro proof-ass-sym (sym)
-  "Return the symbol for SYM for the current prover.  SYM not evaluated."
-  `(proof-ass-symv (quote ,sym)))
+  "Return the symbol for SYM for the current prover.  SYM not evaluated.
+This macro should only be called once a specific prover is known."
+  `(intern (concat (symbol-name proof-assistant-symbol) "-"
+		   (symbol-name ',sym))))
+
+(defmacro proof-ass-symv (sym)
+  "Return the symbol for SYM for the current prover.  SYM evaluated.
+This macro should only be invoked once a specific prover is engaged."
+  `(intern (concat (symbol-name proof-assistant-symbol) "-"
+		   (symbol-name ,sym))))
+
+(defmacro proof-ass (sym)
+  "Return the value for SYM for the current prover.
+This macro should only be invoked once a specific prover is engaged."
+  `(symbol-value (intern (concat (symbol-name proof-assistant-symbol) "-"
+				 (symbol-name ',sym)))))
 
 (defun proof-defpgcustom-fn (sym args)
-  "Define a new customization variable <PA>-sym for the current proof assistant.
+  "Define a new customization variable <PA>-sym for current proof assistant.
 Helper for macro `defpgcustom'."
   (let ((specific-var (proof-ass-symv sym))
-	(generic-var  (intern (concat "proof-assistant-" (symbol-name sym)))))
+	 (generic-var  (intern (concat "proof-assistant-" (symbol-name sym)))))
     (eval
-     `(defcustom ,specific-var 
-	,@args
-	;; FIXME: would be nicer to grab group from @args here and
-	;; prefix it automatically.  For now, default to internals
-	;; setting for PA.
-	;; FIXME 2: would also be nice to grab docstring from args
-	;; and allow substitution for prover name, etc.  A bit too 
-	;; fancy perhaps!
-	:group ,(quote proof-assistant-internals-cusgrp)))
+     `(defcustom ,specific-var
+       ,@args
+       ;; We could grab :group from @args and prefix it.
+       :group ,(quote proof-assistant-internals-cusgrp)))
     ;; For functions, we could simply use defalias.  Unfortunately there
     ;; 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) " for current proof assistant.
+     `(defun ,generic-var (&optional newval)
+	,(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 
+	(if newval
 	    (setq ,specific-var newval)
 	  ,specific-var)))))
 
@@ -208,24 +173,21 @@ If NEWVAL is present, set the variable, otherwise return its current value.")
 
 (defmacro defpgcustom (sym &rest args)
   "Define a new customization variable <PA>-SYM for the current proof assistant.
-The function proof-assistant-<SYM> is also defined, which can be used in the 
+The function proof-assistant-<SYM> is also defined, which can be used in the
 generic portion of Proof General to set and retrieve the value for the current p.a.
 Arguments as for `defcustom', which see.
 
 Usage: (defpgcustom SYM &rest ARGS)."
   `(proof-defpgcustom-fn (quote ,sym) (quote ,args)))
 
-(defmacro proof-ass (sym)
-  "Return the value for SYM for the current prover."
-  ;; (eval `(proof-ass-sym ,sym))
-  `(symbol-value (proof-ass-symv ',sym))) ;; [Stefan Monnier]
+
 
 (defun proof-defpgdefault-fn (sym value)
   "Helper for `defpgdefault', which see.  SYM and VALUE are evaluated."
   ;; NB: we need this because nothing in customize library seems to do
   ;; the right thing.
   (let ((symbol  (proof-ass-symv sym)))
-    (set-default symbol 
+    (set-default symbol
 		 (cond
 		  ;; Use saved value if it's set
 		  ((get symbol 'saved-value)
@@ -250,10 +212,18 @@ Usage: (defpgdefault SYM VALUE)"
   `(defun ,(proof-ass-symv name) ,arglist
      ,@args))
 
-
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; End macros
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; 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))))
+    
+
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -285,7 +255,7 @@ Usage: (defpgdefault SYM VALUE)"
 (defun proof-buffers-in-mode (mode &optional buflist)
   "Return a list of the buffers in the buffer list in major-mode MODE.
 Restrict to BUFLIST if it's set."
-  (let ((bufs-left (or buflist (buffer-list))) 
+  (let ((bufs-left (or buflist (buffer-list)))
 	bufs-got)
     (dolist (buf bufs-left bufs-got)
       (if (with-current-buffer buf (eq mode major-mode))
@@ -299,7 +269,7 @@ Restrict to BUFLIST if it's set."
 (defun pg-save-from-death ()
   "Prevent this associated buffer from being killed: merely erase it.
 A hook function for `kill-buffer-hook'.
-This is a fairly crude and not-entirely-robust way to prevent the 
+This is a fairly crude and not-entirely-robust way to prevent the
 user accidently killing an associated buffer."
   (if (and (proof-shell-live-buffer) proof-buffer-type)
       (progn
@@ -332,10 +302,10 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
 
 ;; Notes:
 ;;
-;; * Various mechanisms for setting defaults, different between 
+;; * Various mechanisms for setting defaults, different between
 ;;   Emacsen.  Old method(?) was to set "blah-mode-font-lock-keywords"
 ;;   and copy it into "font-lock-keywords" to engage font-lock.
-;;   Present method for XEmacs is to put a 'font-lock-defaults 
+;;   Present method for XEmacs is to put a 'font-lock-defaults
 ;;   property on the major-mode symbol, or use font-lock-defaults
 ;;   buffer local variable.  We use the latter.
 ;;
@@ -391,14 +361,14 @@ font-lock-mode."
     ;; 11.12.01: Emacs 21 is very eager about turning on font
     ;; lock and has hooks all over the place to do it.  To make
     ;; sure it doesn't happen we have to eradicate all sense of
-    ;; having any fontification ability.  
+    ;; having any fontification ability.
     (proof-font-lock-clear-font-lock-vars)
     ;; In fact, this still leaves font-lock switched on! But
     ;; hopefully in a useless way.  XEmacs has better control
     ;; over which modes not to enable it for (although annoying
     ;; that it's a custom setting)
-    (if proof-running-on-XEmacs
-	(setq font-lock-mode-disable-list 
+    (if (featurep 'xemacs)
+	(setq font-lock-mode-disable-list
 	      (cons major-mode font-lock-mode-disable-list)))))
 
 (defun proof-font-lock-clear-font-lock-vars ()
@@ -413,9 +383,9 @@ font-lock-mode."
   )
 
 (defun proof-font-lock-set-font-lock-vars ()
-  (setq font-lock-defaults 
-	`(proof-font-lock-keywords 
-	  nil 
+  (setq font-lock-defaults
+	`(proof-font-lock-keywords
+	  nil
 	  ,proof-font-lock-keywords-case-fold-search))
   (setq font-lock-keywords proof-font-lock-keywords))
 
@@ -442,10 +412,10 @@ Returns new END value."
 	(proof-font-lock-set-font-lock-vars)
 
 	;; Yukky hacks to immorally interface with font-lock
-	(unless proof-running-on-XEmacs
+	(unless (featurep 'xemacs)
 	  (font-lock-set-defaults))
 	(let ((font-lock-keywords proof-font-lock-keywords))
-	  (if (and proof-running-on-XEmacs
+	  (if (and (featurep 'xemacs)
 		   (>= emacs-major-version 21)
 		   (>= emacs-minor-version 4)
 		   (not font-lock-cache-position))
@@ -481,7 +451,7 @@ Returns new END value."
   "Remove special characters in region.  Default to whole buffer.
 Leave point at END."
   (save-restriction
-    (if (and start end) 
+    (if (and start end)
 	(narrow-to-region start end))
     (goto-char (or start (point-min)))
     (while (re-search-forward pg-special-char-regexp end t)
@@ -518,7 +488,7 @@ NB: may change the selected window."
   ;; IF there *isn't* a visible window showing buffer...
   (unless (get-buffer-window buffer 0)
     ;; THEN find somewhere nice to display it
-	  (if (and 
+	  (if (and
 	     ;; If we're in two-window mode and already displaying a
 	     ;; script/response/goals, try to just switch the buffer
 	     ;; instead of calling display-buffer which alters sizes.
@@ -530,18 +500,18 @@ NB: may change the selected window."
 		   ;; NB: 3.5: added rest of assoc'd buffers here
 		   (cons proof-script-buffer (proof-associated-buffers))))
 	    (if (eq (selected-window) (minibuffer-window))
-		;; 17.8.01: avoid switching the minibuffer's contents 
+		;; 17.8.01: avoid switching the minibuffer's contents
 		;; -- terrrible confusion -- use next-window after
 		;; script buffer instead.
 		;; (another hack which is mostly right)
-		(set-window-buffer 
-		 (next-window 
+		(set-window-buffer
+		 (next-window
 		  (car-safe (get-buffer-window-list proof-script-buffer))
 		  'ignoreminibuf) buffer)
 	      (if (eq (window-buffer (next-window nil 'ignoreminibuf))
-		      proof-script-buffer) 
+		      proof-script-buffer)
 		  ;; switch this window
-		  (set-window-buffer (selected-window) buffer) 
+		  (set-window-buffer (selected-window) buffer)
 		;; switch other window
 		(set-window-buffer (next-window nil 'ignoreminibuf) buffer)))
 	    ;; o/w: call display buffer to configure windows nicely.
@@ -565,7 +535,7 @@ NB: may change the selected window."
 
 (defun proof-display-and-keep-buffer (buffer &optional pos)
   "Display BUFFER and make window according to display mode.
-If optional POS is present, will set point to POS.  
+If optional POS is present, will set point to POS.
 Otherwise move point to the end of the buffer.
 Ensure that point is visible in window."
   (save-excursion
@@ -648,7 +618,7 @@ If proof-general-debug is nil, do nothing."
   "Switch to or display buffer BUF in other window unless already displayed.
 If optional arg NOSELECT is true, don't switch, only display it.
 No action if BUF is nil or killed."
-  ;; Maybe this needs to be more sophisticated, using 
+  ;; Maybe this needs to be more sophisticated, using
   ;; proof-display-and-keep-buffer ?
   (and (buffer-live-p buf)
        (unless (eq buf (window-buffer (selected-window)))
@@ -667,11 +637,11 @@ No action if BUF is nil or killed."
 ;; Originally based on `shrink-window-if-larger-than-buffer', which
 ;; has a pretty wierd implementation.
 ;; TODO: desirable improvements would be to add some crafty history based
-;; on user resize-events.  E.g. user resizes window, that becomes the 
+;; on user resize-events.  E.g. user resizes window, that becomes the
 ;; new maximum size.
 ;; FIXME: GNU Emacs has useful "window-size-fixed" which we use
 ;; HOWEVER, it's still not quite the right thing, it seems to me.
-;; We'd like to specifiy a *minimum size* for a given buffer, 
+;; We'd like to specifiy a *minimum size* for a given buffer,
 ;; not a maximum.  With a frame split with just goals/response
 ;; we'd still get resize errors here using window-size-fixed.
 ;; FIXME: shrink-to-fit doesn't really work in three-buffer mode,
@@ -782,12 +752,12 @@ or if the window is the only window of its frame."
   (interactive)
   (require 'reporter)
   (let
-      ((reporter-prompt-for-summary-p 
+      ((reporter-prompt-for-summary-p
 	"(Very) brief summary of problem or suggestion: "))
     (reporter-submit-bug-report
      "da+pg-bugs@inf.ed.ac.uk"
-     "Proof General" 
-     (list 'proof-general-version 'proof-assistant 
+     "Proof General"
+     (list 'proof-general-version 'proof-assistant
 	   'x-symbol-version)
      nil nil
      "*** Proof General now uses Trac for project management and bug reporting, please go to:
@@ -798,13 +768,13 @@ or if the window is the only window of its frame."
 *** To report a bug, either register yourself as a user, or use the generic account
 *** username \"pgemacs\" with password \"pgemacs\"
 ***
-*** Please only continue with this email mechanism instead IF YOU REALLY MUST.  
-*** The address is not monitored very often and quite possibly will be ignored.  
+*** Please only continue with this email mechanism instead IF YOU REALLY MUST.
+*** The address is not monitored very often and quite possibly will be ignored.
 ***
 *** When reporting a bug, please include a small test case for us to repeat it.
 *** Please also check that it is not already covered in the BUGS or FAQ files that came with
-*** the distribution, or the latest versions at 
-***    http://proofgeneral.inf.ed.ac.uk/BUGS  and 
+*** the distribution, or the latest versions at
+***    http://proofgeneral.inf.ed.ac.uk/BUGS  and
 ***    http://proofgeneral.inf.ed.ac.uk/FAQ ")))
 
 
@@ -817,13 +787,13 @@ or if the window is the only window of its frame."
   "Define a function <VAR>-toggle for toggling a boolean customize setting VAR.
 Args as for the macro `proof-deftoggle', except will be evaluated."
   (eval
-   `(defun ,(if othername othername 
+   `(defun ,(if othername othername
 	      (intern (concat (symbol-name var) "-toggle"))) (arg)
 	      ,(concat "Toggle `" (symbol-name var) "'. With ARG, turn on iff ARG>0.
 This function simply uses customize-set-variable to set the variable.
 It was constructed with `proof-deftoggle-fn'.")
 	      (interactive "P")
-	      (customize-set-variable 
+	      (customize-set-variable
 	       (quote ,var)
 	       (if (null arg) (not ,var)
 		 (> (prefix-numeric-value arg) 0))))))
@@ -839,14 +809,14 @@ The name of the defined function is returned."
   "Define a function <VAR>-intset for setting an integer customize setting VAR.
 Args as for the macro `proof-defintset', except will be evaluated."
   (eval
-   `(defun ,(if othername othername 
+   `(defun ,(if othername othername
 	      (intern (concat (symbol-name var) "-intset"))) (arg)
 	      ,(concat "Set `" (symbol-name var) "' to ARG.
 This function simply uses customize-set-variable to set the variable.
 It was constructed with `proof-defintset-fn'.")
-	      (interactive (list 
-			    (read-number 
-			     (format "Value for %s (int, currently %s): " 
+	      (interactive (list
+			    (read-number
+			     (format "Value for %s (int, currently %s): "
 				     (symbol-name (quote ,var))
 				     (symbol-value (quote ,var))))))
 	      (customize-set-variable (quote ,var) arg))))
@@ -862,7 +832,7 @@ The name of the defined function is returned."
   "Define a function <VAR>-toggle for setting an integer customize setting VAR.
 Args as for the macro `proof-defstringset', except will be evaluated."
   (eval
-   `(defun ,(if othername othername 
+   `(defun ,(if othername othername
 	      (intern (concat (symbol-name var) "-stringset"))) (arg)
 	      ,(concat "Set `" (symbol-name var) "' to ARG.
 This function simply uses customize-set-variable to set the variable.
@@ -881,6 +851,49 @@ The name of the defined function is returned."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
+;;; Macris for defining user-level functions (previously in proof-menu.el)
+;;;
+
+
+(defmacro proof-defshortcut (fn string &optional key)
+  "Define shortcut function FN to insert STRING, optional keydef KEY.
+This is intended for defining proof assistant specific functions.
+STRING is inserted using `proof-insert', which see.
+KEY is added onto proof-assistant map."
+  `(progn
+     (if ,key
+	 (define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
+     (defun ,fn ()
+       ,(concat "Shortcut command to insert "
+		(replace-in-string  string "\\\\" "\\\\=") ;; for substitute-command-keys
+		" into the current buffer.\nThis simply calls `proof-insert', which see.")
+       (interactive)
+       (proof-insert ,string))))
+
+(defmacro proof-definvisible (fn string &optional key)
+  "Define function FN to send STRING to proof assistant, optional keydef KEY.
+This is intended for defining proof assistant specific functions.
+STRING is sent using proof-shell-invisible-command, which see.
+STRING may be a string or a function which returns a string.
+KEY is added onto proof-assistant map."
+  `(progn
+     (if ,key
+	 (define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
+     (defun ,fn ()
+       ,(concat "Command to send "
+		(if (stringp string)
+		    (replace-in-string
+		     string "\\\\" "\\\\=") ;; for substitute-command-keys
+		  "an instruction")
+		" to the proof assistant.")
+       (interactive)
+       ,(if (stringp string)
+	    (list 'proof-shell-invisible-command string)
+	  (list 'proof-shell-invisible-command (eval string))))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
 ;;; Interface to custom lib
 ;;;
 
@@ -889,8 +902,8 @@ The name of the defined function is returned."
   "Save custom vars VARIABLES."
   (dolist (symbol variables)
     (let ((value (get symbol 'customized-value)))
-      ;; This code from customize-save-customized adjusts 
-      ;; properties so that custom-save-all will save 
+      ;; This code from customize-save-customized adjusts
+      ;; properties so that custom-save-all will save
       ;; the value.
       (when value
 	(put symbol 'saved-value value)
@@ -901,7 +914,7 @@ The name of the defined function is returned."
 
 ;; FIXME: this doesn't do quite same thing as reset button,
 ;; which *removes* a setting from `custom-set-variables' list
-;; in custom.el.  Instead, this adds something to a 
+;; in custom.el.  Instead, this adds something to a
 ;; custom-reset-variables list.
 (defun pg-custom-reset-vars (&rest variables)
   "Reset custom vars VARIABLES to their default values."
@@ -920,7 +933,7 @@ The name of the defined function is returned."
   "Search for PROGNAME on PATH.  Return the full path to PROGNAME, or nil.
 If RETURNNOPATH is non-nil, return PROGNAME even if we can't find a full path.
 EXTRAPATH is a list of extra path components"
-  (or 
+  (or
    (cond
     ((fboundp 'executable-find)
      (let ((exec-path (append exec-path extrapath)))
@@ -932,44 +945,5 @@ EXTRAPATH is a list of extra path components"
 		  1)))
    (if returnnopath progname)))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Stuff for developing PG, not needed for ordinary users really.
-;; [Could consider moving this to a new file `proof-devel.el']
-;;
-
-(put 'proof-if-setting-configured 'lisp-indent-function 1)
-(put 'proof-define-assistant-command 'lisp-indent-function 'defun)
-(put 'proof-define-assistant-command-witharg 'lisp-indent-function 'defun)
-(put 'defpgcustom 'lisp-indent-function 'defun)
-(put 'proof-map-buffers 'lisp-indent-function 'defun)
-(put 'proof-with-current-buffer-if-exists 'lisp-indent-function 'defun)
-
-(defconst proof-extra-fls
-  (list
-   (list "^(\\(proof-def\\"
-	 ;; Variable like things
-	 "\\(asscustom)\\|"
-	 ;; Function like things
-	 "\\([^ \t\n\(\)]+\\)"
-	 ;; Any whitespace and declared object.
-	 "[ \t'\(]*"
-	 "\\([^ \t\n\)]+\\)?")
-   '(1 font-lock-keyword-face)
-   '(8 (cond ((match-beginning 3) 'font-lock-variable-name-face)
-	     ;; ((match-beginning 6) 'font-lock-type-face)
-	     (t 'font-lock-function-name-face))
-       nil t)))
-
-;; This doesn't work for FSF's font lock, developers should use
-;; XEmacs!  (unless edebug is broken, which it is in my 21.4.12)
-(if (boundp 'lisp-font-lock-keywords)	; compatibility hack
-    (setq lisp-font-lock-keywords 
-	  (append proof-extra-fls
-		  lisp-font-lock-keywords)))
-       
-(setq autoload-package-name "proof")
-(setq generated-autoload-file "proof-autoloads.el")
-	
-;; End of proof-utils.el
 (provide 'proof-utils)
+;;; proof-utils.el ends here
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index faec0e49..47246fd6 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -47,12 +47,8 @@
 ;; -- Is it possible to remove setting of language in x-symbol-enable?
 ;; -- Simplify proof-x-symbol-initialize
 
-(require 'proof-site)			; for proof-assistant-symbol
-
-(defpgcustom x-symbol-language proof-assistant-symbol
-  "Setting for x-symbol-language for the current proof assistant.
-It defaults to proof-assistant-symbol, which makes X Symbol
-look for files named x-symbol-<PA>.el.")
+(eval-when-compile
+  (require 'proof-utils))	 ; proof-eval-when-ready-for-assistant
 
 (defvar proof-x-symbol-initialized nil
   "Non-nil if x-symbol support has been initialized.")
@@ -67,7 +63,7 @@ look for files named x-symbol-<PA>.el.")
   "A test to see whether x-symbol support may be available."
   (and
    (or (featurep 'x-symbol-hooks)
-       (and (pg-window-system)		; Not on a tty
+       (and window-system
 	    (progn
 	      ;; put bundled version on load path
 	      (setq load-path
@@ -87,8 +83,8 @@ look for files named x-symbol-<PA>.el.")
   "Initialize x-symbol support for Proof General, if possible.
 If ERROR is non-nil, give error on failure, otherwise a warning."
   (interactive)
-  (unless (or proof-x-symbol-initialized ;; already done
-	      ;; or can't be done
+  (unless (or proof-x-symbol-initialized   ; already done
+	      (not proof-assistant-symbol) ; too early
 	      (not (proof-x-symbol-support-maybe-available)))
     (let*
 	((xs-lang        (proof-ass x-symbol-language))
@@ -107,7 +103,7 @@ If ERROR is non-nil, give error on failure, otherwise a warning."
 	(funcall error-or-warn
  "Proof General: x-symbol package must be installed for x-symbol-support!
 The package is available at http://x-symbol.sourceforge.net/"))
-       ((not (pg-window-system))
+       ((not window-system)
 	(funcall error-or-warn 
  "Proof General: x-symbol package only runs under a window system!"))
        ((or (not (fboundp 'x-symbol-initialize))
@@ -132,19 +128,11 @@ The package is available at http://x-symbol.sourceforge.net/"))
 	(require 'x-symbol-vars)  ;; [new requirement to require this]
 	(let*
 	    ((xs-xtra-modes  proof-xsym-extra-modes)
-	     (xs-std-modes   
-	      (list
-	       ;; NB: these variables are set in script/shell mode
-	       ;; initialization, maybe too late for here.  Backup:
-	       ;; default names, which everyone should follow.
-	       (or proof-mode-for-shell
-		   (intern (concat proof-assistant "-shell-mode")))
-	       (or proof-mode-for-response
-		   (intern (concat proof-assistant "-response-mode")))
-	       (or proof-mode-for-script
-		   (intern (concat proof-assistant "-mode")))
-	       (or  proof-mode-for-goals
-		    (intern (concat proof-assistant "-goals-mode")))))
+	     (xs-std-modes   (list
+			      proof-mode-for-shell
+			      proof-mode-for-response
+			      proof-mode-for-script
+			      proof-mode-for-goals))
 	     (all-xs-modes   (append xs-std-modes xs-xtra-modes))
 	     (am-entry       (list proof-xsym-extra-modes t 
 				   `(quote ,xs-lang)))
@@ -180,32 +168,29 @@ This invokes `x-symbol-mode' to toggle the setting for the current
 buffer, and then sets PG's option for default to match.
 Also we arrange to have X-Symbol mode turn itself on automatically 
 in future if we have just activated it for this buffer."
-;; Calls proof-x-symbol-toggle-clean-buffers afterwards.
-  (if (not proof-x-symbol-initialized) ;; Check inited
-      (progn
-	(set (proof-ass-sym x-symbol-enable) nil) ; assume failure!
-	(proof-x-symbol-initialize 'giveerrors)
-	(set (proof-ass-sym x-symbol-enable) t)))
-
-;; C RAFFALLI: we need to set x-symbol-language even for the script buffer
-;; and I think this is a good place ... may be a variable should control
-;; an option to have x-symbol only in the output buffer but not in the script
-;; buffer ?
-;;  (proof-x-symbol-set-language)
-;; DA: this is done already I believe, PhoX used a funny startup perhaps.
-
-  (x-symbol-mode)
-  (proof-x-symbol-mode-associated-buffers))
+  (if (proof-ass-sym x-symbol-enable) 
+      ;; We're trying to initialise it
+      (if (not proof-x-symbol-initialized) ;; Check inited
+	  (progn
+	    (set (proof-ass-sym x-symbol-enable) nil) ; assume failure!
+	    (proof-x-symbol-initialize 'giveerrors)
+	    (set (proof-ass-sym x-symbol-enable) t))))
 
+  (if proof-x-symbol-initialized
+      (if (fboundp 'x-symbol-mode)
+	  (progn
+	    (x-symbol-mode)
+	    (proof-x-symbol-mode-associated-buffers)))))
+  
 ;; Old behaviour for proof-x-symbol-enable was to update state in all
 ;; buffers --- but this can take ages if there are many buffers!  
-;; We also used to refresh the output, but this doesn't always work.
+;; Refreshing output buffers also causes glitches
 ;; (proof-x-symbol-mode-all-buffers)
 ;; (proof-x-symbol-refresh-output-buffers))
 
 
 (defun proof-x-symbol-refresh-output-buffers ()
-  ;; FIXME: this isn't used.  Might be nice to do so again, turning
+  ;; NB: this isn't used.  Might be nice to do so again, turning
   ;; off X-Sym can leave junk displayed.  OTOH, sending messages to PA
   ;; can give errors, because there is no generic "refresh" or
   ;; "repeat" option.  (Isar: gives errors outside proof mode).
@@ -214,7 +199,7 @@ in future if we have just activated it for this buffer."
 This function is intended to clean the display after a change
 in the status of X-Symbol display.
 This is a subroutine of proof-x-symbol-enable."
-  (proof-shell-maybe-erase-response nil t t)
+  (pg-response-maybe-erase nil t t)
   (if (and proof-showproof-command (proof-shell-available-p))
     (proof-shell-invisible-command proof-showproof-command)))
 
@@ -347,14 +332,6 @@ Assumes that the current buffer is the proof shell buffer."
   ;     (x-symbol-encode))))
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Initialize x-symbol-support on load-up if user has asked for it
-;;
-;; FIXME: this initialization seems to result in x-symbol-language not
-;; being set properly.  We let this be called on demand instead.
-;(if (proof-ass x-symbol-enable) 
-;      (proof-x-symbol-initialize))
 
 (provide 'proof-x-symbol)
 ;; End of proof-x-symbol.el
diff --git a/generic/proof.el b/generic/proof.el
index d30dbaf5..3187f32c 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,147 +1,32 @@
-;; proof.el	 Proof General loader.  All files require this one.
+;;; proof.el --- Proof General loader.  
 ;;
-;; Copyright (C) 1998-2002 LFCS Edinburgh. 
+;; Copyright (C) 1998-2008 LFCS Edinburgh.
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
-
-(require 'proof-site)			; site config
+;;; Commentary:
+;; 
+;; This file loads Proof General.  It is required by the
+;; individual prover modes.  Loading order of PG is:
+;;
+;; 1. proof-site (autoloads & stubs for mode functions)
+;; 2. autoload of <PA>/<PA>.el by auto-mode-alist 
+;; 3. <PA>.el requires this file
+;; 4. rest of PG loaded here, inc proof-config/pg-custom
+;; 5. further modules loaded by autoloads.
+;; 
+;;; Code:
+
+(require 'proof-site)			; site/prover config, global vars
+(require 'proof-autoloads)		; autoloaded functions
 (require 'proof-compat)			; Emacs and OS compatibility
 (require 'proof-utils)			; utilities
 (require 'proof-config)			; configuration variables
 
-
-(proof-splash-message)                  ; welcome the user now.
-
-;;;
-;;; Extra autoloads that aren't automatic 
-;;; (defined with define-derived-mode)
-;;;
-
-(autoload 'proof-mode "proof-script"
-  "Proof General major mode class for proof scripts.")
-
-(autoload 'proof-shell-mode "proof-shell"
-  "Proof General shell mode class for proof assistant processes")
-
-
-;;;
-;;; Global variables
-;;;
-
-(deflocal proof-buffer-type nil
-  "Symbol for the type of this buffer: 'script, 'shell, 'goals, or 'response.")
-
-(defvar proof-shell-busy nil
-  "A lock indicating that the proof shell is processing.
-When this is non-nil, proof-shell-ready-prover will give
-an error.")
-
-(defvar proof-included-files-list nil 
-  "List of files currently included in proof process.
-This list contains files in canonical truename format
-\(see `file-truename').
-
-Whenever a new file is being processed, it gets added to this list
-via the proof-shell-process-file configuration settings.
-When the prover retracts a file, this list is resynchronised via the
-proof-shell-retract-files-regexp and proof-shell-compute-new-files-list 
-configuration settings.
-
-Only files which have been *fully* processed should be included here.
-Proof General itself will automatically add the filenames of a script
-buffer which has been completely read when scripting is deactivated.
-It will automatically remove the filename of a script buffer which
-is completely unread when scripting is deactivated.
-
-NB: Currently there is no generic provision for removing files which
-are only partly read-in due to an error, so ideally the proof assistant
-should only output a processed message when a file has been successfully
-read.")
-
-
-(defvar proof-script-buffer nil
-  "The currently active scripting buffer or nil if none.")
-
-;; FIXME: should fixup Coq's multiple file mode
-(defvar proof-previous-script-buffer nil
-  "Previous value of proof-script-buffer, recorded when scripting turned off.
-At the moment, this is only used for Coq's ugly multiple file code,
-to help guess the directory of files Coq says it's reinterning.")
-
-(defvar proof-shell-buffer nil
-  "Process buffer where the proof assistant is run.")
-
-(defvar proof-goals-buffer nil
-  "The goals buffer.")
-
-(defvar proof-response-buffer nil
-  "The response buffer.")
-
-(defvar proof-trace-buffer nil
-  "A tracing buffer for storing tracing output from the proof shell.
-See `proof-shell-trace-output-regexp' for details.")
-
-(defvar proof-thms-buffer nil
-  "A buffer for displaying a list of theorems from the proof assistant.
-See `proof-shell-thm-display-regexp' for details.")
-
-(defvar proof-shell-error-or-interrupt-seen nil
-  "Flag indicating that an error or interrupt has just occurred.
-Set to 'error or 'interrupt if one was observed from the proof 
-assistant during the last group of commands.")
-
-(defvar proof-shell-proof-completed nil
-  "Flag indicating that a completed proof has just been observed.
-If non-nil, the value counts the commands from the last command
-of the proof (starting from 1).")
-
-;; FIXME da: remove proof-terminal-string.  At the moment some
-;; commands need to have the terminal string, some don't.
-;; It's used variously in proof-script and proof-shell, which
-;; is another mess.  [Shell mode implicitly assumes script mode
-;; has been configured].
-;; We should assume commands are terminated at the specific level.
-
-(defvar proof-terminal-string nil
-  "End-of-line string for proof process.")
-
-;;;
-;;; Load other Proof General libraries
-;;;
-
-;(require 'proof-system) ; PC: buggy for now David please fix this.
-
-
-;;;
-;;; Unload utility (not wholly successful)
-;;;
-
-(defun unload-pg ()
-  (interactive)
-  (mapcar 
-   (lambda (feat) (condition-case nil
-		    (unload-feature feat 'force)
-		    (error nil)))
-   '(proof-splash pg-assoc pg-xml proof-depends proof-indent proof-site
-     proof-shell pg-metadata proof-menu pg-pbrpm pg-pgip proof-script
-     proof-autoloads pg-response pg-goals pg-pgip-old proof-toolbar
-     proof-easy-config proof-config proof-mmm proof pg-xhtml
-     proof-utils proof-syntax proof-system _pkg pg-user proof-x-symbol
-     pg-thymodes pg-autotest
-     ;; 
-     isar-syntax isar-find-theorems x-symbol-isar
-     isar-autotest interface-setup isabelle-system isar isar-mmm
-     isar-keywords
-     ;;
-     coq-abbrev coq-db x-symbol-coq coq-local-vars coq coq-syntax
-     coq-indent coq-autotest)))
-
-     
-
+(proof-splash-message)			; welcome the user now.
 
 (provide 'proof)
-;; proof.el ends here
+;;; proof.el ends here