diff options
| -rw-r--r-- | coq/coq-smie-lexer.el | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el index 1e3eebbf..30738f02 100644 --- a/coq/coq-smie-lexer.el +++ b/coq/coq-smie-lexer.el @@ -562,6 +562,8 @@ The point should be at the beginning of the command name." ((member tok coq-smie-dot-friends) ".") + ((and (equal tok "") (eq (point) (point-min))) "b o f") + (tok)))) @@ -634,7 +636,16 @@ Lemma foo: forall n, (". modulestart" commands "end module" exp) (moduledecl) (moduledef) (mutual) (exp)) - (commands (commands "." commands) + + ;; unknown tokens make smie fallback to backward-sexp, which + ;; behaves badly on ill-formed comments. Generally we always + ;; find a known token except when reaching the top of the + ;; file. Therefore we need to have the "beginning of file" + ;; token ("b o f") somewhere to avoid falling back on + ;; backward-sexp. This is the reasonable place probably. The + ;; best would be that smiefallback ignore comments. + (commands ("b o f" commands) + (commands "." commands) (commands "- bullet" commands) (commands "+ bullet" commands) (commands "* bullet" commands) @@ -645,7 +656,8 @@ Lemma foo: forall n, ;; each line orders tokens by increasing priority ;; | C x => fun a => b | C2 x => ... ;;'((assoc "=>") (assoc "|") (assoc "|-" "=> fun")) ; (assoc ", quantif") - '((assoc "- bullet") (assoc "+ bullet") (assoc "* bullet") (assoc ".")) + '((assoc "b o f") ;; beginning of file + (assoc "- bullet") (assoc "+ bullet") (assoc "* bullet") (assoc ".")) '((assoc "with inductive") (assoc ":= def" ":= inductive") (assoc ":=") (assoc "|") (assoc "=>") (assoc "xxx provedby") @@ -731,7 +743,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((equal token "with match") 4) - ((equal token "; tactic") ; "; tactic" maintenant!! + ((equal token "; tactic") (cond ((smie-rule-parent-p "; tactic") (smie-rule-separator kind)) (t (smie-rule-parent 2)))) |