Improved implementation of zap-commas font lock behaviour, patch from Stefan Monnier

8 files changed, 38 insertions, 95 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index dce173e2..e8f1fe64 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -455,7 +455,9 @@ Idtac (Nop) tactic, put the following line in your .emacs:
      (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)
      (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face)
      (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
-     (list coq-save-with-hole-regexp 2 'font-lock-function-name-face))))
+     (list coq-save-with-hole-regexp 2 'font-lock-function-name-face)
+     ;; Remove spurious variable and function faces on commas.
+     '(proof-zap-commas))))
 (defvar coq-font-lock-keywords coq-font-lock-keywords-1)
 
 (defun coq-init-syntax-table ()
diff --git a/coq/coq.el b/coq/coq.el
index 641fc1b4..06015bb6 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -680,8 +680,6 @@ This is specific to coq-mode."
 
   (setq font-lock-keywords coq-font-lock-keywords-1)
 
-  (setq proof-font-lock-zap-commas t)	; enable the painful hack
-  
   (proof-config-done)
 
 ;; outline
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 2d2da9fc..7933fbc3 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -118,7 +118,7 @@ whether X-Symbol is installed in your Emacs."
   "*Whether to fontify output from the proof assistant.
 If non-nil, output from the proof assistant will be highlighted
 in the goals and response buffers.
-(This is providing font-lock-keywords have been set for the 
+\(This is providing font-lock-keywords have been set for the 
 buffer modes)."
   :type 'boolean
   :group 'proof-user-options)
@@ -153,7 +153,7 @@ read-only region.  If nil, Proof General is more relaxed (but may give
 you a reprimand!).
 
 If you change proof-strict-read-only during a session, you must 
-use the \"Restart\" button (or M-x proof-shell-restart) before
+use the \"Restart\" button (or \\[proof-shell-restart]) before
 you can see the effect in buffers.
 
 The default value for proof-strict-read-only depends on which
@@ -704,11 +704,11 @@ If a function, it should return the command string to insert."
 
 (defconst proof-toolbar-entries-default
   `((state	"Display Proof State" "Display the current proof state" t 
-		proof-showproof-command)
-    (context	"Display Context" "Display the current context" t 
-		proof-context-command)
+				      proof-showproof-command)
+    (context	"Display Context"     "Display the current context" t 
+				      proof-context-command)
     (goal	"Start a New Proof"   "Start a new proof" t
-		proof-goal-command)
+				      proof-goal-command)
     (retract	"Retract Buffer"      "Retract (undo) whole buffer" t)
     (undo	"Undo Step"           "Undo the previous proof command" t)
     (delete	"Delete Step"         nil t)
@@ -717,15 +717,14 @@ If a function, it should return the command string to insert."
     (goto	"Goto Point"	      "Process or undo to the cursor position" t)
     (restart	"Restart Scripting"   "Restart scripting (clear all locked regions)" t)
     (qed	"Finish Proof"        "Close/save proved theorem" t
-		proof-save-command)
+				      proof-save-command)
     (lockedend  "Goto Locked End"     nil t)
-    (find	"Find Theorems"	      "Find theorems" t
-		proof-find-theorems-command)
+    (find	"Find Theorems"	      "Find theorems" t proof-find-theorems-command)
     (command    "Issue Command"	      "Issue a non-scripting command" t)
     (interrupt  "Interrupt Prover"    "Interrupt the proof assistant (warning: may break synchronization)" t)
     (visibility "Toggle Visibility"   nil t)
     (info	nil		      "Show online proof assistant information" t
-		proof-info-command)
+				      proof-info-command)
     (help	nil		      "Proof General manual" t))
 "Example value for proof-toolbar-entries.  Also used to define scripting menu.
 This gives a bare toolbar that works for any prover, providing the
@@ -1390,21 +1389,6 @@ for scripting commands), unless activated-interactively is set."
   :group 'proof-script)
 
 
-(defcustom proof-font-lock-zap-commas nil
-  "If non-nil, enable a font-lock hack which unfontifies commas.
-If you fontify variables inside lists like [a,b,c] by matching
-on the brackets `[' and `]', you may take objection to the commas 
-being coloured as well.  In that case, enable this hack which
-will magically restore the commas to the default font for you.
-
-The hack is rather painful and forces immediate fontification of
-files on loading (no lazy, caching locking).  It is unreliable
-under GNU Emacs, to boot.
-
-LEGO and Coq enable it by tradition."
-  :type 'boolean
-  :group 'proof-script)
-
 (defcustom proof-script-font-lock-keywords nil
   "Value of font-lock-keywords used to fontify proof scripts.
 This is currently used only by proof-easy-config mechanism,
@@ -1458,7 +1442,7 @@ See pg-user.el: pg-create-in-span-context-menu for more hints."
 Suggestion: this can be set in proof-pre-shell-start-hook from
 a variable which is in the proof assistant's customization
 group.  This allows different proof assistants to coexist
-(albeit in separate Emacs sessions)."
+\(albeit in separate Emacs sessions)."
   :type 'string
   :group 'proof-shell)
 
@@ -1488,9 +1472,9 @@ See also `proof-shell-init-cmd'."
 (defcustom proof-shell-init-cmd nil
    "The command for initially configuring the proof process.
 This command is sent to the process as soon as synchronization is gained
-(when an annotated prompt is first recognized).  It can be used to configure 
+\(when an annotated prompt is first recognized).  It can be used to configure 
 the proof assistant in some way, or print a welcome message
-(since output before the first prompt is discarded).
+\(since output before the first prompt is discarded).
 
 See also `proof-shell-pre-sync-init-cmd'."
    :type '(choice string (const nil))
@@ -1703,7 +1687,7 @@ See `proof-shell-error-regexp' and `proof-shell-interrupt-regexp'."
   "Regular expression which matches an error message, perhaps with line/column.
 Used by `proof-next-error' to jump to line numbers causing 
 errors during some batch processing of the proof assistant.
-(During \"manual\" script processing, script usually automatically
+\(During \"manual\" script processing, script usually automatically
 jumps to the end of the locked region)
 
 Match number 2 should be the line number, if present.
@@ -1718,13 +1702,13 @@ which is assumed to precede pg-next-error-regexp."
   "Used to locate a filename that an error message refers to.
 Used by `proof-next-error' to jump to locations causing 
 errors during some batch processing of the proof assistant.
-(During \"manual\" script processing, the script usually automatically
+\(During \"manual\" script processing, the script usually automatically
 jumps to the end of the locked region).
 
 Match number 2 should be the file name, if present.
 
 Errors must first be matched by `pg-next-error-regexp'
-(whether they contain a line number or not).  The response buffer
+\(whether they contain a line number or not).  The response buffer
 is then searched *backwards* for a regexp matching this variable,
 `pg-next-error-filename-regexp'.  (So if the
 filename appears after the line number, make the first regexp
@@ -1976,7 +1960,7 @@ This is an experimental feature, currently work-in-progress."
   "Regexp used to split the list of strings which match
 `proof-shell-theorem-dependency-list-regexp'.  Used as
 an argument to `split-string'; nil defaults to whitespace.
-(This setting is necessary for provers which allow whitespace in
+\(This setting is necessary for provers which allow whitespace in
 the names of theorems/definitions/constants), see setting for
 Isabelle in isa/isa.el and isar/isar.el."
   :type '(choice nil regexp)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 67c52088..2c24a3d9 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2439,15 +2439,15 @@ Otherwise just do proof-restart-buffers to delete some spans from memory."
 
 (defun proof-config-done-related ()
   "Finish setup of Proof General scripting and related modes.
-This is a subroutine of proof-config-done.
+This is a subroutine of `proof-config-done'.
 
 This is intended for proof assistant buffers which are similar to
 script buffers, but for which scripting is not enabled.  In
 particular, we: lock the buffer if it appears on
-proof-included-files-list; configure font-lock support from
-font-lock-keywords; maybe turn on X-Symbol minor mode.
+`proof-included-files-list'; configure font-lock support from
+`font-lock-keywords'; maybe turn on X-Symbol minor mode.
 
-This is used for Isabelle theory files, which share some scripting 
+This is used for Isabelle theory files, which share some scripting
 mode features, but are only ever processed atomically by the proof
 assistant."
   (setq proof-script-buffer-file-name buffer-file-name)
@@ -2487,24 +2487,6 @@ assistant."
   ;; Assume font-lock case folding follows proof-case-fold-search
   (proof-font-lock-configure-defaults 'autofontify proof-case-fold-search)
   
-  ;; Hack for unfontifying commas (yuck)
-  (remove-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer t)
-  (remove-hook 'font-lock-mode-hook 'proof-unfontify-separator t)
-  (if proof-font-lock-zap-commas
-      (progn
-	(add-hook 'font-lock-after-fontify-buffer-hook 
-		  'proof-zap-commas-buffer nil t)
-	(add-hook 'font-lock-mode-hook 'proof-unfontify-separator 
-		  nil t)
-	;; if we don't have the following in XEmacs, zap-commas fails.
-	(if (boundp 'font-lock-always-fontify-immediately)
-	    (progn
-	      (make-local-variable 'font-lock-always-fontify-immediately)
-	      ;; FIXME da: this is pretty nasty.  Disables use of 
-	      ;; lazy/caching font lock for large files, and they
-	      ;; can take a long time to fontify.
-	      (setq font-lock-always-fontify-immediately t)))))
-
   ;; Maybe turn on x-symbol mode.
   (proof-x-symbol-mode))
 
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 02bf6aca..e912c1b7 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -125,7 +125,7 @@ If so, return non-nil."
   "A regular expression for parsing identifiers.")
 
 ;; For font-lock, we treat ,-separated identifiers as one identifier
-;; and refontify commata using \{proof-unfontify-separator}.
+;; and refontify commata using \{proof-zap-commas}.
 
 (defun proof-ids (proof-id &optional sepregexp)
   "Generate a regular expression for separated lists of identifiers.
@@ -140,38 +140,15 @@ Default is comma separated, or SEPREGEXP if set."
 ;; this was even more bogus.                                        ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; Refontify the whole line, 'cos that's what font-lock-after-change
-;; does.
-
-;; FIXME: This is quite broken under GNU Emacs, where the elaborate
-;; font-lock support mechanisms tend to get in the way.  Setting
-;; font-lock-support-mode to nil restores the behaviour after editing,
-;; but initial un-fontification is still broken.
-;; FIXME: this should be removed/made specific!!
-;;
-(defun proof-zap-commas-region (start end &optional length)
-  "Remove the face of all `,' within the region (START,END).
-The optional argument LENGTH has no effect. It is required so that we
-may assign this function to `after-change-function'."
-  (save-match-data
-    (save-excursion
-      (let 
-	  ((start (progn (goto-char start) (beginning-of-line) (point)))
-	   (end (progn (goto-char end) (end-of-line) (point))))
-	(goto-char start)
-	(while (search-forward "," end t)
-	  (if (memq (get-char-property (- (point) 1) 'face)
-		    (list 'proof-declaration-name-face
-			  'font-lock-function-name-face))
-	      (font-lock-unfontify-region (- (point) 1) (point))
-	    ))))))
-
-(defun proof-zap-commas-buffer () 
-  "Remove the face of all `,' in the current buffer."
-  (proof-zap-commas-region (point-min) (point-max)))
-
-(defun proof-unfontify-separator ()
-  (add-hook 'after-change-functions 'proof-zap-commas-region t t))
+(defun proof-zap-commas (limit)
+  "Remove the face of all `,' from point to LIMIT.
+Meant to be used from `font-lock-keywords'."
+  (while (search-forward "," limit t)
+    (if (memq (get-text-property (1- (point)) 'face)
+	      '(proof-declaration-name-face
+		font-lock-variable-name-face
+		font-lock-function-name-face))
+	(put-text-property (1- (point)) (point) 'face nil))))
 
 ;;
 ;; Functions for doing something like "format" but with customizable
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 0bf5e305..46b4b5d3 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -407,9 +407,9 @@ Returns new END value."
 	    (narrow-to-region start end)
 	    (run-hooks 'pg-before-fontify-output-hook)
 	    (setq end (point-max)))
-	  (font-lock-default-fontify-region start end nil)
+	  (font-lock-default-fontify-region start end nil))))
 	  ;; FIXME: after-fontify hook might do this ugly zap commas thing.
-	  (proof-zap-commas-region start end))))
+	  ;;(proof-zap-commas-region start end))))
   (save-restriction
     (narrow-to-region start end)
     (run-hooks 'pg-after-fontify-output-hook)
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index bdb30a72..5cf7867a 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -103,7 +103,9 @@
      (cons (proof-ids-to-regexp lego-keywords) 'font-lock-keyword-face)
      (cons (proof-ids-to-regexp lego-tacticals) 'proof-tacticals-name-face)
      (list lego-goal-with-hole-regexp 2 'font-lock-function-name-face)
-     (list lego-save-with-hole-regexp 2 'font-lock-function-name-face))))
+     (list lego-save-with-hole-regexp 2 'font-lock-function-name-face)
+     ;; Remove spurious variable and function faces on commas.
+     '(proof-zap-commas))))
      
 (defun lego-init-syntax-table ()
   "Set appropriate values for syntax table in current buffer."
diff --git a/lego/lego.el b/lego/lego.el
index 74e32dd6..6a8b50d6 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -339,8 +339,6 @@ Checks the width in the `proof-goals-buffer'"
 
   (setq font-lock-keywords lego-font-lock-keywords-1)
 
-  (setq proof-font-lock-zap-commas t)	; enable the painful hack
-  
   (proof-config-done)
 
 ;; outline