diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-03-31 08:39:29 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-03-31 08:39:29 +0000 |
| commit | a7c9490551d8f7638c09eea238e77c0b4aa86e6e (patch) | |
| tree | c0c6288f102d9d849fd4f3549bd51313690a0b27 /coq/coq-smie.el | |
| parent | 605a9890bca09e9c6e24ce0e774bc7bfbd3f212e (diff) | |
Fixed smie code for ";" + added || in grammar.
Actually || and + are overloaded and I don"t see how to deambiguate
them. Indetation may be buggy until I found away.
Diffstat (limited to 'coq/coq-smie.el')
| -rw-r--r-- | coq/coq-smie.el | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 349004ac..14bf6b87 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -429,6 +429,7 @@ The point should be at the beginning of the command name." (t ":=")))) ; a parenthesis stopped the search + (defun coq-smie-backward-token () (let ((tok (smie-default-backward-token))) (cond @@ -451,7 +452,7 @@ The point should be at the beginning of the command name." (save-excursion (let ((backtok (coq-smie-search-token-backward '("." "[" "{" "Ltac")))) (cond - ((equal backtok ".") "; tactic") + ((member backtok '("." "Ltac")) "; tactic") ((equal backtok nil) (if (or (looking-back "(") (looking-back "\\[") (and (looking-back "{") @@ -682,7 +683,7 @@ Typical values are 2 or 4." '((exp (exp ":= def" exp) (exp ":=" exp) (exp ":= inductive" exp) - (exp "|" exp) (exp "=>" exp) + (exp "||" exp) (exp "|" exp) (exp "=>" exp) (exp "xxx provedby" exp) (exp "as morphism" exp) (exp "with signature" exp) ("match" matchexp "with match" exp "end");expssss @@ -774,6 +775,7 @@ Typical values are 2 or 4." (assoc "&") (assoc "/\\") (assoc "\\/") (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>") (assoc "=?") (assoc "<=?") (assoc "<?") (assoc "^") + (assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible (assoc "+") (assoc "-") (assoc "*") (assoc ": ltacconstr") (assoc ". selector")) '((assoc ":" ":<") (assoc "<")) |