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

It seems to be the cause for bug #2472.

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

10 files changed, 13 insertions, 364 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 5db5f0f3ab..5c7d8cce80 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -250,6 +250,4 @@ let goals coqtop =
 
 let make_cases coqtop s = eval_call coqtop (Ide_blob.make_cases s)
 
-let contents coqtop = eval_call coqtop (Ide_blob.contents)
-
 let current_status coqtop = eval_call coqtop Ide_blob.current_status
diff --git a/ide/coq.mli b/ide/coq.mli
index 9c39409abe..6bc5934775 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -57,8 +57,6 @@ val is_in_loadpath : coqtop -> string -> bool Ide_blob.value
 
 val make_cases : coqtop -> string -> string list list Ide_blob.value
 
-val contents : coqtop -> Lib.library_segment Ide_blob.value
-
 (* Message to display in lower status bar. *)
 
 val current_status : coqtop -> string Ide_blob.value
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 25bbf0ef4f..8845cade09 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -31,7 +31,7 @@ object('self)
   val message_view : GText.view
   val proof_buffer : GText.buffer
   val proof_view : GText.view
-  val cmd_stack : (ide_info * Indent.interp_node) Stack.t
+  val cmd_stack : ide_info Stack.t
   val mutable is_active : bool
   val mutable read_only : bool
   val mutable filename : string option
@@ -67,8 +67,7 @@ object('self)
   method get_insert : GText.iter
   method get_start_of_input : GText.iter
   method go_to_insert : unit
-  method indent_current_line_using_previous_line : unit
-  method indent_current_line_using_levels : unit
+  method indent_current_line : unit
   method go_to_next_occ_of_cur_word : unit
   method go_to_prev_occ_of_cur_word : unit
   method insert_command : string -> string -> unit
@@ -540,12 +539,6 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
 
 let sup_args = ref ""
 
-let current_interp_node stk =
-    try
-      let (_, pno) = Stack.top stk in
-      pno
-    with Stack.Empty -> Indent.first_interp_node
-
 class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct =
 object(self)
   val input_view = _script
@@ -564,7 +557,6 @@ object(self)
   val mutable last_auto_save_time = 0.
   val mutable detached_views = []
   val mutable find_forward_instead_of_backward = false
-  val mutable tab_one_tap = false
 
   val mutable auto_complete_on = !current.auto_complete
   val hidden_proofs = Hashtbl.create 32
@@ -734,7 +726,7 @@ object(self)
               `INSERT)
 
 
-  method indent_current_line_using_previous_line =
+  method indent_current_line =
     let get_nb_space it =
       let it = it#copy in
       let nb_sep = ref 0 in
@@ -764,45 +756,6 @@ object(self)
       end
 
 
-  method indent_current_line_using_levels =
-    let get_nb_space it =
-      let it = it#copy in
-      let nb_sep = ref 0 in
-      let continue = ref true in
-      while !continue do
-        if it#char = space then begin
-          incr nb_sep;
-          if not it#nocopy#forward_char then continue := false;
-        end else continue := false
-      done;
-      !nb_sep
-    in
-    let current_line_start = self#get_insert#set_line_offset 0 in
-    let current_line_spaces = get_nb_space current_line_start in
-    if input_buffer#delete_interactive
-      ~start:current_line_start
-      ~stop:(current_line_start#forward_chars current_line_spaces)
-      ()
-    then
-      let current_line_start = self#get_insert#set_line_offset 0 in
-      let levels = Indent.compute_nesting (current_interp_node cmd_stack) in
-      let common_shift =
-	!current.indent_module_factor * levels.Indent.module_levels +
-          !current.indent_section_factor * levels.Indent.section_levels
-      in
-      let additionnal_shift =
-            if !current.indent_tactic_was_mode
-            then !current.indent_was_factor * levels.Indent.tactic_levels +
-	         if levels.Indent.tactic_alinea
-                 then 0
-                 else !current.indent_was_alinea
-            else !current.indent_saw_factor * levels.Indent.subgoal_levels
-      in
-      let shifting = common_shift + additionnal_shift in
-      input_buffer#insert
-        ~iter:current_line_start
-        (String.make shifting ' ')
-
   method go_to_next_occ_of_cur_word =
     let cv = session_notebook#current_term in
     let av = cv.analyzed_view in
@@ -973,13 +926,7 @@ object(self)
            end;
          let ide_payload = { start = `MARK (b#create_mark start);
                              stop = `MARK (b#create_mark stop); } in
-         let (interp_node, e_msg_opt) = Indent.compute_interp_node
-                (Coq.goals mycoqtop)
-	     (current_interp_node cmd_stack)
-             (Coq.contents mycoqtop)
-         in
-         Stack.push (ide_payload, interp_node) cmd_stack;
-(*         (match e_msg_opt with Some(s) -> flash_info s | _ -> ());*)
+         Stack.push ide_payload cmd_stack;
          if display_goals then self#show_goals;
          remove_tag (start,stop) in
     begin
@@ -1007,13 +954,7 @@ object(self)
                input_buffer#place_cursor ~where:stop;
              let ide_payload = { start = `MARK (input_buffer#create_mark start);
                                  stop = `MARK (input_buffer#create_mark stop); } in
-             let (interp_node, e_msg_opt) = Indent.compute_interp_node
-                (Coq.goals mycoqtop)
-	         (current_interp_node cmd_stack)
-                 (Coq.contents mycoqtop)
-             in
-             Stack.push (ide_payload, interp_node) cmd_stack;
-(*         (match e_msg_opt with Some(s) -> flash_info s | _ -> ());*)
+             Stack.push ide_payload cmd_stack;
              self#show_goals;
       (*Auto insert save on success...
        try (match Coq.get_current_goals () with
@@ -1087,7 +1028,7 @@ object(self)
   method reset_initial =
     sync (fun _ ->
             Stack.iter
-              (function (inf, _) ->
+              (function inf ->
                  let start = input_buffer#get_iter_at_mark inf.start in
                  let stop = input_buffer#get_iter_at_mark inf.stop in
                    input_buffer#move_mark ~where:start (`NAME "start_of_input");
@@ -1108,11 +1049,11 @@ object(self)
     (* pop Coq commands until we reach iterator [i] *)
     let rec n_step n =
       if Stack.is_empty cmd_stack then n else
-        let (ide_ri, ide_ii) = Stack.pop cmd_stack in
+        let ide_ri = Stack.pop cmd_stack in
         if i#compare (input_buffer#get_iter_at_mark ide_ri.stop) < 0 then
           n_step (succ n)
         else
-          (Stack.push (ide_ri, ide_ii) cmd_stack; n)
+          (Stack.push ide_ri cmd_stack; n)
     in
     begin
       try
@@ -1124,8 +1065,7 @@ object(self)
               sync (fun _ ->
                       let start =
                         if Stack.is_empty cmd_stack then input_buffer#start_iter
-                        else input_buffer#get_iter_at_mark
-                                 (fst (Stack.top cmd_stack)).stop in
+                        else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
                       prerr_endline "Removing (long) processed tag...";
                       input_buffer#remove_tag
                         Tags.Script.processed
@@ -1162,7 +1102,7 @@ object(self)
     if Mutex.try_lock coq_may_stop then
       (push_info "Undoing last step...";
        (try
-          let (ide_ri, _) = Stack.pop cmd_stack in
+          let ide_ri = Stack.pop cmd_stack in
           let start = input_buffer#get_iter_at_mark ide_ri.start in
           let update_input () =
             prerr_endline "Removing processed tag...";
@@ -1206,8 +1146,6 @@ object(self)
               ("progress "^p^".\n") (p^".\n")) l)
 
   method active_keypress_handler k =
-    (if GdkEvent.Key.keyval k <> GdkKeysyms._Tab
-     then tab_one_tap <- false);
     let state = GdkEvent.Key.state k in
       begin
         match  state with
@@ -1230,12 +1168,7 @@ object(self)
           | l ->
               if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin
                 prerr_endline "active_kp_handler for Tab";
-                begin
-                  tab_one_tap <- not tab_one_tap;
-                  if tab_one_tap
-                  then self#indent_current_line_using_levels
-                  else self#indent_current_line_using_previous_line
-                end;
+                self#indent_current_line;
                 true
               end else false
       end
diff --git a/ide/ide.mllib b/ide/ide.mllib
index af9861c3a5..87b66babae 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -20,5 +20,4 @@ Undo
 Coq
 Coq_commands
 Command_windows
-Indent
 Coqide
diff --git a/ide/indent.ml b/ide/indent.ml
deleted file mode 100644
index 05afb6f2a1..0000000000
--- a/ide/indent.ml
+++ /dev/null
@@ -1,148 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-type proof_node = {
-        (* In saw mode, identation depends directly from
-         * the remaining subgoals to be proven
-         * *)
-        remaining_subgoals : int;
-        (* A subgoal stack is a list of remaining subgoals
-         * at each "keypoint";
-         *
-         * Imagine you have to solve a subgoal "S", and you
-         * know that "n" subgoals remain to be proved.
-         *
-         * After running a tactic, let us call "m" the number of
-         * remaining subgoals to be proven; 3 cases occur:
-         * - if "m" > "n", then you know that you have entered a
-         *   new indentation level and that you will close it
-         *   once the remaining goals are below "n", so
-         *   we push "n" in this case to keep track of it
-         * - if "m" = "n" then nothing changes
-         * - if "m" < "n" then according to the first case we
-         *   have to look if the top of our stack is below "n";
-         *   if so we pop our stack, so that our indentation
-         *   level is always equal to depth of our stack
-         * *)
-        subgoals_stack : int list;
-        (* [first_step] means that the number of remaining
-         * subgoals has changed (cases 1 and 3 of previous enumeration)
-         * *)
-        first_step : bool;
-}
-type interp_node = {
-  opened_sections : int;
-  opened_modules : int;
-  interp_mode : proof_node option;
-}
-
-(* In the first step, we have not yet any interp node,
- * but we need one to use [compute_interp_node],
- * so we provide one
- * *)
-let first_interp_node = {
-  opened_sections = 0;
-  opened_modules = 0;
-  interp_mode = None;
-}
-
-(* this functions finds how many modules and sections are opened *)
-let get_opened lstk =
-  let rec get_opened lstk (sections, modules) =
-    match lstk with
-    | [] -> (sections, modules)
-    | (_, node)::lstk -> get_opened lstk
-          ( match node with
-            | Lib.OpenedModule(_,_,_)
-            | Lib.OpenedModtype(_,_) ->
-              sections, 1+modules
-            | Lib.OpenedSection(_,_) ->
-              1+sections, modules
-(*            | Lib.ClosedModule(_)
-            | Lib.ClosedModtype(_) ->
-              sections, modules-1
-            | Lib.ClosedSection(_) ->
-              sections-1, modules*)
-            | _ -> sections, modules
-          )
-  in
-  match lstk with
-  | Ide_blob.Fail(_,_) -> (0,0)
-  | Ide_blob.Good lstk -> get_opened lstk (0, 0)
-
-(* given the current pftreestate
- * (or None if we are neither in proof nor tactic mode)
- *  and the previous proof_node, we can compute the
- * current proof_node
- * *)
-let compute_interp_node pftso pno lstk =
-  let (i_mode, o_msg) =
-  match pftso with
-  | Ide_blob.Fail(_,_) -> (None, None)
-  | Ide_blob.Good (Ide_blob.Message s) -> (None, None)
-  | Ide_blob.Good (Ide_blob.Goals goals) ->
-     (* we need the number of remaining subgoals in tactic mode *)
-     let rs = List.length goals in
-     (* and the indication that the proof is really terminated in case
-      * rs = 0 for declarative mode
-      * *)
-     if rs = 0
-     then (None, None)
-     else
-       let (fs, (ss, e_msg)) =
-         match pno.interp_mode with
-         | None -> (true, ([], None))
-         | Some pn ->
-            let (fs, (ss, e_msg)) =
-             if rs = pn.remaining_subgoals
-             then (false, (pn.subgoals_stack, None))
-             else (true,
-                   if rs > pn.remaining_subgoals
-                   then (pn.remaining_subgoals::pn.subgoals_stack, None)
-                   else let rec unhead l = match l with
-                                           | [] -> ([], Some("Indentation system broken"))
-                                           |h::t-> if h = pn.remaining_subgoals
-                                                   then unhead t
-                                                   else (h::t, None)
-                        in unhead pn.subgoals_stack)
-            in (fs, (ss, e_msg))
-          in
-          (Some { remaining_subgoals = rs;
-                  subgoals_stack = ss;
-                  first_step = fs;
-                },
-           e_msg)
-     in
-     let (s, m) = get_opened lstk in
-     { opened_sections = s;
-       opened_modules = m;
-       interp_mode = i_mode;
-     }, o_msg
-
-type nesting = {
-        module_levels : int;  (* number of opened modules *)
-        section_levels : int; (* number of opened sections *)
-        subgoal_levels : int; (* number of remaining subgoals *)
-        tactic_levels : int;  (* number of imbricated proofs *)
-        tactic_alinea : bool; (* are we entering a new node? *)
-}
-
-let compute_nesting pno =
-  let subgoals, tactic_depth, alinea =
-      match pno.interp_mode with
-        | None -> (0, 0, true)
-        | Some pn -> (pn.remaining_subgoals,
-                      List.length pn.subgoals_stack,
-                      pn.first_step)
-    in
-    { section_levels = pno.opened_sections;
-      module_levels = pno.opened_modules;
-      subgoal_levels = subgoals;
-      tactic_levels = tactic_depth;
-      tactic_alinea = alinea;
-    }
diff --git a/ide/indent.mli b/ide/indent.mli
deleted file mode 100644
index f57ca1d44e..0000000000
--- a/ide/indent.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* some data to have informations on how we can indent proofs *)
-type interp_node
-
-(* the default value of this data *)
-val first_interp_node : interp_node
-
-(* the function to compute our data *)
-val compute_interp_node :
-  Ide_blob.goals Ide_blob.value ->
-  interp_node -> Lib.library_segment Ide_blob.value -> interp_node * string option
-
-(* our data are abstract, so we need to get access to some of it informations to
- * use it; that is the aim of (compute_nesting)
- * *)
-type nesting = {
-  module_levels : int;
-  section_levels : int;
-  subgoal_levels : int;
-  tactic_levels : int;
-  tactic_alinea : bool;
-}
-val compute_nesting : interp_node -> nesting
diff --git a/ide/preferences.ml b/ide/preferences.ml
index aabedbe7ad..a6aaef2576 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -96,15 +96,6 @@ type pref =
       mutable lax_syntax : bool;
       mutable vertical_tabs : bool;
       mutable opposite_tabs : bool;
-(*
-      for indentation in proof mode
-*)
-      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;
 }
 
 let use_default_doc_url = "(automatic)"
@@ -161,13 +152,6 @@ let (current:pref ref) =
     lax_syntax = true;
     vertical_tabs = false;
     opposite_tabs = false;
-
-    indent_module_factor = 1;
-    indent_section_factor = 1;
-    indent_saw_factor = 1;
-    indent_was_factor = 3;
-    indent_was_alinea = 1;
-    indent_tactic_was_mode = false;
   }
 
 
@@ -235,14 +219,6 @@ let save_pref () =
     add "lax_syntax" [string_of_bool p.lax_syntax] ++
     add "vertical_tabs" [string_of_bool p.vertical_tabs] ++
     add "opposite_tabs" [string_of_bool p.opposite_tabs] ++
-
-    add "indent_module_factor" [string_of_int p.indent_module_factor] ++
-    add "indent_section_factor" [string_of_int p.indent_section_factor] ++
-    add "indent_saw_factor" [string_of_int p.indent_saw_factor] ++
-    add "indent_was_factor" [string_of_int p.indent_was_factor] ++
-    add "indent_was_alinea" [string_of_int p.indent_was_alinea] ++
-    add "indent_tactic_was_mode"
-         [string_of_bool p.indent_tactic_was_mode] ++
     Config_lexer.print_file pref_file
   with _ -> prerr_endline "Could not save preferences."
 
@@ -311,13 +287,6 @@ let load_pref () =
     set_bool "lax_syntax" (fun v -> np.lax_syntax <- v);
     set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v);
     set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v);
