Documentation.

2 files changed, 12 insertions, 12 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 40d1da52..171a27bb 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1818,11 +1818,16 @@ If nil, just use the rest of the output following proof-shell-start-goals-regexp
 
 (defcustom proof-shell-eager-annotation-start nil
   "Eager annotation field start.  A regular expression or nil.
-An eager annotation indicates to Proof General that some following output
+An \"eager annotation indicates\" to Proof General that some following output
 should be displayed (or processed) immediately and not accumulated for
-parsing later.
+parsing later.  Note that this affects processing of output which is
+ordinarily accumulated: output which appears before the eager annotation 
+start will be discarded.
 
-It is nice to recognize (starts of) warnings or file-reading messages
+The start/end annotations can be used to hilight the output, but
+are stripped from display of the message in the minibuffer.
+
+It is useful to recognize (starts of) warnings or file-reading messages
 with this regexp.  You must also recognize any special messages
 from the prover to PG with this regexp (e.g. `proof-shell-clear-goals-regexp',
 `proof-shell-retract-files-regexp', etc.)
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index 47246fd6..cdb0bd05 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -207,14 +207,10 @@ This is a subroutine of proof-x-symbol-enable."
 (defun proof-x-symbol-mode-associated-buffers ()
   "Activate/deactivate x-symbols in all Proof General associated buffers.
 A subroutine of proof-x-symbol-enable."
-  ;; Response and goals buffer are fontified/decoded 
-  ;; manually in the code, configuration only sets
-  ;; x-symbol-language.
   (proof-map-buffers (list proof-goals-buffer 
 			   proof-response-buffer
 			   proof-trace-buffer)
    (proof-x-symbol-config-output-buffer))
-  ;; Shell has its own configuration
   (proof-with-current-buffer-if-exists proof-shell-buffer
    (proof-x-symbol-shell-config)))
 
@@ -264,8 +260,7 @@ Assumes that the current buffer is the proof shell buffer."
   ;; NB: after changing X-Symbols in output it would be nice to
   ;; refresh display, but there's no robust way of doing that yet
   ;; (see proof-x-symbol-refresh-output-buffers above)
-  ;; [ Actually, we could ask that the activate/decativate command
-  ;;   itself does this ]
+  ;; [ The activate/decativate prover command itself could do it ]
   ;;
   (if proof-x-symbol-initialized
       (progn
@@ -320,9 +315,9 @@ Assumes that the current buffer is the proof shell buffer."
 	      (set-buffer-modified-p modified))))
 	;; END code from x-symbol.el/x-symbol-mode-internal
 
-	;; If we're turning on x-symbol, attempt to convert to 
-	;; characters.  (Only works if the buffer already
-	;; contains tokens!)
+	;; If we're turning on x-symbol, attempt to convert to
+	;; characters.  (Only works if the buffer already contains
+	;; tokens!)  This breaks manual fontification, too.
 	(x-symbol-decode))))
   ;; Encoding back to tokens doesn't work too well: needs to 
   ;; do some de-fontification to remove font properties, and