From 189ae3c0fb18dba26462dee590d6a7949ceae5d8 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 29 Feb 2004 18:59:18 +0000 Subject: Test cases for Coq indentation. --- etc/coq/indent.v | 62 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 etc/coq/indent.v diff --git a/etc/coq/indent.v b/etc/coq/indent.v new file mode 100644 index 00000000..456018c6 --- /dev/null +++ b/etc/coq/indent.v @@ -0,0 +1,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 "\\(\\\\s-+\\)?Definition") *) +(* (posix-search-backward "\\(\\\\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 + + -- cgit v1.2.3