aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-syntax.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2012-06-28 16:10:43 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2012-06-28 16:10:43 +0000
commit8ee46969bf68ebb3dc5e18ccc64a3d0f6e018f14 (patch)
tree5b6ed98c8520b90ee2ba251316de033b96328de2 /coq/coq-syntax.el
parentde7919ddc8ca3b365667061c10ff5f3442418bfa (diff)
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.
Diffstat (limited to 'coq/coq-syntax.el')
-rw-r--r--coq/coq-syntax.el15
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