aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/coq/indent.v
blob: 456018c6c696cf70485db9ef6f289728b29f710d (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
(* 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