From 7ecdbfb869b5e9d6cd75c610ef125823b3727071 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 8 Jun 2012 11:40:43 +0000 Subject: Indentation is a bit more accurate. --- coq/coq.el | 97 ++++++++++++++++++++++++++++++++++++-------------------------- 1 file changed, 57 insertions(+), 40 deletions(-) (limited to 'coq/coq.el') diff --git a/coq/coq.el b/coq/coq.el index 05fd9cb6..de331372 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -382,9 +382,9 @@ Lemma foo: forall n, ;; Having "return" here rather than as a separate rule in `exp' causes ;; it to be indented at a different level than "with". (matchexp (exp) (exp "as match" exp) (exp "in match" exp) (exp "return" exp) ) - (assigns (exp ":=" exp) (assigns ";" assigns)) + (assigns (exp ":= let" exp) (assigns ";" assigns)) (exps (exp) (exps "," exps)) - (expss (exps) (expss ";" expss) (expss "as" expss)) + (expss (exps) (exps ":= record" exps) (expss ";" expss) (expss "as" expss)) (expsss (expss) (expsss "=>" expsss)) (expssss (expsss) (expssss "|" expssss)) ;; The elements below are trying to capture the syntactic structure @@ -398,16 +398,16 @@ Lemma foo: forall n, ("Proof" subcmds "Proof End") ("Module" subcmds "End") ("Section" subcmds "End")) - (cmds ("Add" exp ":=" exp) - ("Lemma" exp ":=" exp) - ("Theorem" exp ":=" exp) - ("Instance" exp ":=" exp) - ("Class" exp ":=" exp) - ("Definition" exp ":=" exp) - ("Let" exp ":=" exp) + (cmds ("Add" exp ":=" exp) ("Add" exp) + ("Lemma" exp ":=" exp) ("Lemma" exp) + ("Theorem" exp ":=" exp) ("Theorem" exp) + ("Instance" exp ":=" exp) ("Instance" exp) + ("Class" exp ":=" exp) ("Class" exp) + ("Definition" exp ":=" exp) ("Definition" exp) + ("Let" exp ":=" exp) ("Let" exp) ("Function" exp ":=" exp) - ("Fixpoint" exp ":=" exp) - ("Inductive" exp ":= inductive") + ("Program Fixpoint" exp ":=" exp) ("Fixpoint" exp ":=" exp) + ("Inductive" exp ":= inductive" expssss) ("CoInductive" exp ":= inductive" expssss) ("Notation" exp ":=" exp) ("Record" exp ":=" exp) @@ -431,14 +431,15 @@ Lemma foo: forall n, (assoc ">") (assoc ">=") (assoc "<") (assoc "<=") (left "<>") (left "=") (left "==") (nonassoc "else") - (nonassoc "in") (assoc "in tactic") (left "=>")) + (nonassoc "in") (assoc "in tactic") (left ":= record") (left "=>")) ;;'((nonassoc "return") (nonassoc "in match") (nonassoc "as match")) '((assoc ",")(assoc ";")(right "as")(assoc "|")(left "=>")) '((left "- bullet") (left "+ bullet") (left "* bullet")) '((assoc "."))))) "Parsing table for Coq. See `smie-grammar'.") -(defun coq-smie-search-token-forward (tokens &optional end) + +(defun coq-smie-search-token-forward (tokens &optional end ignore-between) "Search for one of TOKENS between point and END. Token \".\" is considered only if followed by a space." (unless end (setq end (point-max))) @@ -446,16 +447,20 @@ Token \".\" is considered only if followed by a space." (catch 'found (while (< (point) end) ;; The default lexer is faster and is good enough for our needs. - (let ((next (smie-default-forward-token))) - ;; Do not consider "." when not followed by a space - (when (or (not (equal next ".")) - (looking-at "[[:space:]]")) - (cond - ((zerop (length next)) (forward-sexp 1)) - ((member next tokens) (throw 'found next))))))) + (let* ((next (smie-default-forward-token)) + (parop (assoc next ignore-between))) + (if parop ; if we find something to ignore, we directly + ; go to corresponding closer + (coq-smie-search-token-forward (cons (cdr parop) nil) end ignore-between) + ;; Do not consider "." when not followed by a space + (when (or (not (equal next ".")) + (looking-at "[[:space:]]")) + (cond + ((zerop (length next)) (forward-sexp 1)) + ((member next tokens) (throw 'found next)))))))) (scan-error nil))) -(defun coq-smie-search-token-backward (tokens &optional end) +(defun coq-smie-search-token-backward (tokens &optional end ignore-between) "Search for one of TOKENS between point and END. Token \".\" is considered only if followed by a space." (unless end (setq end (point-min))) @@ -463,13 +468,17 @@ Token \".\" is considered only if followed by a space." (catch 'found (while (> (point) end) ;; The default lexer is faster and is good enough for our needs. - (let ((next (smie-default-backward-token))) - ;; Do not consider "." when not followed by a space - (when (or (not (equal next ".")) - (looking-at ".[[:space:]]")) - (cond - ((zerop (length next)) (forward-sexp -1)) - ((member next tokens) (throw 'found next))))))) + (let* ((next (smie-default-backward-token)) + (parop (rassoc next ignore-between))) + (if parop ; if we find something to ignore, we directly + ; go to corresponding closer + (coq-smie-search-token-backward (cons (car parop) nil) end ignore-between) + ;; Do not consider "." when not followed by a space + (when (or (not (equal next ".")) + (looking-at ".[[:space:]]")) + (cond + ((zerop (length next)) (forward-sexp -1)) + ((member next tokens) (throw 'found next)))))))) (scan-error nil))) @@ -613,12 +622,16 @@ Token \".\" is considered only if followed by a space." (if (looking-at "{") "BeginSubproof" "EndSubproof")) ((and (equal tok "") (looking-back "|}" (- (point) 2))) (goto-char (match-beginning 0)) "|}") - ((and (equal tok ":=") - (save-excursion - (member (coq-smie-search-token-backward - '("let" "Inductive" "Coinductive" ".")) - '("Inductive" "CoInductive")))) - ":= inductive") + + ((equal tok ":=") + (save-excursion + (let ((corresp (coq-smie-search-token-backward + '("let" "Inductive" "Coinductive" "{|" ".") nil '(("let" . ":="))))) + (cond + ((member corresp '("Inductive" "CoInductive")) ":= inductive") + ((equal corresp "let") ":= let") + ((or (looking-back "{")) ":= record") + (t tok))))) ((equal tok "*.") (forward-char 1) ".") ; for "auto with *." ((and (member tok '("+" "-" "*")) (save-excursion @@ -699,9 +712,9 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((equal token "return") 2) ((equal token "as") 2) ((and (equal token ";") - (smie-rule-parent-p "." "[" "]" "BeginSubproof" "EndSubproof" "|")) - 2) - ;((member token '(":=")) 0) + (smie-rule-parent-p "." "{|" "[" "]" "BeginSubproof" "EndSubproof" "|")) + (smie-rule-separator kind)) + ((member token '(":= inductive")) 2) ((and (equal token ",") (not (smie-rule-parent-p "forall" "quantif exists"))) 0))) (:before @@ -712,9 +725,13 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((equal token "as") 2) ((member token '("return" "in match" "as match")) (if (smie-rule-parent-p "match") 3)) ((equal token "|") - (if (smie-rule-prev-p "with match") - (- (funcall smie-rules-function :after "with match") 2) - (smie-rule-separator kind))) + (cond ((smie-rule-prev-p "with match") + (- (funcall smie-rules-function :after "with match") 2)) + ((smie-rule-prev-p ":= inductive") + (- (funcall smie-rules-function :after ":= inductive") 2)) + (t (smie-rule-separator kind))) + ;(smie-rule-separator kind) + ) ; ((and (equal token ":=") ; (smie-rule-parent-p "Definition" "Lemma" "Fixpoint" "Inductive" ; "Function" "Let" "Record" "Instance" "Class" -- cgit v1.2.3