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

8 files changed, 370 insertions, 253 deletions

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.