blob: be27f9efab36ba1fd00e3a54d3a530edb12bab44 (
plain)
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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
(* Pierre: could you add some real test cases to this file, please?
e.g. a file that can be processed, and indented how you want ---
so TAB makes no difference to indentation (bad examples in comments)
*)
(* First problem: matching compound reserved words *)
Syntactic Definition foo := bar.
(* Neither of these are good enough: the backwards search simply finds "Definition" first *)
(* (re-search-backward "\\(\\<Syntactic\\>\\s-+\\)?Definition") *)
(* (posix-search-backward "\\(\\<Syntactic\\>\\s-+\\)?Definition") *)
(* I suppose Java has this issue too, so the syntax designers of Coq are not
really to blame... However, if you take a look at the Emacs code used for
calculating Java indentation you will get a shock!!
Proof General's is much simpler. I sugest introducing another function
(and regexp)
proof-within-compound-reserved-word
which we can use as a guard for repeating the regexp search backwards, as
an extra condition in proof-indent-goto-prev (similarly to
proof-looking-at-syntactic-context which resumes the search in case we
landed in a string or comment).
Pierre, do you want to try that?
- da
*)
(* Second problem: hanging indentation of cases *)
(* Desirable indent (Pierre: not quite what you said: you had different
indent between Cases and next line in nested case)
Definition f :=
Cases i with
x => Cases x with
z => #
| # => #
| # => #
end
end
*)
(* currently: *)
Definition f :=
Cases i with
x => Cases x with
z => #
| a => b
| # => #
end
end
(* Nasty example from Trac http://proofgeneral.inf.ed.ac.uk/trac/ticket/173 *)
Theorem p : forall (P : Prop), P -> P.
Proof.
try (simpl
in *).
intros P H. apply H. (* da: shouldn't we outdent again here? *)
Qed.
|