-    set_int "indent_module_factor" (fun v -> np.indent_module_factor <- v);
-    set_int "indent_section_factor" (fun v -> np.indent_section_factor <- v);
-    set_int "indent_saw_factor" (fun v -> np.indent_saw_factor <- v);
-    set_int "indent_was_factor" (fun v -> np.indent_was_factor <- v);
-    set_int "indent_was_alinea" (fun v -> np.indent_was_alinea <- v);
-    set_bool "indent_tactic_was_mode"
-        (fun v -> np.indent_tactic_was_mode <- v);
     current := np;
 (*
     Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
@@ -600,53 +569,6 @@ let configure ?(apply=(fun () -> ())) () =
       "Contextual menus on goal" !current.contextual_menus_on_goal
   in
 
-  let indent_module_factor =
-    string
-      ~f:(fun s -> let i = try int_of_string s with _ -> 1 in
-                   !current.indent_module_factor <- i)
-      "Modules depth dependent shifting for indentation"
-      (string_of_int !current.indent_module_factor)
-  in
-
-  let indent_section_factor =
-    string
-      ~f:(fun s -> let i = try int_of_string s with _ -> 1 in
-                   !current.indent_section_factor <- i)
-      "Sections depth dependent shifting for indentation"
-      (string_of_int !current.indent_section_factor)
-  in
-
-  let indent_saw_factor =
-    string
-      ~f:(fun s -> let i = try int_of_string s with _ -> 1 in
-                   !current.indent_saw_factor <- i)
-      "Shifting factor in \"saw mode\" (remaining subgoals dependent)"
-      (string_of_int !current.indent_saw_factor)
-  in
-
-  let indent_was_factor =
-    string
-      ~f:(fun s -> let i = try int_of_string s with _ -> 3 in
-                   !current.indent_was_factor <- i)
-      "Shifting factor in \"was mode\" (proof depth dependent)"
-      (string_of_int !current.indent_was_factor)
-  in
-
-  let indent_was_alinea =
-    string
-      ~f:(fun s -> let i = try int_of_string s with _ -> 1 in
-                   !current.indent_was_alinea <- i)
-      "Constant shift for stagnant subgoals (was mode)"
-      (string_of_int !current.indent_was_alinea)
-  in
-
-  let indent_tactic_was_mode =
-    bool
-      ~f:(fun s -> !current.indent_tactic_was_mode <- s)
-      "tactic mode : indentation in \"was mode\" instead of \"saw mode\""
-      !current.indent_tactic_was_mode
-  in
-
   let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax;
               vertical_tabs;opposite_tabs] in
 
