diff options
| author | Pierre Courtieu | 2012-01-18 14:06:05 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2012-01-18 14:06:05 +0000 |
| commit | 4aa1e71604e91413f84e2de14f01c50df05596da (patch) | |
| tree | 0bba22abaa187e3efef0dbe673ba10e4dbb36adb | |
| parent | b4b0c56b664c79a6e09bf6a70ea14483edd9e2d4 (diff) | |
Fixed a small bug in indentation (ter repetita). Bullets are indented
correctly provided that the precedence - > + > * is respected.
| -rw-r--r-- | coq/coq.el | 12 |
1 files changed, 8 insertions, 4 deletions
@@ -380,7 +380,9 @@ Lemma foo: forall n, ;; layered above the commands language. Bullets are all the same as a ;; first approximation. (subcmds (cmds) - (subcmds "+*- bullet" subcmds) + (subcmds "- bullet" subcmds) + (subcmds "+ bullet" subcmds) + (subcmds "* bullet" subcmds) ("BeginSubproof" subcmds "EndSubproof") ;captures also { and } ("Proof" subcmds "Proof End") ("Proof" subcmds "Proof End") @@ -411,7 +413,7 @@ Lemma foo: forall n, '((assoc ",") (nonassoc "as") (assoc ":") (assoc "->") (nonassoc "else") (nonassoc "in") (assoc "in tactic") (left "=>")) '((assoc ",")(assoc ";")(assoc "|")(left "=>")) - '((left "+*- bullet")) + '((left "- bullet") (left "+ bullet") (left "* bullet")) '((assoc "."))))) "Parsing table for Coq. See `smie-grammar'.") @@ -560,7 +562,7 @@ Lemma foo: forall n, (save-excursion (let ((prev (coq-smie-backward-token))) (member prev '("." "BeginSubproof" "EndSubproof"))))) - "+*- bullet") + (concat tok " bullet")) ((member tok coq-smie-proof-end-tokens) "Proof End") ((and (member tok '("exists" "∃")) (save-excursion @@ -627,7 +629,9 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." (not (smie-rule-parent-p "forall" "quantif exists"))) 0))) (:before (cond - ((equal token "+*- bullet") 2) + ((equal token "- bullet") 2) + ((equal token "+ bullet") 2) + ((equal token "* bullet") 2) ((equal token "return") (if (smie-rule-parent-p "match") 3)) ((equal token "|") (if (smie-rule-prev-p "with match") |