diff options
| -rw-r--r-- | coq/coq-smie.el | 49 | ||||
| -rw-r--r-- | coq/coq.el | 30 | ||||
| -rw-r--r-- | coq/ex/indent.v | 54 |
3 files changed, 102 insertions, 31 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 0dec5703..9fa2e707 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -702,8 +702,7 @@ Lemma foo: forall n, (moduledecl) (moduledef) (exp)) - - (commands (commands "." commands) + (commands (commands "." commands) (commands "- bullet" commands) (commands "+ bullet" commands) (commands "* bullet" commands) @@ -800,11 +799,12 @@ 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 (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")))) +; (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 @@ -824,10 +824,21 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ; "as" tactical is not idented correctly ((equal token "in let") (smie-rule-parent)) + + ((equal token "} subproof") (smie-rule-parent)) )) (:before (cond + +; ((and (member token '("{ subproof")) +; (not coq-indent-box-style) +; (not (smie-rule-bolp))) +; (if (smie-rule-parent-p "Proof") +; (smie-rule-parent 2) +; (smie-rule-parent))) + + ((equal token "with module") (if (smie-rule-parent-p "with module") (smie-rule-parent) @@ -856,17 +867,11 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." -; ((and (member token '("{ subproof")) -; (not coq-indent-box-style) -; (not (smie-rule-bolp))) -; (if (smie-rule-parent-p "Proof") -; (smie-rule-parent 2) -; (smie-rule-parent))) ;; This applies to forall located on the same line than "Lemma" - ;; & co. This says that "if it would be on the beginning of + ;; & co. This says that "if it *were* be on the beginning of ;; line" (which it is not) it would be indented of 2 wrt ;; "Lemma". This never applies directly to indent the forall, ;; but it is used to guess indentation of the next line. This @@ -881,16 +886,6 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ;; Lemma foo: forall x:nat, ;; x <= 0 -> x = 0. -;; Replaced by the code below relying on smie-rule-bolp ; -; ((and (member token '("forall" "quantif exists")) -; (message "ICI 1") -; (not coq-indent-box-style) -; (coq-is-at-first-line-of-def-decl)) -; (message "ICI") -; (back-to-indentation) -; `(column . ,(+ 2 (current-column)))) -; - ;; TEST THIS BEFORE COMMITING. ((and (member token '("forall" "quantif exists")) (not coq-indent-box-style) (not (smie-rule-bolp))) @@ -898,7 +893,11 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((and (member token '("forall" "quantif exists")) (smie-rule-parent-p "forall" "quantif exists")) - (smie-rule-parent)) + (if (save-excursion + (coq-smie-search-token-backward '("forall" "quantif exists")) + (equal (current-column) (current-indentation))) + (smie-rule-parent) + (smie-rule-parent 2))) ;; This rule allows "End Proof" to align with corresponding ". @@ -334,7 +334,9 @@ See also `coq-hide-additional-subgoals'." ;; Indentation and navigation support via SMIE. (defcustom coq-use-smie t - "If non-nil, Coq mode will try to use SMIE for indentation. + "OBSOLETE. smie code is always used now. + +If non-nil, Coq mode will try to use SMIE for indentation. SMIE is a navigation and indentation framework available in Emacs >= 23.3." :type 'boolean :group 'coq) @@ -1310,6 +1312,23 @@ Warning: )) +; +;(defun coq-is-at-cmd-first-line-p () +; (save-excursion +; (let ((l1 (line-number-at-pos))) +; (coq-find-real-start) +; (equal l1 (line-number-at-pos))))) +; + +; +;(defun coq-indent-command () +; (save-excursion +; (when (coq-is-at-cmd-first-line-p) +; (let ((kind (coq-back-to-indentation-prevline))) +; (if +; (current-column)))))) +; + (defun coq-mode-config () ;; SMIE needs this. (set (make-local-variable 'parse-sexp-ignore-comments) t) @@ -1362,10 +1381,11 @@ Warning: proof-nested-undo-regexp coq-state-changing-commands-regexp proof-script-imenu-generic-expression coq-generic-expression) - (if (and coq-use-smie (fboundp 'smie-setup)) - (smie-setup coq-smie-grammar #'coq-smie-rules - :forward-token #'coq-smie-forward-token - :backward-token #'coq-smie-backward-token) + (if (fboundp 'smie-setup) ; always use smie, old indentation code removed + (progn + (smie-setup coq-smie-grammar #'coq-smie-rules + :forward-token #'coq-smie-forward-token + :backward-token #'coq-smie-backward-token)) (require 'coq-indent) (setq ;; indentation is implemented in coq-indent.el diff --git a/coq/ex/indent.v b/coq/ex/indent.v index c146f61d..edf1a536 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -267,7 +267,7 @@ End X. Require Import Morphisms. Generalizable All Variables. -Open Local Scope signature_scope. +Local Open Scope signature_scope. Require Import RelationClasses. Module TC. @@ -344,3 +344,55 @@ Section SET. end. End SET. + +Module curlybracesatend. + + Lemma foo: forall n: nat, + exists m:nat, + m = n + 1. + Proof. + intros n. + destruct n. { + exists 1. + reflexivity. } + exists (S (S n)). + simpl. + rewrite NPeano.Nat.add_1_r. + reflexivity. + Qed. + + Lemma foo2: forall n: nat, + exists m:nat, (* This is strange compared to the same line in the previous lemma *) + m = n + 1. + Proof. + intros n. + destruct n. { + exists 1. + reflexivity. } + + exists (S (S n)). + simpl. + rewrite NPeano.Nat.add_1_r. + reflexivity. + Qed. + + Lemma foo3: forall n: nat, + exists m:nat, (* This is strange compared to the same line in the previous lemma *) + m = n + 1. + Proof. + intros n. cut (n = n). { + destruct n. { + exists 1. + reflexivity. } { + exists (S (S n)). + simpl. + rewrite NPeano.Nat.add_1_r. + reflexivity. } + } + idtac. + reflexivity. + Qed. + + +End curlybracesatend. + |