diff options
| -rw-r--r-- | coq/coq-smie.el | 35 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 10 |
2 files changed, 25 insertions, 20 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 37dc390c..39c68428 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -172,7 +172,7 @@ attention to case differences." (let ((case-fold-search nil)) (save-excursion (coq-find-real-start) - (looking-at "\\(\\(Local\\|Global\\)\\s-+\\)?\\(Ltac\\|Tactic\\s-+Notation\\)\\s-")))) + (looking-at "\\(\\(Local\\|Global\\)\\s-+\\)?\\(Ltac2?\\|Tactic\\s-+Notation\\)\\s-")))) (defun coq-smie-is-inside-parenthesized-tactic () (and (coq-smie-is-tactic) ;; fragile (uppercase test only) @@ -239,7 +239,7 @@ the token of \".\" is simply \".\"." (defun coq-smie-find-unclosed-match-backward () - (let ((tok (coq-smie-search-token-backward '("with" "match" "lazymatch" "multimatch" ".")))) + (let ((tok (coq-smie-search-token-backward '("with" "match" "lazymatch" "multimatch" "lazy_match" "mult_match" ".")))) (cond ((null tok) nil) ((equal tok ".") nil) @@ -493,8 +493,7 @@ The point should be at the beginning of the command name." ;; we can. (save-excursion (coq-smie-backward-token))) - ;; easier to return directly than calling coq-smie-backward-token - ((member tok '("lazymatch" "multimatch")) "match") + ((member tok '("lazymatch" "lazy_match" "multimatch" "multi_match")) "match") ;; detect "with signature", otherwies use coq-smie-backward-token ((equal tok "with") @@ -629,7 +628,7 @@ The point should be at the beginning of the command name." ((equal tok ",") (save-excursion (let ((backtok (coq-smie-search-token-backward - '("forall" "∀" "∃" "exists" "|" "match" "lazymatch" "multimatch" ".")))) + '("forall" "∀" "∃" "exists" "|" "match" "lazymatch" "multimatch" "lazy_match" "multi_match" ".")))) (cond ((member backtok '("forall" "∀" "∃")) ", quantif") ((equal backtok "exists") ; there is a tactic called exists @@ -645,9 +644,9 @@ The point should be at the beginning of the command name." ;; trying to discriminate between bollean operator || and tactical ||. ((equal tok "||") (save-excursion - (let ((backtok (coq-smie-search-token-backward '("." ";" "Ltac" "(" "[" "{")))) + (let ((backtok (coq-smie-search-token-backward '("." ";" "Ltac" "Ltac2" "(" "[" "{")))) (cond - ((member backtok '("." "Ltac")) "|| tactic") + ((member backtok '("." "Ltac" "Ltac2")) "|| tactic") ((and (equal backtok ";") (or (forward-char) t) (equal (coq-smie-backward-token) "; tactic")) ;; recursive @@ -697,7 +696,7 @@ The point should be at the beginning of the command name." ;(coq-find-real-start) (coq-smie-module-deambiguate))) - ((member tok '("lazymatch" "multimatch")) "match") + ((member tok '("lazy_?match" "multi_?match")) "match") ((equal tok "tryif") "if") @@ -734,7 +733,7 @@ The point should be at the beginning of the command name." ;; (forward-char -1) ;; (if (looking-at "{") "{ subproof" "} subproof")) - ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" + ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac2?\\|uconstr\\)" (- (point) 7))) ": ltacconstr") @@ -745,8 +744,8 @@ The point should be at the beginning of the command name." ((equal tok "=>") (save-excursion (let ((corresp (coq-smie-search-token-backward - '("|" "match" "lazymatch" "multimatch" "fun" ".") - nil '((("match" "lazymatch" "multimatch") . "end") ("fun" . "=>"))))) + '("|" "match" "lazymatch" "multimatch" "lazy_match" "multi_match" "fun" ".") + nil '((("match" "lazy_match" "multi_match") . "end") ("fun" . "=>"))))) (cond ((member corresp '("fun")) "=> fun") ; fun (t tok))))) @@ -803,12 +802,12 @@ The point should be at the beginning of the command name." (save-excursion (let ((prev-interesting (coq-smie-search-token-backward - '("match" "lazymatch" "multimatch" "Morphism" "Relation" "." ". proofstart" + '("match" "lazymatch" "multimatch" "lazy_match" "multi_match" "Morphism" "Relation" "." ". proofstart" "{ subproof" "} subproof" "as") nil - '((("match" "lazymatch" "multimatch" "let") . "with") ("with" . "signature"))))) + '((("match" "lazy_match" "multi_match" "let") . "with") ("with" . "signature"))))) (cond - ((member prev-interesting '("match" "lazymatch" "multimatch")) "as match") + ((member prev-interesting '("match" "lazymatch" "multimatch" "lazy_match" "mult_match")) "as match") ((member prev-interesting '("Morphism" "Relation")) "as morphism") (t tok))))) @@ -834,9 +833,9 @@ The point should be at the beginning of the command name." (save-excursion (let ((prev-interesting (coq-smie-search-token-backward - '("let" "match" "lazymatch" "multimatch" ;"eval" should be "eval in" but this is not supported by search-token-backward + '("let" "match" "lazymatch" "multimatch" "lazy_match" "mult_match" ;"eval" should be "eval in" but this is not supported by search-token-backward "." ) nil - '((("match" "lazymatch" "multimatch") . "with") (("let" ;"eval" + '((("match" "lazymatch" "multimatch" "lazy_match" "mult_match") . "with") (("let" ;"eval" ) . "in"))))) (cond ((member prev-interesting '("." nil)) "in tactic") @@ -875,6 +874,10 @@ The point should be at the beginning of the command name." (let ((newtok (coq-smie-backward-token))) ; recursive call (concat newtok "." tok))) + ;; easier to return directly than calling coq-smie-backward-token + ((member tok '("lazymatch" "lazy_match" "multimatch" "multi_match")) "match") + + ((coq-dot-friend-p tok) ".") (tok)))) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 0e143637..a517df71 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -236,14 +236,16 @@ so for the following reasons: ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear") ("lapply" "lap" "lapply" t "lapply") ("lazy" "lazy" "lazy beta delta [#] iota zeta" t "lazy") - ("lazymatch with" "m" "lazymatch # with\n| # => #\nend") + ("lazymatch with" "lazym" "lazymatch # with\n| # => #\nend") + ("lazy_match! with" "lazy_m" "lazy_match! # with\n| # => #\nend") ("left" "left" "left" t "left") ("lia" nil "lia" t "lia") ("linear" "lin" "linear" t "linear") ("load" "load" "load" t "load") ("lra" nil "lra" t "lra") ("move after" "mov" "move # after #" t "move") - ("multimatch with" "m" "multimatch # with\n| # => #\nend") + ("multimatch with" "mm" "multimatch # with\n| # => #\nend") + ("multi_match! with" "multi_m" "multi_match! # with\n| # => #\nend") ("nia" nil "nia" t "nia") ("now_show" nil "now_show" t "now_show") ("nra" nil "nra" t "nra") @@ -955,7 +957,7 @@ so for the following reasons: ("forall (4 args)" "fo4" "forall (#:#) (#:#) (#:#) (#:#), #") ("if" "if" "if # then # else #" nil "if") ("let in" "li" "let # := # in #" nil "let") - ("match! (from type)" nil "" nil "match" coq-insert-match) + ("match?" nil "" nil "match" coq-insert-match) ("match with" "m" "match # with\n| # => #\nend") ("match with 2" "m2" "match # with\n| # => #\n| # => #\nend") ("match with 3" "m3" "match # with\n| # => #\n| # => #\n| # => #\nend") @@ -1172,7 +1174,7 @@ It is used: (append '( "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match" - "lazymatch" "multimatch" + "lazymatch" "multimatch" "lazy_match" "multi_match" "return" "struct" "else" "end" "if" "in" "into" "let" "then" "using" "with" "beta" "delta" "iota" "zeta" "after" "until" "at" "Sort" "Time" "dest" "where" |