Refactor several variable names; clean up, doc subterm markup and output display.

19 files changed, 474 insertions, 356 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 80bcd83b..ca6a6009 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -566,7 +566,7 @@ This is specific to coq-mode."
 
   (setq proof-goal-command-p 'coq-goal-command-p
 	proof-find-and-forget-fn 'coq-find-and-forget
-        proof-goal-hyp-fn 'coq-goal-hyp
+        pg-topterm-goalhyp-fn 'coq-goal-hyp
 	proof-state-preserving-p 'coq-state-preserving-p)
 
   (setq proof-save-command-regexp coq-save-command-regexp
@@ -710,13 +710,13 @@ This is specific to coq-mode."
    proof-shell-error-regexp coq-error-regexp
    proof-shell-interrupt-regexp coq-interrupt-regexp
    proof-shell-assumption-regexp coq-id
-   proof-shell-first-special-char ?\360
+   pg-subterm-first-special-char ?\360
    proof-shell-wakeup-char ?\371 ; done: prompt
    ;; The next three represent path annotation information
-   proof-shell-start-char ?\372 ; not done
-   proof-shell-end-char ?\373 ; not done
-   proof-shell-field-char ?\374 ; not done
-   proof-shell-goal-char ?\375 ; done
+   pg-subterm-start-char ?\372 ; not done
+   pg-subterm-sep-char ?\373 ; not done
+   pg-subterm-end-char ?\374 ; not done
+   pg-topterm-char ?\375 ; done
    proof-shell-eager-annotation-start "\376\\|\\[Reinterning"
    proof-shell-eager-annotation-start-length 12
    proof-shell-eager-annotation-end "\377\\|done\\]" ; done
@@ -732,7 +732,7 @@ This is specific to coq-mode."
 	                 ; Coq has no global settings?
 			 ; (proof-assistant-settings-cmd))
    proof-shell-restart-cmd coq-shell-restart-cmd
-   proof-analyse-using-stack t)
+   pg-subterm-anns-use-stack t)
   
   (coq-init-syntax-table)
   (setq font-lock-keywords coq-font-lock-keywords-1)
@@ -740,8 +740,8 @@ This is specific to coq-mode."
   (proof-shell-config-done))
 
 (defun coq-goals-mode-config ()
-  (setq pbp-change-goal "Show %s. ")
-  (setq pbp-error-regexp coq-error-regexp)
+  (setq pg-goals-change-goal "Show %s. ")
+  (setq pg-goals-error-regexp coq-error-regexp)
   (coq-init-syntax-table)
   (setq font-lock-keywords coq-font-lock-keywords-1)
   (proof-goals-config-done))
diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index 1740a100..e9a3908d 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -135,7 +135,7 @@
 
 ;; The response buffer and goals buffer modes defined above are
 ;; trivial.  In fact, we don't need to define them at all -- they
