diff options
| -rw-r--r-- | etc/coq/queryreplace.v | 7 | ||||
| -rw-r--r-- | generic/proof-syntax.el | 14 |
2 files changed, 10 insertions, 11 deletions
diff --git a/etc/coq/queryreplace.v b/etc/coq/queryreplace.v index cbe8e13f..d368d013 100644 --- a/etc/coq/queryreplace.v +++ b/etc/coq/queryreplace.v @@ -1,5 +1,6 @@ (* STATUS: Solved. This was caused by the anyway faulty proof-zap-commas-region failing to save the match data. + See comments in proof-syntax.el about that function. *) (* @@ -27,11 +28,11 @@ Record t : Type := make { null_r : (x:dom)x=(op x null); inv_l : (x:dom)null=(op (inv x) x); inv_r : (x:dom)null=(op x (inv x)); - assoc : (x, y,z:dom)(op x (op y z))=(op (op x y) z); + assoc : (x,y,z:dom)(op x (op y z))=(op (op x y) z); inv_null : null=(inv null); inv_inv : (x:dom)x=(inv (inv x)); - assoc_inv_l : (x, y:dom)y=(op (inv x) (op x y)); - assoc_inv_r : (x, y:dom)y=(op x (op (inv x) y)); + assoc_inv_l : (x,y:dom)y=(op (inv x) (op x y)); + assoc_inv_r : (x,y:dom)y=(op x (op (inv x) y)); inv_op : (x,y:dom)(op (inv y) (inv x))=(inv (op x y)) }. diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index eb873b45..efc0e036 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -143,10 +143,11 @@ Default is comma separated, or SEPREGEXP if set." ;; Refontify the whole line, 'cos that's what font-lock-after-change ;; does. -;;FIXME: Under FSF Emacs 20.2, when initially fontifying the buffer, -;; commas are not zapped. -;; -;; FIXME da: this should be more specific!! +;; 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). @@ -170,10 +171,7 @@ may assign this function to `after-change-function'." (proof-zap-commas-region (point-min) (point-max))) (defun proof-unfontify-separator () - (make-local-variable 'after-change-functions) - (setq after-change-functions - (append (delq 'proof-zap-commas-region after-change-functions) - '(proof-zap-commas-region)))) + (add-hook 'after-change-functions 'proof-zap-commas-region t t)) ;; ;; Functions for doing something like "format" but with customizable |