diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2013-07-08 10:01:38 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2013-07-08 10:01:38 +0000 |
| commit | 60f4c20ee80f138f287aba7b252c5eb71c2bfd1b (patch) | |
| tree | 272fc6453d90ff7e9be4846eea4994b519c0cce8 | |
| parent | 01e99e72aacce3cd833cd2c484dd86e9b8e9223d (diff) | |
Fixing again bug #466. With a bbetter solution.
Not using "b o f" token anymore.
| -rw-r--r-- | coq/coq-smie-lexer.el | 15 | ||||
| -rw-r--r-- | coq/coq.el | 2 |
2 files changed, 4 insertions, 13 deletions
diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el index cf9c9878..9cd69c98 100644 --- a/coq/coq-smie-lexer.el +++ b/coq/coq-smie-lexer.el @@ -566,8 +566,6 @@ The point should be at the beginning of the command name." ((coq-dot-friend-p tok) ".") - ((and (equal tok "") (eq (point) (point-min))) "b o f") - (tok)))) @@ -642,15 +640,7 @@ Lemma foo: forall n, (moduledecl) (moduledef) (mutual) (exp)) - ;; 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 (commands "." commands) (commands "- bullet" commands) (commands "+ bullet" commands) (commands "* bullet" commands) @@ -661,8 +651,7 @@ 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 "b o f") ;; beginning of file - (assoc "- bullet") (assoc "+ bullet") (assoc "* bullet") (assoc ".")) + '((assoc "- bullet") (assoc "+ bullet") (assoc "* bullet") (assoc ".")) '((assoc "with inductive") (assoc ":= def" ":= inductive") (assoc ":=") (assoc "|") (assoc "=>") (assoc "xxx provedby") @@ -1148,6 +1148,8 @@ and `use-project-file' to disable this feature." (defun coq-mode-config () + ; smie needs this + (set (make-local-variable 'parse-sexp-ignore-comments) t) ;; Coq error messages are thrown off by TAB chars. (set (make-local-variable 'indent-tabs-mode) nil) ;; Coq defninition never start by a parenthesis |