-;; would simply default to "proof-response-mode" and "pbp-mode".
+;; would simply default to "proof-response-mode" and "pg-goals-mode".
 
 ;; A more sophisticated instantiation might set font-lock-keywords to
 ;; add highlighting, or some of the proof by pointing markup
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 7a90241f..65f7b76e 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1082,8 +1082,8 @@ This is only used in the implementation of @samp{@code{proof-generic-find-and-fo
 you only need to set if you use that function (by not customizing
 @samp{@code{proof-find-and-forget-fn}}.
 @end defvar
-@c TEXI DOCSTRING MAGIC: proof-goal-hyp-fn
-@defvar proof-goal-hyp-fn 
+@c TEXI DOCSTRING MAGIC: pg-topterm-goalhyp-fn
+@defvar pg-topterm-goalhyp-fn 
 Function which returns cons cell if point is at a goal/hypothesis.@*
 This is used to parse the proofstate output to mark it up for
 proof-by-pointing.  It should return a cons or nil.  First element of
@@ -1525,8 +1525,8 @@ communication with the prover process.
 A special character which terminates an annotated prompt.@*
 Set to nil if proof assistant does not support annotated prompts.
 @end defvar
-@c TEXI DOCSTRING MAGIC: proof-shell-first-special-char
-@defvar proof-shell-first-special-char 
+@c TEXI DOCSTRING MAGIC: pg-subterm-first-special-char
+@defvar pg-subterm-first-special-char 
 First special character.@*
 Codes above this character can have special meaning to Proof General,
 and are stripped from the prover's output strings.
@@ -1634,7 +1634,7 @@ A regular expression matching the name of assumptions.
 
 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 @samp{@code{proof-goal-hyp-fn}},
+In the future it will be used for a generic implementation for @samp{@code{pg-topterm-goalhyp-fn}},
 used to help parse the goals buffer to annotate it for proof by pointing.
 @end defvar
 
@@ -1912,22 +1912,22 @@ at how to use these settings.
 
 @c At the moment these settings are disabled.
 
-@c TEXI DOCSTRING MAGIC: pbp-change-goal
-@defvar pbp-change-goal 
+@c TEXI DOCSTRING MAGIC: pg-goals-change-goal
+@defvar pg-goals-change-goal 
 Command to change to the goal @samp{%s}
 @end defvar
 @c TEXI DOCSTRING MAGIC: pbp-goal-command
 @defvar pbp-goal-command 
-Command informing the prover that @samp{@code{pbp-button-action}} has been@*
+Command informing the prover that @samp{@code{pg-goals-button-action}} has been@*
 requested on a goal.
 @end defvar
 @c TEXI DOCSTRING MAGIC: pbp-hyp-command
 @defvar pbp-hyp-command 
-Command informing the prover that @samp{@code{pbp-button-action}} has been@*
+Command informing the prover that @samp{@code{pg-goals-button-action}} has been@*
 requested on an assumption.
 @end defvar
-@c TEXI DOCSTRING MAGIC: pbp-error-regexp
-@defvar pbp-error-regexp 
+@c TEXI DOCSTRING MAGIC: pg-goals-error-regexp
+@defvar pg-goals-error-regexp 
 Regexp indicating that the proof process has identified an error.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-result-start
@@ -1941,28 +1941,28 @@ Regexp matching end of output from the prover after pbp commands.@*
 In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}.
 @end defvar
 
-@c TEXI DOCSTRING MAGIC: proof-shell-start-char
-@defvar proof-shell-start-char 
+@c TEXI DOCSTRING MAGIC: pg-subterm-start-char
+@defvar pg-subterm-start-char 
 Starting special for a subterm markup.@*
-Subsequent characters with values @strong{below} @code{proof-shell-first-special-char}
+Subsequent characters with values @strong{below} @code{pg-subterm-first-special-char}
 are assumed to be subterm position indicators.  Subterm markups should
-be finished with @code{proof-shell-end-char}.
+be finished with @code{pg-subterm-sep-char}.
 @end defvar
-@c TEXI DOCSTRING MAGIC: proof-shell-end-char
-@defvar proof-shell-end-char 
+@c TEXI DOCSTRING MAGIC: pg-subterm-sep-char
+@defvar pg-subterm-sep-char 
 Finishing special for a subterm markup.@*
-See documentation of @code{proof-shell-start-char}.
+See documentation of @code{pg-subterm-start-char}.
 @end defvar
-@c TEXI DOCSTRING MAGIC: proof-shell-goal-char
-@defvar proof-shell-goal-char 
+@c TEXI DOCSTRING MAGIC: pg-topterm-char
+@defvar pg-topterm-char 
 Mark for goal.
 
 This setting is also used to see if proof-by-pointing features
 are configured.  If it is unset, some of the code 
 for parsing the prover output is disabled.
 @end defvar
-@c TEXI DOCSTRING MAGIC: proof-shell-field-char
-@defvar proof-shell-field-char 
+@c TEXI DOCSTRING MAGIC: pg-subterm-end-char
+@defvar pg-subterm-end-char 
 Annotated field end
 @end defvar
 
@@ -2197,8 +2197,8 @@ under GNU Emacs, to boot.
 @var{lego} and Coq enable it by tradition.
 @end defvar
 
-@c TEXI DOCSTRING MAGIC: proof-before-fontify-output-hook
-@defvar proof-before-fontify-output-hook 
+@c TEXI DOCSTRING MAGIC: pg-before-fontify-output-hook
+@defvar pg-before-fontify-output-hook 
 This hook is called before fonfitying a region in an output buffer.@*
 This hook is mainly used by @code{phox-sym-lock}.
 @end defvar
@@ -3083,8 +3083,8 @@ triples, which is a queue of things to do.
 See the functions @samp{@code{proof-start-queue}} and @samp{proof-exec-loop}.
 @end defvar
 
-@c TEXI DOCSTRING MAGIC: proof-analyse-using-stack
-@defvar proof-analyse-using-stack 
+@c TEXI DOCSTRING MAGIC: pg-subterm-anns-use-stack
+@defvar pg-subterm-anns-use-stack 
 Choice of syntax tree encoding for terms.
 
 If nil, prover is expected to make no optimisations.
@@ -3844,7 +3844,7 @@ Proof General.
 
 ;; The response buffer and goals buffer modes defined above are
 ;; trivial.  In fact, we don't need to define them at all -- they
-;; would simply default to "proof-response-mode" and "pbp-mode".
+;; would simply default to "proof-response-mode" and "pg-goals-mode".
 
 ;; A more sophisticated instantiation might set font-lock-keywords to
 ;; add highlighting, or some of the proof by pointing markup
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 42016e51..d3e27b24 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1824,11 +1824,11 @@ The mouse bindings are these:
 
 @table @kbd
 @item button2
-@code{pbp-button-action}
+@code{pg-goals-button-action}
 @item C-button2
 @code{proof-undo-and-delete-last-successful-command}
 @item button3
-@code{pbp-yank-subterm}
+@code{pg-goals-yank-subterm}
 @end table
 
 Where @kbd{button2} indicates the middle mouse button, and @kbd{button3}
@@ -1847,9 +1847,9 @@ single step in the proof script.  However, if the proof is later
 replayed (without using PBP), the proof-by-pointing constructions will
 be considered as separate proof commands, as usual.
 
-@c TEXI DOCSTRING MAGIC: pbp-button-action
+@c TEXI DOCSTRING MAGIC: pg-goals-button-action
 
-@deffn Command pbp-button-action event
+@deffn Command pg-goals-button-action event
 Construct a proof-by-pointing command based on the mouse-click @var{event}.@*
 This function should be bound to a mouse button in the Proof General
 goals buffer.
@@ -1872,11 +1872,11 @@ easily copy subterms from the output to a proof script.
 
 The right-hand mouse button provides this convenient way to copy
 subterms from the goals buffer, using the function
-@code{pbp-yank-subterm}.
+@code{pg-goals-yank-subterm}.
 
-@c TEXI DOCSTRING MAGIC: pbp-yank-subterm
+@c TEXI DOCSTRING MAGIC: pg-goals-yank-subterm
 
-@deffn Command pbp-yank-subterm event
+@deffn Command pg-goals-yank-subterm event
 Copy the subterm indicated by the mouse-click @var{event}.@*
 This function should be bound to a mouse button in the Proof General
 goals buffer.
diff --git a/etc/lego/pbp.l b/etc/lego/pbp.l
index 82318dce..66a6df72 100644
--- a/etc/lego/pbp.l
+++ b/etc/lego/pbp.l
@@ -2,12 +2,14 @@
 
 (* All using middle-clicks.
   
-   1. Click on  ->        (Intros A B)
-   2. Click on  -> again  (Intros H; Try Refine H)
-   3. Click on A          (Intros H1; Try Refine H1)
-   4. Click on B          (Intros H2; Try Refine H2)
-   5. Click on A in A/\B  (Refine pair; Try Assumption)
-   6. Click on final B    (Try Assumption)
+   1. Click on  ->          (Pbp 0 3 1: Intros A B)
+   2. Click on left (A/\B)  (Pbp 1 2 1: Intros H; Try Refine H)
+   3. Click on A            (Pbp 4 2 1: Intros H1; Try Refine H1)
+   4. Click on B            (Pbp 5 2 1: Intros H2; Try Refine H2)
+   5. Click on A in A/\B    (Pbp 6 2 1: Refine pair; Try Assumption)
+   6. Click on final B      (Pbp 10:    Try Assumption)
+      OR:
+      Click on assumption B (PbpHyp H2: Try Refine H2)
    QED!!
 *)
 
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 66b932f1..dabd9a5c 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -33,19 +33,19 @@ May enable proof-by-pointing or similar features.
 (define-key proof-goals-mode-map [q] 'bury-buffer)
 (cond 
 (proof-running-on-XEmacs
-(define-key proof-goals-mode-map [(button2)] 'pbp-button-action)
+(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)] 'pbp-button-action)
+;; (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)
-(define-key proof-goals-mode-map [(button3)] 'pbp-yank-subterm))
+(define-key proof-goals-mode-map [(button3)] 'pg-goals-yank-subterm))
 (t
-(define-key proof-goals-mode-map [mouse-2] 'pbp-button-action)
+(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] 'pbp-button-action)
+;; (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)
-(define-key proof-goals-mode-map [mouse-3] 'pbp-yank-subterm)))
+(define-key proof-goals-mode-map [mouse-3] 'pg-goals-yank-subterm)))
 
 
 ;;
@@ -77,7 +77,7 @@ May enable proof-by-pointing or similar features.
 ;; To make sense of this code, you should read the
 ;; relevant LFCS tech report by tms, yb, and djs
 
-(defun pbp-yank-subterm (event)
+(defun pg-goals-yank-subterm (event)
   "Copy the subterm indicated by the mouse-click EVENT.
 This function should be bound to a mouse button in the Proof General
 goals buffer.
@@ -104,7 +104,7 @@ explicit yank."
     (if (and span (not (eq proof-buffer-type 'goals)))
 	(yank))))
 
-(defun pbp-button-action (event)
+(defun pg-goals-button-action (event)
   "Construct a proof-by-pointing command based on the mouse-click EVENT.
 This function should be bound to a mouse button in the Proof General
 goals buffer.
@@ -119,7 +119,7 @@ proof-by-pointing command, just as for any proof command the
 user types by hand."
    (interactive "e")
    (mouse-set-point event)
-   (pbp-construct-command))
+   (pg-goals-construct-command))
 
 ;; Using the spans in a mouse behavior is quite simple: from the
 ;; mouse position, find the relevant span, then get its annotation
@@ -135,7 +135,7 @@ user types by hand."
       (incf a))
     (apply 'concat (nreverse ls))))
 
-(defun pbp-construct-command ()
+(defun pg-goals-construct-command ()
   (let* ((span (span-at (point) 'goalsave))
 	 (top-span (span-at (point) 'proof-top-element))
 	 top-info)
@@ -154,16 +154,15 @@ user types by hand."
 	 (format pbp-hyp-command (cdr top-info))))
        (t
 	 (proof-insert-pbp-command
-	  (format pbp-change-goal (cdr top-info))))))))
+	  (format pg-goals-change-goal (cdr top-info))))))))
 
 ;;
 ;; Goals buffer processing
 ;;
-;; FIXME: rename next fn proof-display-in-goals or similar
-(defun proof-shell-analyse-structure (string)
-  "Analyse the term structure of STRING and display it in proof-goals-buffer.
-This function converts proof-by-pointing markup into mouse-highlighted
-extents."
+(defun pg-goals-display (string)
+  "Display STRING in the proof-goals-buffer, properly marked up.
+Converts term substructure markup into mouse-highlighted extents,
+and properly fontifies STRING using proof-fontify-region."
   (save-excursion
       ;; Response buffer may be out of date. It may contain (error)
       ;; messages relating to earlier proof states
@@ -184,14 +183,19 @@ extents."
       (set-buffer proof-goals-buffer)
       (erase-buffer)
       (insert string)
+
+      (if pg-use-specials-for-fontify
+	  ;; With special chars for fontification, do that first,
+	  ;; but keep specials in case also used for subterm markup.
+	  (proof-fontify-region (point-min) (point-max) 'keepspecials))
       
-      ;; Do term-structure markup if its enabled
-      (unless (not proof-shell-goal-char) 
-	(proof-shell-analyse-structure1 (point-min) (point-max)))
+      (run-hooks 'pg-before-subterm-markup-hook)
+      (pg-goals-analyse-structure (point-min) (point-max))
 
-      ;; Now get fonts and characters right
-      ;; FIXME: this may be broken by markup or aided by it!
-      (proof-fontify-region (point-min) (point-max))
+      (unless pg-use-specials-for-fontify
+	;; provers which use ordinary keywords to fontify output must
+	;; do fontification second after subterm specials are removed.
+	(proof-fontify-region (point-min) (point-max)))
 
       ;; Record a cleaned up version of output string
       (setq proof-shell-last-output 
@@ -199,14 +203,60 @@ extents."
 
       (set-buffer-modified-p nil)	; nicety
 
-      ;; Keep point at the start of the buffer.  Might be nicer to
-      ;; keep point at "current" subgoal a la Isamode, but never mind
-      ;; just now.
-      (proof-display-and-keep-buffer proof-goals-buffer (point-min))))
-
-
-(defun proof-shell-analyse-structure1 (start end)
-  "Really analyse the structure here."
+      ;; 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-char' and
+`pg-topterm-goalhyp-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-char
+
+And the function `pg-topterm-goalhyp-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 pg-subterm-start-char
   (let* 
       ((cur start)
        (len (- end start))
@@ -219,21 +269,22 @@ extents."
       (cond
        ;; Seen goal char: this is the start of a top extent
        ;; (assumption or goal)
-       ((= c proof-shell-goal-char)
+       ((= c pg-topterm-char)
 	(setq topl (cons cur topl))
 	(setq ap 0))
 
-       ;; Seen subterm start char: it's followed by at least 
-       ;; one subterm pointer byte
-       ((= c proof-shell-start-char)
+       ;; 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.
+       ((= c pg-subterm-start-char)
 	(incf cur)
-	(if proof-analyse-using-stack
+	(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)) proof-shell-end-char))
+	(while (not (= (setq c (char-after cur)) pg-subterm-sep-char))
 	  (aset ann ap (- c 128))
 	  (incf ap)
 	  (incf cur))
@@ -241,15 +292,15 @@ extents."
 	(setq stack (cons cur 
 			  (cons (substring ann 0 ap) stack))))
 
-       ;; Seen a field char, which terminates an annotated position
+       ;; Seen a subterm end char, terminating an annotated region
        ;; in the concrete syntax.  We make a highlighting span now.
-       ((and (consp stack) (= c proof-shell-field-char))
+       ((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?
-	(if proof-analyse-using-stack
+	(if pg-subterm-anns-use-stack
 	    ;; Pop annotation off stack
 	    (progn
 	      (setq ap 0)
@@ -261,59 +312,62 @@ extents."
       ;; On to next char
       (incf cur))
     
-    ;; List of subterm regions (goals) found
+    ;; List of topterm beginning positions (goals/hyps) found
     (setq topl (reverse (cons end topl)))
     
-    ;; If we want Coq pbp: (setq coq-current-goal 1)
-    (if proof-goal-hyp-fn
-	(while (setq ip (car 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-goalhyp-fn is set.
+    ;; NB: If we want Coq pbp: (setq coq-current-goal 1) 
+    (if pg-topterm-goalhyp-fn
+	(while (setq ap (car topl) 
 		     topl (cdr topl))
-	  (pbp-make-top-span ip (car topl))))
+	  (pg-goals-make-top-span ap (car topl))))
 
     ;; Finally: strip the specials.  This should
     ;; leave the spans in exactly the right place.
-    (proof-shell-strip-special-annotations-buf start end)))
+    (pg-goals-strip-subterm-markup-buf start end))))
 
 
-(defun pbp-make-top-span (start end)
-  "Make a top span (goal area) for mouse active output."
+(defun pg-goals-make-top-span (start end)
+  "Make a top span (goal/hyp area) for mouse active output."
   (let (span name)
     (goto-char start)
-    ;; We need to skip an annotation here for proof-goal-hyp-fn
-    ;; to work again now we don't strip buffers.  Is it
-    ;; safe to assume that we're called exactly at proof-goal-char?
-    ;; [maybe except for last case?]
+    ;; skip the pg-topterm-char itself
     (forward-char)
-    (setq name (funcall proof-goal-hyp-fn))
-    (beginning-of-line)
+    ;; typname is expected to be a cons-cell of a type (goal/hyp)
+    ;; with a name, retrieved from the text immediately following
+    ;; the topterm-char annotation.
+    (setq typname (funcall pg-topterm-goalhyp-fn))
+    (beginning-of-line) ;; any reason why?
     (setq start (point))
     (goto-char end)
     (beginning-of-line)
     (backward-char)
     (setq span (make-span start (point)))
     (set-span-property span 'mouse-face 'highlight)
-    (set-span-property span 'proof-top-element name)))
+    (set-span-property span 'proof-top-element typname)))
 
 
-(defun proof-shell-strip-special-annotations (string)
-  "Strip special annotations from a string, returning cleaned up string.
-*Special* annotations are characters with codes higher than
-'proof-shell-first-special-char'.
-If proof-shell-first-special-char is unset, return STRING unchanged."
-  (if proof-shell-first-special-char
+(defun pg-goals-strip-subterm-markup (string)
+  "Return STRING with subterm and pbp annotations removed.
+Special annotations are characters with codes higher than
+'pg-subterm-first-special-char'.
+If pg-subterm-first-special-char is unset, return STRING unchanged."
+  (if pg-subterm-first-special-char
       (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x )))
 	(while (< ip l)
-	  (if (>= (aref string ip) proof-shell-first-special-char)
-	      (if (char-equal (aref string ip) proof-shell-start-char)
+	  (if (>= (aref string ip) pg-subterm-first-special-char)
+	      (if (char-equal (aref string ip) pg-subterm-start-char)
 		  (progn (incf ip)
+			 ;; da: this relies on annotations being
+			 ;; characters between \200 and first special
+			 ;; char (e.g. \360).  Why not just look for
+			 ;; the sep char??
 			 (while 
-			     ;; FIXME: this relies on annotations 
-			     ;; being characters between 
-			     ;; \200 and \360 (first special char).
-			     ;; Why do we not just look for the 
-			     ;; field char??
 			     (< (aref string ip) 
-				proof-shell-first-special-char)
+				pg-subterm-first-special-char)
 			   (incf ip))))
 	    (aset out op (aref string ip))
 	    (incf op))
@@ -321,25 +375,48 @@ If proof-shell-first-special-char is unset, return STRING unchanged."
 	(substring out 0 op))
     string))
 
-(defun proof-shell-strip-special-annotations-buf (start end)
-  "Strip specials and return new END value."
+(defun pg-goals-strip-subterm-markup-buf (start end)
+  "Remove subterm and pbp annotations from region."
+  ;; FIXME: create these regexps ahead of time.
+  (if pg-subterm-start-char
+      (let ((ann-regexp 
+	     (concat 
+	      (regexp-quote (char-to-string pg-subterm-start-char))
+	      "[^" 
+	      (regexp-quote (char-to-string pg-subterm-sep-char))
+	      "]*"
+	      (regexp-quote (char-to-string pg-subterm-sep-char)))))
+	(save-restriction
+	  (narrow-to-region start end)
+	  (goto-char start)
+	  (proof-replace-regexp ann-regexp "")
+	  (goto-char start)
+	  (proof-replace-string (char-to-string pg-subterm-end-char) "")
+	  (goto-char start)
+	  (if pg-topterm-char
+	      (proof-replace-string (char-to-string pg-topterm-char) ""))))))
+	  
+	 
+
+(defun pg-goals-strip-subterm-markup-buf-old (start end)
+  "Remove subterm and pbp annotations from region."
   (let (c)
     (goto-char start)
     (while (< (point) end)
       ;; FIXME: small OBO here: if char at end is special
       ;; it won't be removed.
       (if (>= (setq c (char-after (point))) 
-	      proof-shell-first-special-char)
+	      pg-subterm-first-special-char)
 	  (progn
 	    (delete-char 1)
 	    (decf end)
-	    (if (char-equal c proof-shell-start-char)
+	    (if (char-equal c pg-subterm-start-char)
 		(progn 
 		  ;; FIXME: could simply replace this by replace
-		  ;; match, matching on field-char??
+		  ;; match, matching on sep-char??
 		  (while (and (< (point) end)
 			      (< (char-after (point))
-				 proof-shell-first-special-char))
+				 pg-subterm-first-special-char))
 		    (delete-char 1)
 		    (decf end)))))
 	(forward-char)))
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 86dfe0ea..c1220a53 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -99,6 +99,105 @@ Internal variable, setting this will have no effect!")
 		  special-display-regexps)))))
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; 
+;; Displaying in the response buffer
+;;
+
+;;
+;; 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.")
+
+(defun proof-shell-maybe-erase-response
+  (&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.
+If CLEAN-WINDOWS is set, use proof-clean-buffer to do the erasing.
+If FORCE, override pg-response-erase-flag.
+
+If the user option proof-tidy-response is nil, then
+the buffer is only cleared when FORCE is set.
+
+No effect if there is no response buffer currently.
+Returns non-nil if response buffer was cleared."
+  (when (buffer-live-p proof-response-buffer)
+    (let ((doit (or (and
+		     proof-tidy-response
+		     (not (eq pg-response-erase-flag 'invisible))
+		     pg-response-erase-flag) 
+		    force)))
+      (if doit
+	  (if clean-windows
+	      (proof-clean-buffer proof-response-buffer)
+	  ;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(.
+	  ;; (erase-buffer proof-response-buffer)
+	    (with-current-buffer proof-response-buffer
+	      (setq proof-shell-next-error nil)	; all error msgs lost!
+	      (erase-buffer))))
+      (setq pg-response-erase-flag erase-next-time)
+      doit)))
+
+(defun pg-response-display (str)
+  "Show STR as a response in the response buffer."
+  (unless pg-use-specials-for-fontify
+    (setq str (pg-goals-strip-subterm-markup str)))
+  (proof-shell-maybe-erase-response t nil)
+  (pg-response-display-with-face str)
+  (proof-display-and-keep-buffer proof-response-buffer))
+  
+;; FIXME: this function should be combined with
+;; proof-shell-maybe-erase-response-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.
+  (if (string-equal str "\n")	
+      str				; quick exit, no display.
+  (let (start end)
+    (with-current-buffer proof-response-buffer
+      ;; da: I've moved newline before the string itself, to match
+      ;; the other cases when messages are inserted and to cope
+      ;; with warnings after delayed output (non newline terminated).
+      ; (ugit (format "End is %i" (point-max)))
+      (goto-char (point-max))
+      (newline)				
+      (setq start (point))
+      (insert str)
+      (unless (bolp) (newline))
+      (setq end (proof-fontify-region start (point)))
+      ;; This is one reason why we don't keep the buffer in font-lock
+      ;; 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 start end 'face face))
+      ;; This returns the decorated string, but it doesn't appear 
+      ;; decorated in the minibuffer, unfortunately.
+      ;; 3.4: remove this for efficiency.
+      ;; (buffer-substring start (point-max))
+      ))))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Tracing buffers
+;;
+
+;; An analogue of pg-response-display-with-face 
+(defun proof-trace-buffer-display (str)
+  "Display STR in the trace buffer."
+  (let (start end)
+    (with-current-buffer proof-trace-buffer
+      (goto-char (point-max))
+      (newline)				
+      (setq start (point))
+      (insert str)
+      (unless (bolp) (newline))
+      (proof-fontify-region start (point)))))
+
+
 
 
 (provide 'pg-response)
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 72bfe296..e91891c4 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -672,7 +672,7 @@ last use time, to discourage saving these into the users database."
 	  (pg-insert-output-as-comment-fn proof-shell-last-output)
 	;; Otherwise the default behaviour is to use comment-region
 	(let  ((beg (point)) end)
-	  ;; proof-shell-strip-special-annotations: should be done
+	  ;; pg-goals-strip-subterm-markup: should be done
 	  ;; for us in proof-fontify-region
 	  (insert proof-shell-last-output)
 	  ;; 3.4: add fontification. Questionable since comments will
diff --git a/generic/proof-compat.el b/generic/proof-compat.el
index 577fbdc7..ac4b74bb 100644
--- a/generic/proof-compat.el
+++ b/generic/proof-compat.el
@@ -1,4 +1,4 @@
-;; proof-comapt.el   Operating system and Emacs version compatibility
+;; proof-compat.el   Operating system and Emacs version compatibility
 ;;
 ;; Copyright (C) 2000-2002 LFCS Edinburgh. 
 ;; Author:      David Aspinall <da@dcs.ed.ac.uk> and others
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 4fb461c5..01ea2bfe 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -513,7 +513,7 @@ Warning messages can come from proof assistant or from Proof General itself."
 
 (defface proof-eager-annotation-face
   (proof-face-specs
-   (:background "lightgoldenrod")
+   (:background "palegoldenrod")
    (:background "darkgoldenrod")
    (:italic t))
   "*Face for important messages from proof assistant."
@@ -1243,7 +1243,7 @@ you only need to set if you use that function (by not customizing
   :type 'string
   :group 'proof-script)
 
-(defcustom proof-goal-hyp-fn nil
+(defcustom pg-topterm-goalhyp-fn nil
   "Function which returns cons cell if point is at a goal/hypothesis.
 This is used to parse the proofstate output to mark it up for
 proof-by-pointing.  It should return a cons or nil.  First element of
@@ -1618,7 +1618,7 @@ Set to nil if proof assistant does not support annotated prompts."
   :type '(choice character (const nil))
   :group 'proof-shell)
 
-(defcustom proof-shell-first-special-char nil
+(defcustom pg-subterm-first-special-char nil
   "First special character.
 Codes above this character can have special meaning to Proof General,
 and are stripped from the prover's output strings.
@@ -1832,7 +1832,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 `proof-goal-hyp-fn',
+In the future it will be used for a generic implementation for `pg-topterm-goalhyp-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)
@@ -1880,7 +1880,7 @@ data triggered by `proof-shell-retract-files-regexp'."
   :type '(choice function (const nil))
   :group 'proof-shell)
 
-(defcustom proof-shell-leave-annotations-in-output nil
+(defcustom pg-use-specials-for-fontify nil
   "Flag indicating whether to strip annotations from output or not.
 \"annotations\" are special characters with the top bit set.
 If annotations are left in, they are made invisible and can be used
@@ -2100,28 +2100,22 @@ output format."
 
 (defcustom proof-state-change-hook nil
   "This hook is called when state change may have occurred. 
-Specifically, this hook is called after a region has been
-asserted or retracted, or after a command has been sent
-to the prover with proof-shell-invisible-command.
+Specifically, this hook is called after a region has been asserted or
+retracted, or after a command has been sent to the prover with
+proof-shell-invisible-command.
 
-This hook is used within Proof General to refresh the 
-toolbar."
-  :type '(repeat function)
-  :group 'proof-shell)
+This hook is used within Proof General to refresh the toolbar."
 
-(defcustom proof-before-fontify-output-hook nil
-  "This hook is called before fonfitying a region in an output buffer.
-This hook is mainly used by phox-sym-lock."
-  :type '(repeat function)
+  :type '(repeat function) 
   :group 'proof-shell)
 
 (defcustom proof-shell-font-lock-keywords nil
   "Value of font-lock-keywords used to fontify the proof shell.
-This is currently used only by proof-easy-config mechanism,
-to set font-lock-keywords before calling proof-config-done.
+This is currently used only by proof-easy-config mechanism, to set
+`font-lock-keywords' before calling `proof-config-done'.
 See also proof-{script,resp,goals}-font-lock-keywords."
   :type 'sexp
-  :group 'proof-script)
+  :group 'proof-shell)
 
 
 
@@ -2132,9 +2126,9 @@ See also proof-{script,resp,goals}-font-lock-keywords."
 (defgroup proof-goals nil
   "Settings for configuring the goals buffer."
   :group 'prover-config
-  :prefix "pbp-")
+  :prefix "pg-goals-")
 
-(defcustom proof-analyse-using-stack nil
+(defcustom pg-subterm-anns-use-stack nil
   "Choice of syntax tree encoding for terms.
 
 If nil, prover is expected to make no optimisations.
@@ -2143,24 +2137,24 @@ For LEGO 1.3.1 use `nil', for Coq 6.2, use `t'."
   :type 'boolean
   :group 'proof-goals)
 
-(defcustom pbp-change-goal nil
+(defcustom pg-goals-change-goal nil
   "Command to change to the goal `%s'"
   :type 'string
   :group 'proof-goals)
 
 (defcustom pbp-goal-command nil
-  "Command informing the prover that `pbp-button-action' has been
+  "Command informing the prover that `pg-goals-button-action' has been
 requested on a goal."
   :type '(choice nil regexp)
   :group 'proof-goals)
 
 (defcustom pbp-hyp-command nil
-  "Command informing the prover that `pbp-button-action' has been
+  "Command informing the prover that `pg-goals-button-action' has been
 requested on an assumption."
   :type '(choice nil regexp)
   :group 'proof-goals)
 
-(defcustom pbp-error-regexp nil
+(defcustom pg-goals-error-regexp nil
   "Regexp indicating that the proof process has identified an error."
   :type '(choice nil regexp)
   :group 'proof-goals)
@@ -2177,22 +2171,32 @@ In particular, after a `pbp-goal-command' or a `pbp-hyp-command'."
   :type 'regexp
   :group 'proof-goals)
 
-(defcustom proof-shell-start-char nil
-  "Starting special for a subterm markup.
-Subsequent characters with values *below* proof-shell-first-special-char
-are assumed to be subterm position indicators.  Subterm markups should
-be finished with proof-shell-end-char."
+(defcustom pg-subterm-start-char nil
+  "Opening special character for subterm markup.
+Subsequent special characters with values *below* 
+pg-subterm-first-special-char are assumed to be subterm position 
+indicators.  Annotations should be finished with pg-subterm-sep-char; 
+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
+subterm and proof-by-pointing markup mechanisms.."
   :type '(choice character (const nil))
   :group 'proof-goals)
 
-(defcustom proof-shell-end-char nil
+(defcustom pg-subterm-sep-char nil
   "Finishing special for a subterm markup.
-See documentation of proof-shell-start-char."
+See doc of `pg-subterm-start-char'."
   :type '(choice character (const nil))
   :group 'proof-goals)
 
-(defcustom proof-shell-goal-char nil
-  "Mark for goal.
+(defcustom pg-topterm-char nil
+  "Annotation character that indicates the beginning of a \"top\" element.
+A \"top\" element may be a sub-goal to be proved or a named hypothesis,
+for example.  It is currently assumed (following LEGO/Coq conventions)
+to span a whole line (the region marked in . 
+The function `pg-topterm-goalhyp-fn' examines text following
 
 This setting is also used to see if proof-by-pointing features
 are configured.  If it is unset, some of the code 
@@ -2200,8 +2204,9 @@ for parsing the prover output is disabled."
   :type 'character
   :group 'proof-goals)
 
-(defcustom proof-shell-field-char nil
-  "Annotated field end"
+(defcustom pg-subterm-end-char nil
+  "Closing special character for subterm markup.
+See `pg-subterm-start-char'."
   :type 'character
   :group 'proof-goals)
 
@@ -2231,6 +2236,17 @@ See also proof-{script,shell,resp}-font-lock-keywords."
   :type 'sexp
   :group 'proof-goals)
 
+(defcustom pg-before-fontify-output-hook nil
+  "This hook is called before fonfitying a region in an output buffer.
+[This hook is presently only used by phox-sym-lock]."
+  :type '(repeat function)
+  :group 'proof-goals)
+
+(defcustom pg-before-subterm-markup-hook nil
+  "This hook is called before analysiing a region for subterm markup."
+  :type '(repeat function)
+  :group 'proof-goals)
+
 
 
 ;;
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 794632ca..6de9d20c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -548,23 +548,15 @@ This is a subroutine of proof-shell-handle-error."
       ;; this string can contain X-Symbol characters, which
       ;; is not suitable for processing with proof-fontify-region.
       (setq string
-	    (if proof-shell-leave-annotations-in-output
+	    (if pg-use-specials-for-fontify
 		(buffer-substring start end)
-	      (proof-shell-strip-special-annotations
+	      (pg-goals-strip-subterm-markup
 	       (buffer-substring start end)))))
     ;; Erase if need be, and erase next time round too.
     (proof-shell-maybe-erase-response t nil)
-    (proof-response-buffer-display string append-face)))
+    (pg-response-display-with-face string append-face)))
 
 
-(defun proof-shell-show-as-response (str)
-  "Show STR as a response in the response buffer."
-  (unless proof-shell-leave-annotations-in-output
-    (setq str (proof-shell-strip-special-annotations str)))
-  (proof-shell-maybe-erase-response t nil)
-  (proof-response-buffer-display str)
-  (proof-display-and-keep-buffer proof-response-buffer))
-  
 (defun proof-shell-handle-delayed-output ()
   "Display delayed output.
 This function handles the cases of proof-shell-delayed-output-kind which
@@ -573,13 +565,13 @@ are not dealt with eagerly during script processing, namely
   (cond
    ;; Response buffer output
    ((eq proof-shell-delayed-output-kind 'abort)
-    (proof-shell-show-as-response proof-shell-delayed-output))
+    (pg-response-display proof-shell-delayed-output))
      ;; "Aborted."  why??
    ((eq proof-shell-delayed-output-kind 'response)
-    (proof-shell-show-as-response proof-shell-delayed-output))
+    (pg-response-display proof-shell-delayed-output))
    ;; Goals buffer output
    ((eq proof-shell-delayed-output-kind 'goals)
-    (proof-shell-analyse-structure proof-shell-delayed-output))
+    (pg-goals-display proof-shell-delayed-output))
    ;; Ignore other cases
    )
   (run-hooks 'proof-shell-handle-delayed-output-hook))
@@ -703,7 +695,7 @@ which see."
     ((proof-shell-string-match-safe proof-shell-error-regexp string)
      ;; FIXME: is the next setting correct or even needed?
      (setq proof-shell-last-output
-	   (proof-shell-strip-special-annotations
+	   (pg-goals-strip-subterm-markup
 	    (substring string (match-beginning 0))))
      (setq proof-shell-last-output-kind 'error))
     
@@ -736,10 +728,10 @@ which see."
        ;;  for Coq by Robert Schneck because Coq has specials but
        ;;  doesn't markup goals output specially).
        (unless (and 
-		proof-shell-first-special-char
+		pg-subterm-first-special-char
 		(not (string-equal 
 		      proof-shell-start-goals-regexp
-		      (proof-shell-strip-special-annotations 
+		      (pg-goals-strip-subterm-markup 
 		       proof-shell-start-goals-regexp))))
 	 (setq start (match-beginning 0)))
        (setq end (if proof-shell-end-goals-regexp
@@ -1230,9 +1222,9 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end."
      ((and proof-shell-trace-output-regexp
 	   (string-match proof-shell-trace-output-regexp message))
       (proof-trace-buffer-display 
-       (if proof-shell-leave-annotations-in-output
+       (if pg-use-specials-for-fontify
 	   message
-	 (proof-shell-strip-special-annotations message)))
+	 (pg-goals-strip-subterm-markup message)))
       (proof-display-and-keep-buffer proof-trace-buffer)
       ;; Force redisplay in case in a fast loop which keeps Emacs
       ;; fully-occupied processing prover output
@@ -1250,15 +1242,15 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end."
       ;; 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)
-      (let ((stripped	(proof-shell-strip-special-annotations message))
+      (let ((stripped	(pg-goals-strip-subterm-markup message))
 	    firstline)
 	;; Display first chunk of output in minibuffer.
 	;; Maybe this should be configurable, it can get noisy.
 	(proof-shell-message 
 	 (substring stripped 0 (or (string-match "\n" stripped)
 				   (min (length stripped) 75))))
-	(proof-response-buffer-display 
-	 (if proof-shell-leave-annotations-in-output
+	(pg-response-display-with-face 
+	 (if pg-use-specials-for-fontify
 	     message
 	   stripped)
 	 'proof-eager-annotation-face)))))
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 77fd63c1..34dc13f2 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -105,6 +105,20 @@ If so, return non-nil."
    (proof-looking-at-safe proof-string-start-regexp)))
 
 
+
+;; Replacing matches
+
+(defun proof-replace-string (string to-string)
+  "Non-interactive version of `replace-string', which see."
+  (while (search-forward string nil t)
+    (replace-match to-string nil t)))
+
+(defun proof-replace-regexp (regexp to-string)
+  "Non-interactive version of `replace-regexp', which see."
+  (while (re-search-forward regexp nil t)
+    (replace-match to-string nil nil)))
+
+
 ;; Generic font-lock
 
 (defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)"
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index b938ecce..e0502010 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -350,40 +350,29 @@ font-lock-mode."
 	  ,proof-font-lock-keywords-case-fold-search))
   (setq font-lock-keywords proof-font-lock-keywords))
 
-(defun proof-fontify-region (start end)
+(defun proof-fontify-region (start end &optional keepspecials)
   "Fontify and decode X-Symbols in region START...END.
 Fontifies according to the buffer's font lock defaults.
 Uses proof-x-symbol-decode to decode tokens if x-symbol is present.
 
-If proof-shell-leave-annotations-in-output is set, remove characters
-with top bit set after fontifying so they don't spoil cut and paste.
+If `pg-use-specials-for-fontify' is set, remove characters
+with top bit set after fontifying so they don't spoil cut and paste,
+unless KEEPSPECIALS is set to override this.
 
 Returns new END value."
   ;; We fontify first because X-sym decoding changes char positions.
   ;; It's okay because x-symbol-decode works even without font lock.
   ;; Possible disadvantage is that font lock patterns can't refer
-  ;; to X-Symbol characters.  Probably they shouldn't!
-
-  ;; 3.5.01: narrowing causes failure in parse-sexp in XEmacs 21.4.
-  ;; I don't think we need it now we use a function to fontify
-  ;; just the region.
-  ;; (narrow-to-region start end)
-
+  ;; to X-Symbol characters.  
   (if proof-output-fontify-enable
       (progn
 	;; Temporarily set font-lock defaults
 	(proof-font-lock-set-font-lock-vars)
-	;; (put major-mode 'font-lock-defaults font-lock-defaults)
-	;; GNU Emacs hack, yuk.
+
+	;; Yukky hacks to immorally interface with font-lock
 	(unless proof-running-on-XEmacs
 	  (font-lock-set-defaults))
 	(let ((font-lock-keywords proof-font-lock-keywords))
-	  ;; FIXME: should set other bits of font lock defaults,
-	  ;; perhaps, such as case fold etc.  What happened to
-	  ;; the careful buffer local font-lock-defaults??
-	  ;; ================================================
-	  ;; 3.5.01: call to font-lock-fontify-region breaks
-	  ;; in xemacs 21.4.  Following hack to fix.
 	  (if (and proof-running-on-XEmacs
 		   (>= emacs-minor-version 4)
 		   (not font-lock-cache-position))
@@ -391,31 +380,42 @@ Returns new END value."
 		(setq font-lock-cache-position (make-marker))
 		(set-marker font-lock-cache-position 0)))
 
-	  ;; ================================================
-	  (run-hooks 'proof-before-fontify-output-hook)
-	  ;; Emacs 21.1: add loudly flag below for font lock
+	  (run-hooks 'pg-before-fontify-output-hook)
 	  (font-lock-default-fontify-region start end nil)
+	  ;; after-fontify hook might do this ugly zap commas thing.
 	  (proof-zap-commas-region start end))))
-  (if proof-shell-leave-annotations-in-output
-      ;; Remove special characters that were used for font lock,
-      ;; so that cut and paste works from here.
+  (if (and pg-use-specials-for-fontify (not keepspecials))
       (progn
-	(goto-char start)
-	(while (< (point) end)
-	  (forward-char)
-	  (unless (< (char-before (point)) 128) ; char-to-int in XEmacs
-	    (delete-char -1)
-	    (setq end (1- end))))))
+	(pg-remove-specials start end)
+	(setq end (point))))
   (prog1
-      ;; Returns new end value
+      ;; Return new end value
       (proof-x-symbol-decode-region start end)
     (proof-font-lock-clear-font-lock-vars)))
-;; old ending:
-;; (prog1 (point-max)
-;; (widen)))
+
+
+(defconst pg-special-char-regexp
+  (let ((c 128) (r "\200"))
+    (while (< c 256) 
+      (setq r (concat r "\\|" (regexp-quote (char-to-string c))))
+      (incf c))
+    r)
+  "Regexp matchin any special character (top bit set).")
+
+
+(defun pg-remove-specials (&optional start end)
+  "Remove special characters (with top bit set) in region.
+Default to whole buffer.  Leave point at END."
+  (save-restriction
+    (if (and start end) 
+	(narrow-to-region start end))
+    (goto-char (or start (point-min)))
+    (proof-replace-regexp pg-special-char-regexp "")
+    (point-max)))
+
+  
 
 ;; FIXME todo: add toggle for fontify region which turns it on/off
-;; (maybe).
 
 (defun proof-fontify-buffer ()
   "Call proof-fontify-region on whole buffer."
@@ -435,48 +435,6 @@ Returns new END value."
   (unless (and (boundp sym) (symbol-value sym))
     (warn "Proof General %s: %s is unset."  tag (symbol-name sym))))
 
-;; FIXME: this function should be combined with
-;; proof-shell-maybe-erase-response-buffer. 
-(defun proof-response-buffer-display (str &optional face)
-  "Display STR with FACE in response buffer."
-  ;; 3.4: no longer return fontified STR, it wasn't used.
-  (if (string-equal str "\n")	
-      str				; quick exit, no display.
-  (let (start end)
-    (with-current-buffer proof-response-buffer
-      ;; da: I've moved newline before the string itself, to match
-      ;; the other cases when messages are inserted and to cope
-      ;; with warnings after delayed output (non newline terminated).
-      ; (ugit (format "End is %i" (point-max)))
-      (goto-char (point-max))
-      (newline)				
-      (setq start (point))
-      (insert str)
-      (unless (bolp) (newline))
-      (setq end (proof-fontify-region start (point)))
-      ;; This is one reason why we don't keep the buffer in font-lock
-      ;; 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 start end 'face face))
-      ;; This returns the decorated string, but it doesn't appear 
-      ;; decorated in the minibuffer, unfortunately.
-      ;; 3.4: remove this for efficiency.
-      ;; (buffer-substring start (point-max))
-      ))))
-
-;; An analogue of proof-response-buffer-display 
-(defun proof-trace-buffer-display (str)
-  "Display STR in the trace buffer."
-  (let (start end)
-    (with-current-buffer proof-trace-buffer
-      (goto-char (point-max))
-      (newline)				
-      (setq start (point))
-      (insert str)
-      (unless (bolp) (newline))
-      (proof-fontify-region start (point)))))
-
 (defun proof-display-and-keep-buffer (buffer &optional pos)
   "Display BUFFER and mark window according to `proof-dont-switch-windows'.
 If optional POS is present, will set point to POS.  
@@ -537,13 +495,13 @@ frame is the one showing the script buffer.)"
 
 (defun proof-message (&rest args)
   "Issue the message ARGS in the response buffer and display it."
-    (proof-response-buffer-display (apply 'concat args))
+    (pg-response-display-with-face (apply 'concat args))
     (proof-display-and-keep-buffer proof-response-buffer))
 
 (defun proof-warning (&rest args)
   "Issue the warning ARGS in the response buffer and display it.
 The warning is coloured with proof-warning-face."
-    (proof-response-buffer-display (apply 'concat args) 'proof-warning-face)
+    (pg-response-display-with-face (apply 'concat args) 'proof-warning-face)
     (proof-display-and-keep-buffer proof-response-buffer))
 
 ;; could be a macro for efficiency in compiled code
@@ -552,7 +510,7 @@ The warning is coloured with proof-warning-face."
 If proof-show-debug-messages is nil, do nothing."
   (if proof-show-debug-messages
       (progn
-	(proof-response-buffer-display (apply 'concat 
+	(pg-response-display-with-face (apply 'concat 
 					      "PG debug: " 
 					      args)
 				       'proof-debug-message-face)
@@ -572,45 +530,6 @@ No action if BUF is nil or killed."
 	     (display-buffer buf t)
 	   (switch-to-buffer-other-window buf)))))
 
-;;
-;; Flag and function to keep response buffer tidy.
-;;
-;; FIXME: rename this now it's moved out of proof-shell.
-;;
-(defvar proof-shell-erase-response-flag nil
-  "Indicates that the response buffer should be cleared before next message.")
-
-(defun proof-shell-maybe-erase-response
-  (&optional erase-next-time clean-windows force)
-  "Erase the response buffer according to proof-shell-erase-response-flag.
-ERASE-NEXT-TIME is the new value for the flag.
-If CLEAN-WINDOWS is set, use proof-clean-buffer to do the erasing.
-If FORCE, override proof-shell-erase-response-flag.
-
-If the user option proof-tidy-response is nil, then
-the buffer is only cleared when FORCE is set.
-
-No effect if there is no response buffer currently.
-Returns non-nil if response buffer was cleared."
-  (when (buffer-live-p proof-response-buffer)
-    (let ((doit (or (and
-		     proof-tidy-response
-		     (not (eq proof-shell-erase-response-flag 'invisible))
-		     proof-shell-erase-response-flag) 
-		    force)))
-      (if doit
-	  (if clean-windows
-	      (proof-clean-buffer proof-response-buffer)
-	  ;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(.
-	  ;; (erase-buffer proof-response-buffer)
-	    (with-current-buffer proof-response-buffer
-	      (setq proof-shell-next-error nil)	; all error msgs lost!
-	      (erase-buffer))))
-      (setq proof-shell-erase-response-flag erase-next-time)
-      doit)))
-
-
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Function for submitting bug reports.
diff --git a/isa/isa.el b/isa/isa.el
index b55085ba..cb4c9481 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -146,7 +146,7 @@ and script mode."
 (defun isa-shell-mode-config-set-variables ()
   "Configure generic proof shell mode variables for Isabelle."
   (setq
-   proof-shell-first-special-char	?\350
+   pg-subterm-first-special-char	?\350
 
    proof-shell-wakeup-char		 ?\372
    proof-shell-annotated-prompt-regexp   "\\(val it = () : unit\n\\)?> \372"
@@ -180,7 +180,7 @@ and script mode."
 
    proof-shell-start-goals-regexp	"\366"
    proof-shell-end-goals-regexp		"\367"
-   proof-shell-goal-char	        ?\370
+   pg-topterm-char	        ?\370
 
    proof-shell-proof-completed-regexp	"^No subgoals!"
 
@@ -210,15 +210,15 @@ and script mode."
    
    ;; Dirty hack to allow font-locking for output based on hidden
    ;; annotations, see isa-output-font-lock-keywords-1
-   proof-shell-leave-annotations-in-output t
+   pg-use-specials-for-fontify t
 
    ;; === ANNOTATIONS  === ones here are broken
    proof-shell-result-start	        "\372 Pbp result \373"
    proof-shell-result-end		"\372 End Pbp result \373"
-   proof-analyse-using-stack		t
-   proof-shell-start-char		?\372
-   proof-shell-end-char			?\373
-   proof-shell-field-char		?\374
+   pg-subterm-anns-use-stack		t
+   pg-subterm-start-char		?\372
+   pg-subterm-sep-char			?\373
+   pg-subterm-end-char		?\374
 
    ;; === MULTIPLE FILE HANDLING ===
    proof-shell-process-file 
@@ -302,7 +302,7 @@ This is a hook function for proof-activate-scripting-hook."
 				 t ; was nil, but falsely leaves Scripting on! 
 			       t))
 	;; Leave the messages from the update around.
-	(setq proof-shell-erase-response-flag nil))))
+	(setq pg-response-erase-flag nil))))
 
 (defun isa-remove-file (name files cmp-base)
   (if (not files) nil
@@ -591,8 +591,8 @@ you will be asked to retract the file or process the remainder of it."
 
 (defun isa-goals-mode-config ()
   ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO.
-  (setq pbp-change-goal "Show %s.")	
-  (setq pbp-error-regexp proof-shell-error-regexp)
+  (setq pg-goals-change-goal "Show %s.")	
+  (setq pg-goals-error-regexp proof-shell-error-regexp)
   (isa-init-output-syntax-table)
   (setq font-lock-keywords isa-goals-font-lock-keywords)
   (proof-goals-config-done))
diff --git a/isar/isar.el b/isar/isar.el
index 6d56eb73..2269145a 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -169,8 +169,6 @@ See -k option for Isabelle interface script."
    proof-really-save-command-p  'isar-global-save-command-p
    proof-count-undos-fn         'isar-count-undos
    proof-find-and-forget-fn     'isar-find-and-forget
-   ;; da: for pbp.
-   ;; proof-goal-hyp-fn         'isar-goal-hyp
    proof-state-preserving-p     'isar-state-preserving-p
    proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list))
 
@@ -178,7 +176,7 @@ See -k option for Isabelle interface script."
 (defun isar-shell-mode-config-set-variables ()
   "Configure generic proof shell mode variables for Isabelle/Isar."
   (setq
-   proof-shell-first-special-char       ?\350
+   pg-subterm-first-special-char        ?\350
 
    proof-shell-wakeup-char              ?\372
    proof-shell-annotated-prompt-regexp  "^\\w*[>#] \372"
@@ -213,13 +211,13 @@ See -k option for Isabelle interface script."
    ;; matches names of assumptions
    proof-shell-assumption-regexp        isar-id
    ;; matches subgoal name
-   ;; da: not used at the moment, maybe after 3.0 used for
-   ;; proof-generic-goal-hyp-fn to get pbp-like features.
+   ;; da: not used at the moment, maybe after 4.0 used for
+   ;; proof-generic-goal-hyp-fn to get pg-goals-like features.
    ;; proof-shell-goal-regexp           "\370[ \t]*\\([0-9]+\\)\\."
 
    proof-shell-start-goals-regexp       "\366\n"
    proof-shell-end-goals-regexp         "\367"
-   proof-shell-goal-char                ?\370
+   pg-topterm-char			?\370
 
    proof-assistant-setting-format       'isar-markup-ml
    proof-shell-init-cmd                 (proof-assistant-settings-cmd)
@@ -234,18 +232,19 @@ See -k option for Isabelle interface script."
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
    proof-shell-clear-goals-regexp       "Proof General, please clear the goals buffer."
 
-   ;; Dirty hack to allow font-locking for output based on hidden
-   ;; annotations, see isar-output-font-lock-keywords-1
-   proof-shell-leave-annotations-in-output t
+   ;; Allow font-locking for output based on hidden annotations, see
+   ;; isar-output-font-lock-keywords-1
+   pg-use-specials-for-fontify		t
 
-   ;; === ANNOTATIONS  === ones below here are broken
+   ;; === ANNOTATIONS  === these ones are not implemented in Isabelle
    proof-shell-result-start             "\372 Pbp result \373"
    proof-shell-result-end               "\372 End Pbp result \373"
-   proof-analyse-using-stack            t
-   proof-shell-start-char               ?\372
-   proof-shell-end-char                 ?\373
-   proof-shell-field-char               ?\374
-
+   pg-subterm-anns-use-stack            t
+   pg-subterm-start-char                ?\372
+   pg-subterm-sep-char                  ?\373
+   pg-subterm-end-char                  ?\374
+   pg-before-subterm-markup-hook	'isabelle-convert-idmarkup-to-subterm
+					;'pg-remove-specials
    proof-shell-process-file
    (cons
     ;; Theory loader output
@@ -578,8 +577,8 @@ proof-shell-retract-files-regexp."
 
 (defun isar-goals-mode-config ()
   ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO.
-  (setq pbp-change-goal "Show %s.")
-  (setq pbp-error-regexp proof-shell-error-regexp)
+  (setq pg-goals-change-goal "Show %s.")
+  (setq pg-goals-error-regexp proof-shell-error-regexp)
   (isar-init-output-syntax-table)
   (setq font-lock-keywords  ;FIXME handle x-symbol stuff by generic code!?
 	;; (append 
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index e1ff82a4..bdb30a72 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -82,7 +82,7 @@
      ;; Special hacks!!
      (cons "Discharge.." 'font-lock-keyword-face)
      (cons "\\*\\*\\* QED \\*\\*\\*" 'font-lock-keyword-face))
-  "*Font-lock table for LEGO terms.")
+  "*Font-lock table for LEGO terms (displayed in output buffers).")
 
 ;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore,
 ;; it might be safer to append "\\s-*:".
diff --git a/lego/lego.el b/lego/lego.el
index 18d5e728..f170c5a2 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -318,7 +318,7 @@ Checks the width in the `proof-goals-buffer'"
 	proof-completed-proof-behaviour 'closeany ; new in 3.0
 	proof-count-undos-fn 'lego-count-undos
 	proof-find-and-forget-fn 'lego-find-and-forget
-        proof-goal-hyp-fn 'lego-goal-hyp
+        pg-topterm-goalhyp-fn 'lego-goal-hyp
 	proof-state-preserving-p 'lego-state-preserving-p)
 
   (setq	proof-save-command-regexp lego-save-command-regexp
@@ -397,12 +397,12 @@ We assume that module identifiers coincide with file names."
         proof-shell-error-regexp lego-error-regexp
 	proof-shell-interrupt-regexp lego-interrupt-regexp
         proof-shell-assumption-regexp lego-id
-        proof-shell-first-special-char ?\360
+        pg-subterm-first-special-char ?\360
         proof-shell-wakeup-char ?\371
-        proof-shell-start-char ?\372
-        proof-shell-end-char ?\373
-        proof-shell-field-char ?\374
-        proof-shell-goal-char ?\375
+        pg-subterm-start-char ?\372
+        pg-subterm-sep-char ?\373
+        pg-subterm-end-char ?\374
+        pg-topterm-char ?\375
 	proof-shell-eager-annotation-start "\376"
 	proof-shell-eager-annotation-start-length 1
 	proof-shell-eager-annotation-end "\377"
@@ -414,7 +414,7 @@ We assume that module identifiers coincide with file names."
 	proof-shell-pre-sync-init-cmd "Configure AnnotateOn;"
         proof-shell-init-cmd lego-process-config
 	proof-shell-restart-cmd lego-process-config
-	proof-analyse-using-stack nil
+	pg-subterm-anns-use-stack nil
 	proof-shell-process-output-system-specific lego-shell-process-output
         lego-shell-current-line-width nil
 
@@ -436,8 +436,8 @@ We assume that module identifiers coincide with file names."
   (proof-shell-config-done))
 
 (defun lego-goals-mode-config ()
-  (setq pbp-change-goal "Next %s;"
-	pbp-error-regexp lego-error-regexp)
+  (setq pg-goals-change-goal "Next %s;"
+	pg-goals-error-regexp lego-error-regexp)
   (setq font-lock-keywords lego-font-lock-terms)
   (lego-init-syntax-table)
   (proof-goals-config-done))
diff --git a/phox/phox.el b/phox/phox.el
index 88396b5b..c7d11ba6 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -152,12 +152,12 @@
    proof-shell-quit-cmd            "quit."
    proof-shell-restart-cmd         "restart."
    proof-shell-proof-completed-regexp   "^.*^proved"
-   ;; proof-shell-first-special-char ?\371
+   ;; pg-subterm-first-special-char ?\371
    ;; proof-shell-wakeup-char ?\371
-   ;; proof-shell-start-char ?\371
-   ;; proof-shell-end-char ?\372
-   ;; proof-shell-goal-char ?\373
-   ;; proof-shell-field-char ?\374
+   ;; pg-subterm-start-char ?\371
+   ;; pg-subterm-sep-char ?\372
+   ;; pg-topterm-char ?\373
+   ;; pg-subterm-end-char ?\374
    ;; proof-shell-eager-annotation-start "\376"
    ;; proof-shell-eager-annotation-start-length 1
    ;; proof-shell-eager-annotation-end "\377"
@@ -215,12 +215,12 @@
    font-lock-keywords  phox-font-lock-keywords
    proof-output-fontify-enable     t)
   (phox-sym-lock-start)
-  (add-hook 'proof-before-fontify-output-hook 'phox-sym-lock-font-lock-hook)
+  (add-hook 'pg-before-fontify-output-hook 'phox-sym-lock-font-lock-hook)
   (proof-goals-config-done))
 
 ;; The response buffer and goals buffer modes defined above are
 ;; trivial.  In fact, we don't need to define them at all -- they
-;; would simply default to "proof-response-mode" and "pbp-mode".
+;; would simply default to "proof-response-mode" and "pg-goals-mode".
 
 ;; A more sophisticated instantiation might set font-lock-keywords to
 ;; add highlighting, or some of the proof by pointing markup
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 185ebd48..922725c3 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -372,7 +372,7 @@ Given is the first SPAN which needs to be undone."
   (setq proof-goal-command-p 'plastic-goal-command-p
 	proof-count-undos-fn 'plastic-count-undos
 	proof-find-and-forget-fn 'plastic-find-and-forget
-        proof-goal-hyp-fn 'plastic-goal-hyp
+        pg-topterm-goalhyp-fn 'plastic-goal-hyp
 	proof-state-preserving-p 'plastic-state-preserving-p)
 
   (setq	proof-save-command-regexp plastic-save-command-regexp
@@ -480,13 +480,13 @@ We assume that module identifiers coincide with file names."
         ;; DEAD proof-shell-noise-regexp "Discharge\\.\\. "
         proof-shell-assumption-regexp plastic-id
         proof-shell-goal-regexp plastic-goal-regexp
-        proof-shell-first-special-char ?\360
+        pg-subterm-first-special-char ?\360
         proof-shell-wakeup-char ?\371		;; only for first send? 
 ;;      proof-shell-wakeup-char nil		;; NIL turns off annotations.
-        proof-shell-start-char ?\372
-        proof-shell-end-char ?\373
-        proof-shell-field-char ?\374
-        proof-shell-goal-char ?\375
+        pg-subterm-start-char ?\372
+        pg-subterm-sep-char ?\373
+        pg-subterm-end-char ?\374
+        pg-topterm-char ?\375
         proof-shell-eager-annotation-start "\376"
 	;; FIXME da: if p-s-e-a-s is implemented, you should set
 	;; proof-shell-eager-annotation-start-length=1 to
@@ -501,7 +501,7 @@ We assume that module identifiers coincide with file names."
 
         proof-shell-init-cmd plastic-process-config
 	proof-shell-restart-cmd plastic-process-config
-        proof-analyse-using-stack nil
+        pg-subterm-anns-use-stack nil
         proof-shell-process-output-system-specific plastic-shell-process-output
         plastic-shell-current-line-width nil
 
@@ -522,8 +522,8 @@ We assume that module identifiers coincide with file names."
   )
 
 (defun plastic-goals-mode-config ()
-  (setq pbp-change-goal "Next %s;"
-        pbp-error-regexp plastic-error-regexp)
+  (setq pg-goals-change-goal "Next %s;"
+        pg-goals-error-regexp plastic-error-regexp)
   (setq font-lock-keywords plastic-font-lock-terms)
   (plastic-init-syntax-table)
   (proof-goals-config-done))