aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--etc/coq/queryreplace.v7
-rw-r--r--generic/proof-syntax.el14
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