1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
(* 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.
*)
(*
From: Cuihtlauac ALVARADO <cuihtlauac.alvarado@francetelecom.com>
To: David Aspinall <da@dcs.ed.ac.uk>
Subject: broken query-replace
Date: 09 Jul 2002 11:09:03 +0200
BTW, there's something stange I've forgot to post.
In FSF-emacs PG & global-font-lock-mode does not play well together. Add
(global-font-lock-mode t)
in your .emacs an then try to query-replace "dom" by "foo" in
*)
Record t : Type := make {
dom : Set;
null : dom;
inv : dom->dom;
op : dom->dom->dom;
null_l : (x:dom)x=(op null x);
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);
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));
inv_op : (x,y:dom)(op (inv y) (inv x))=(inv (op x y))
}.
(*
assoc, assoc_inv_l, assoc_inv_r and inv_op occurences of "dom" are
replaced by "fooom" instead of "dom", quite strange is'n it ?
Query-replacing "dom" by "bar" leads to "barom", which make me thinks
only the first letter of the pattern is replaced...
I've seen this strange behaviour for a while, it was present in
earlier versions of PG & emacs.
*)
|
