From af9a7086bb182405bc3e738a28d5483afe7d40fb Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 23 Dec 2014 12:30:24 +0000 Subject: Supporting more bullets (coq 8.5), like ++ or ++++. --- coq/coq-smie.el | 87 ++++++++++++++++++++++++++++++++++++++------------------- 1 file changed, 59 insertions(+), 28 deletions(-) (limited to 'coq/coq-smie.el') diff --git a/coq/coq-smie.el b/coq/coq-smie.el index f4153221..7c93f392 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -286,6 +286,19 @@ The point should be at the beginning of the command name." ;; '("Qed" "Save" "Defined" "Admitted" "Abort") (cons "EndSubproof" (remove "End" coq-keywords-save-strict))) + +(defun coq-is-at-command-real-start() + (equal (point) + (save-excursion (coq-find-real-start)))) + +(defun coq-is-bullet-token (tok) (string-suffix-p "bullet" tok)) +(defun coq-is-subproof-token (tok) (string-suffix-p "subproof" tok)) +(defun coq-is-dot-token (tok) (or (string-suffix-p "proofstart" tok) + (string-equal "." tok))) +(defun coq-is-cmdend-token (tok) + (or (coq-is-bullet-token tok) (coq-is-subproof-token tok) (coq-is-dot-token tok))) + + (defun coq-smie-forward-token () (let ((tok (smie-default-forward-token))) (cond @@ -308,8 +321,9 @@ The point should be at the beginning of the command name." (let ((newtok (coq-smie-forward-token))) ;; recursive call (concat tok newtok))) (t (save-excursion (coq-smie-backward-token))))) ;; recursive call - ((member tok - '("=>" ":=" "+" "-" "*" "exists" "in" "as" "∀" "∃" "→" "∨" "∧" ";" "," ":" "eval")) + ((or (string-match coq-bullet-regexp-nospace tok) + (member tok '("=>" ":=" "exists" "in" "as" "∀" "∃" "→" "∨" "∧" ";" + "," ":" "eval"))) ;; The important lexer for indentation's performance is the backward ;; lexer, so for the forward lexer we delegate to the backward one when ;; we can. @@ -361,14 +375,11 @@ The point should be at the beginning of the command name." (tok)))) -(defun coq-is-at-command-real-start() - (equal (point) - (save-excursion (coq-find-real-start)))) (defun coq-smie-:=-deambiguate () (let ((corresp (coq-smie-search-token-backward - '("let" "Inductive" "CoInductive" "{|" "." "with" "Module" "where"); + '("let" "Inductive" "CoInductive" "{|" "." "with" "Module" "where") nil '((("let" "with") . ":="))))) (cond ((equal corresp "with") @@ -395,6 +406,8 @@ The point should be at the beginning of the command name." (defun coq-smie-backward-token () (let ((tok (smie-default-backward-token))) (cond + ;; Distinguish between "," from quantification and other uses of + ;; "," (tuples, tactic arguments) ((equal tok ",") (save-excursion (let ((backtok (coq-smie-search-token-backward @@ -406,9 +419,8 @@ The point should be at the beginning of the command name." "quantif exists") ", quantif" tok)) (t tok))))) - ;; Distinguish between "," from quantification and other uses of - ;; "," (tuples, tactic arguments) + ; Same for ";" : record field separator, tactic combinator, etc ((equal tok ";") (save-excursion (let ((backtok (coq-smie-search-token-backward '("." "[" "{")))) @@ -436,9 +448,9 @@ The point should be at the beginning of the command name." ((and (zerop (length tok)) (member (char-before) '(?\{ ?\})) (save-excursion (forward-char -1) - (member (coq-smie-backward-token) ;; recursive call - '("." ". proofstart" "{ subproof" "} subproof" - "- bullet" "+ bullet" "* bullet")))) + (let ((nxttok (coq-smie-backward-token))) ;; recursive call + (coq-is-cmdend-token tok) + ))) (forward-char -1) (if (looking-at "{") "{ subproof" "} subproof")) @@ -463,21 +475,22 @@ The point should be at the beginning of the command name." ((member tok '("*." "-*." "|-*." "*|-*.")) (forward-char 1) ".") ; for "unfold in *|-*;" ((member tok '("*;" "-*;" "|-*;" "*|-*;")) (forward-char 1) "; tactic") - ((and (member tok '("+" "-" "*")) + ((and (string-match coq-bullet-regexp-nospace tok) (save-excursion (let ((prev (coq-smie-backward-token))) ;; recursive call - (member prev '("." ". proofstart" "{ subproof" "} subproof"))))) + (or (coq-is-subproof-token prev) + (coq-is-dot-token prev))))) (concat tok " bullet")) ((and (member tok '("exists" "∃")) (save-excursion - (not (member - (coq-smie-backward-token) ;; recursive call looking at the ptoken immediately before - '("." ". proofstart" "; tactic" "[" "]" "|" "=>" ;; => may be wrong here but rare (h0ave "=> ltac"?) - "{ subproof" "} subproof" "- bullet" "+ bullet" - "* bullet"))))) + ;; recursive call looking at the ptoken immediately before + (let ((prevtok (coq-smie-backward-token))) + ;; => may be wrong here but rare (have "=> ltac"?) + (not (or (coq-is-cmdend-token prevtok) + (member prevtok '("; tactic" "[" "]" "|" "=>"))))))) "quantif exists") @@ -551,9 +564,9 @@ The point should be at the beginning of the command name." ((equal prev-interesting "match") "in match") (t "in tactic"))))) - ((and (eq (char-before) ?@) (member (char-syntax (char-after)) '(?w ?_))) - (forward-char -1) - (concat "@" tok)) + ((and (eq (char-before) ?@) (member (char-syntax (char-after)) '(?w ?_))) + (forward-char -1) + (concat "@" tok)) ((member tok coq-smie-proof-end-tokens) "Proof End") @@ -663,6 +676,15 @@ Lemma foo: forall n, (commands "- bullet" commands) (commands "+ bullet" commands) (commands "* bullet" commands) + (commands "-- bullet" commands) + (commands "++ bullet" commands) + (commands "** bullet" commands) + (commands "--- bullet" commands) + (commands "+++ bullet" commands) + (commands "*** bullet" commands) + (commands "---- bullet" commands) + (commands "++++ bullet" commands) + (commands "**** bullet" commands) ;; "with" of mutual definition should act like "." ;; same for "where" (introduction of a notation ;; after a inductive or fixpoint) @@ -676,7 +698,11 @@ 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 "- bullet") (assoc "+ bullet") (assoc "* bullet") + (assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet") + (assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet") + (assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet") + (assoc ".") (assoc "with inductive" "with fixpoint" "where")) '((assoc ":= def" ":= inductive") (assoc "|") (assoc "=>") @@ -742,7 +768,7 @@ Lemma foo: forall n, (defun coq-smie-rules (kind token) "Indentation rules for Coq. See `smie-rules-function'. KIND is the situation and TOKEN is the thing w.r.t which the rule applies." - (case kind + (case kind (:elem (case token (basic proof-indent))) (:close-all t) @@ -752,17 +778,19 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ;; second {..} is aligned with the first rather than being indented as ;; if it were an argument to the first. ;; FIXME: this gives a strange indentation for ". { \n .. } \n { .. }" - (when (member token '("{ subproof" "- bullet" "+ bullet" "* bullet" - "." ". proofstart")) + (when (or (coq-is-bullet-token token) + (coq-is-dot-token token) + (member token '("{ subproof"))) (forward-char 1) ; skip de "." (equal (coq-smie-forward-token) "{ subproof")))) (:after (cond ;; Override the default indent step added because of their presence ;; in smie-closer-alist. - ((member token '(":" ":=" ":= with" ":= def" "- bullet" "+ bullet" "* bullet" - "by" "in tactic" "<:" "<+" ":= record" - "with module" "as" ":= inductive" ":= module" )) + ((or (coq-is-bullet-token token) + (member token '(":" ":=" ":= with" ":= def" + "by" "in tactic" "<:" "<+" ":= record" + "with module" "as" ":= inductive" ":= module" ))) 2) ((equal token "with match") 4) @@ -785,6 +813,9 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((member token '("in tactic" "as" "by")) (cond ((smie-rule-parent-p "- bullet" "+ bullet" "* bullet" + "-- bullet" "++ bullet" "** bullet" + "--- bullet" "+++ bullet" "*** bullet" + "---- bullet" "++++ bullet" "**** bullet" "{ subproof" ". proofstart") (smie-rule-parent 4)) ((smie-rule-parent-p "in tactic") (smie-rule-parent)) -- cgit v1.2.3