Customization variables for modules, section and proof indentation.

2 files changed, 25 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index e73fb502..b8fb5e5f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,14 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
 *** smie indentation is now the only choice.
     Old code removed. will work only if emacs >= 23.3.
 
+*** indentation off modules, sections and proofs are customizable
+
+    (setq coq-indent-modulestart X) will set indentation width for
+    modules and sections to X characters
+
+    (setq coq-indent-proofstart X) will set indentation width for
+    modules and sections to X characters
+
 *** indentation of match with cases:
     by default the indentation is like this now:
     match n with
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 9a7df711..06cc2582 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -639,6 +639,16 @@ Lemma foo: forall n,
   :type 'boolean
   :group 'coq)
 
+(defcustom coq-indent-proofstart 2
+  "Number of spaces used to indent after a proof start."
+  :type 'integer
+  :group 'coq)
+
+(defcustom coq-indent-modulestart 2
+  "Number of spaces used to indent after a module or section start."
+  :type 'integer
+  :group 'coq)
+
 (defcustom coq-match-indent 2
   "Number of space used to indent cases of a match expression.
 If the \"|\" separator is used, indentation will be reduced by 2.
@@ -838,6 +848,13 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
        ((equal token "in let") (smie-rule-parent))
 
        ((equal token "} subproof") (smie-rule-parent))
+
+       ; using user customized variable to set indentation of modules,
+       ; section and proofs.
+       ((equal token ". proofstart")
+	(smie-rule-parent coq-indent-proofstart))
+       ((equal token ". modulestart")
+	(smie-rule-parent coq-indent-modulestart))
        ))
 
      (:before