@@ -672,12 +594,7 @@ let configure ?(apply=(fun () -> ())) () =
 	     [automatic_tactics]);
      Section("Shortcuts",
 	     [modifiers_valid; modifier_for_tactics;
-	      modifier_for_templates; modifier_for_display;
-              modifier_for_navigation]);
-     Section("Indentation",
-             [indent_module_factor; indent_section_factor;
-              indent_saw_factor; indent_was_factor; indent_was_alinea;
-              indent_tactic_was_mode]);
+	      modifier_for_templates; modifier_for_display; modifier_for_navigation]);
      Section("Misc",
 	     misc)]
   in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 723a771b00..41a581d574 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -55,15 +55,6 @@ 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
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index 6ef45a4429..7e7834743f 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -514,7 +514,6 @@ let explain_exn e =
   in
   toploc,(Cerrors.explain_exn exc)
 
-let contents () = Lib.contents_after None
 
 (**
  * Wrappers around Coq calls. We use phantom types and GADT to protect ourselves
@@ -530,7 +529,6 @@ type 'a call =
   | Cur_goals
   | Cur_status
   | Cases of string
-  | Contents
 
 type 'a value =
   | Good of 'a
@@ -550,9 +548,7 @@ let eval_call c =
               | Read_stdout -> Obj.magic (read_stdout ())
               | Cur_goals -> Obj.magic (current_goals ())
               | Cur_status -> Obj.magic (current_status ())
-              | Cases s -> Obj.magic (make_cases s)
-              | Contents -> Obj.magic (contents ())
-              )
+              | Cases s -> Obj.magic (make_cases s))
   with e ->
     let (l,pp) = explain_exn (filter_compat_exn e) in
     (* force evaluation of format stream *)
@@ -582,9 +578,6 @@ let current_status : string call =
 let make_cases s : string list list call =
   Cases s
 
-let contents : Lib.library_segment call =
-  Contents
-
 (* End of wrappers *)
 
 let loop () =
diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli
index b1261e4966..34879f0577 100644
--- a/toplevel/ide_blob.mli
+++ b/toplevel/ide_blob.mli
@@ -43,6 +43,4 @@ val current_goals : goals call
 
 val read_stdout : string call
 
-val contents : Lib.library_segment call
-
 val loop : unit -> unit