Fix active variable highlighting in Isabelle with X-Symbol.

3 files changed, 26 insertions, 10 deletions

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index e73eca3b..6869bab9 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -101,7 +101,6 @@ and properly fontifies STRING using proof-fontify-region."
 	  ;; but keep specials in case also used for subterm markup.
 	  (proof-fontify-region (point-min) (point-max) 'keepspecials))
       
-      (run-hooks 'pg-before-subterm-markup-hook)
       (pg-goals-analyse-structure (point-min) (point-max))
 
       (unless pg-use-specials-for-fontify
diff --git a/generic/proof-config.el b/generic/proof-config.el
index cbe5e434..bfcda272 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -30,7 +30,7 @@
 ;;  6. Goals buffer configuration
 ;;  [ 7. Splash screen settings  -- moved to proof-splash.el now ]
 ;;  8. X-Symbol support
-;;  9. Prover specific settings [NEW in 3.2 -- using new mechanism]
+;;  9. Prover specific settings
 ;; 10. Global constants 
 ;;
 ;; The user options don't need to be set on a per-prover basis,
@@ -1014,6 +1014,9 @@ match the entire command"
 
 (defcustom proof-non-undoables-regexp nil
   "Regular expression matching commands which are *not* undoable.
+These are commands which should not appear in proof scripts,
+for example, undo commands themselves (if the proof assistant
+cannot \"redo\" an \"undo\").
 Used in default functions `proof-generic-state-preserving-p' 
 and `proof-generic-count-undos'.  If you don't use those,
 may be left as nil."
@@ -2155,7 +2158,9 @@ requested on an assumption."
   :group 'proof-goals)
 
 (defcustom pg-subterm-help-cmd nil
-  "Command to display help about a subterm."
+  "Command to display mouse help about a subterm.
+This command is sent to the proof assistant, replacing %s by the
+subterm that the mouse is over."
   :type '(choice nil string)
   :group 'proof-goals)
 
@@ -2244,13 +2249,16 @@ See also proof-{script,shell,resp}-font-lock-keywords."
   :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 called before fontifying a region in an output buffer.
+A function on this hook can alter the region of the buffer within
+the current restriction, and must return the final value of (point-max).
 [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."
+(defcustom pg-after-fontify-output-hook nil
+  "This hook is called before fonfitying a region in an output buffer.
+[This hook is presently only used by Isabelle]."
   :type '(repeat function)
   :group 'proof-goals)
 
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index e0502010..416edbce 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -363,7 +363,9 @@ 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.  
+  ;; to X-Symbol characters.
+  ;; NB: perhaps we can narrow within the whole function, but there
+  ;; was an earlier problem with doing that.
   (if proof-output-fontify-enable
       (progn
 	;; Temporarily set font-lock defaults
@@ -379,11 +381,18 @@ Returns new END value."
 	      (progn
 		(setq font-lock-cache-position (make-marker))
 		(set-marker font-lock-cache-position 0)))
-
-	  (run-hooks 'pg-before-fontify-output-hook)
+	  
+	  (save-restriction
+	    (narrow-to-region start end)
+	    (run-hooks 'pg-before-fontify-output-hook)
+	    (setq end (point-max)))
 	  (font-lock-default-fontify-region start end nil)
-	  ;; after-fontify hook might do this ugly zap commas thing.
+	  ;; FIXME: after-fontify hook might do this ugly zap commas thing.
 	  (proof-zap-commas-region start end))))
+  (save-restriction
+    (narrow-to-region start end)
+    (run-hooks 'pg-after-fontify-output-hook)
+    (setq end (point-max)))
   (if (and pg-use-specials-for-fontify (not keepspecials))
       (progn
 	(pg-remove-specials start end)