Test cases for Coq indentation.

1 files changed, 62 insertions, 0 deletions

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 "\\(\\<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
+    
+