From ece7af6fc988d835de9b16fc1bb67f5762bb6aad Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 14 Jan 2016 16:04:50 +0100 Subject: Fix #29 + indentation glitch + regexp refactoring. --- coq/coq-smie.el | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'coq/coq-smie.el') diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 403dc4a8..a609727a 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -958,6 +958,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ;; tac1 ; <-- no indentation here ;; now ( tac3 ; <- neither here ;; tac5) ; + ;; ] ((and (equal token "; tactic") coq-indent-semicolon-tactical (not (coq-smie-is-ltacdef)) @@ -974,13 +975,19 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((equal token "} subproof") (smie-rule-parent)) - ; using user customized variable to set indentation of modules, - ; section and proofs. + ;; proofstart is a special hack, since "." should be used as a + ;; separator between commands, here it is recognized as an open + ;; parenthesis, hence the current command (C) ending with "." + ;; is not recognized as correctly terminated. The "parent" + ;; computed by smie is therefore wrong and default indetation + ;; is broken. We fix this by indenting from the real-start of + ;; the command terminated by ". proofstart". ((equal token ". proofstart") - (smie-rule-parent coq-indent-proofstart)) + (save-excursion (forward-char -1) (coq-find-real-start) + `(column . ,(+ coq-indent-modulestart (current-column))))) ((equal token ". modulestart") - (smie-rule-parent coq-indent-modulestart)) - )) + (save-excursion (forward-char -1) (coq-find-real-start) + `(column . ,(+ coq-indent-modulestart (current-column))))))) (:before (cond -- cgit v1.2.3