From a7c9490551d8f7638c09eea238e77c0b4aa86e6e Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 31 Mar 2015 08:39:29 +0000 Subject: 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. --- coq/coq-smie.el | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'coq/coq-smie.el') 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 "