Complete rework of the indentation mechanism using smie. The first

version of smie indentation code was a good first try but this one is
much faster and cleaner. All desambiguations are done in the lexers,
it is still a bit slow on large proofs. Some bugs remain to be fixed.

1 files changed, 11 insertions, 4 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index fbaaebc4..2030d141 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -323,13 +323,20 @@
 (defvar coq-solve-cheat-tactics-db
   (append
    coq-user-cheat-tactics-db
-   '(
-     ("admit" nil "admit" t "admit")
-     ))
+   '(("admit" nil "admit" t "admit")
+     ("Admitted" nil "Admitted" t "Admitted")))
   "Coq tactic(al)s that solve a subgoal."
   )
 
-
+(setq develock-coq-font-lock-keywords
+  '((develock-find-long-lines
+     (1 'develock-long-line-1 t)
+     (2 'develock-long-line-2 t))
+    ("[^	\n ]\\([	 ]+\\)$"
+     (1 'develock-whitespace-1 t))
+    ("^[	 ]+$"
+     (0 'develock-whitespace-2 append))
+    ("\\.[{}]" 0 'develock-whitespace-2 nil nil)))
 
 
 (defvar coq-tacticals-db