Add improved indenters that rely on the current proof state to choose the indentation depth.

Patch by Cedric Auger.

These two indenters need to be exercised a bit to see if they are actually useful to users.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13715 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 0 deletions

diff --git a/ide/preferences.mli b/ide/preferences.mli
index 41a581d57..723a771b0 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -55,6 +55,15 @@ type pref =
       mutable lax_syntax : bool;
       mutable vertical_tabs : bool;
       mutable opposite_tabs : bool;
+(*
+ *    for indentation
+ *)
+      mutable indent_module_factor : int;
+      mutable indent_section_factor : int;
+      mutable indent_saw_factor : int;
+      mutable indent_was_factor : int;
+      mutable indent_was_alinea : int;
+      mutable indent_tactic_was_mode : bool;
     }
 
 val save_pref : unit -> unit