- On adopte finalement la méthode de Pierre Courtieu pour le undo de

  proof general (caractérisation des undos comme triplet d'un nombre de
  Undo, n'un nombre de Abort et d'un Reset vers un état/id).
  C'est plus simple et cela permet en plus d'avoir des buts imbriqués.
  Au passage, "goto point" se comporte comme une suite de "one step back".
- Quelques bricoles sur la fenêtre préférences de Shortcuts.
- Quelques réorganisations autour du menu Display.


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

4 files changed, 109 insertions, 125 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index f45bd9f5c..dc4594292 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -172,7 +172,7 @@ let make_option_commands () =
   (if p.printing_coercions then [with_printing_coercions] else [])@
   (if p.printing_raw_matching then [with_printing_raw_matching;with_printing_no_synth] else [])@
   (if p.printing_no_notation then [with_printing_no_notation] else [])@
-  (if p.printing_all then [with_printing_all] else [])@
+  (if p.printing_all then [with_printing_all;with_printing_evar_instances;with_printing_universes] else [])@
   (if p.printing_evar_instances then [with_printing_evar_instances] else [])@
   (if p.printing_universes then [with_printing_universes] else [])
 
@@ -353,7 +353,7 @@ type reset_mark =
 type reset_info =
   | NoReset
   | ResetAtSegmentStart of Names.identifier * bool ref 
-  | ResetAtStatement of reset_mark * bool ref
+  | ResetAtStatement of bool ref
   | ResetAtRegisteredObject of reset_mark * bool ref
 
 let reset_mark id = match Lib.has_top_frozen_state () with
@@ -371,13 +371,11 @@ let compute_reset_info = function
   | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
   | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
       ResetAtRegisteredObject (reset_mark id, ref true)
-
-  | VernacDefinition (_, (_,id), ProveBody _, _)
-  | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
-      ResetAtStatement (reset_mark id, ref false)
-
   | VernacEndProof _ | VernacExactProof _ | VernacEndSegment _ -> NoReset
-  | com -> if is_vernac_tactic_command com then NoReset else
+  | com when is_vernac_goal_starting_command com ->
+      ResetAtStatement (ref false)
+  | com when is_vernac_tactic_command com -> NoReset
+  | _ ->
       match Lib.has_top_frozen_state () with
       | Some sp -> ResetAtRegisteredObject (ResetToState sp, ref true)
       | None -> NoReset
@@ -389,15 +387,15 @@ let reset_initial () =
 let reset_to = function
   | ResetToId id ->
       prerr_endline ("Reset called with "^(string_of_id id));
-      Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id)
+      Lib.reset_name (Util.dummy_loc,id)
   | ResetToState sp ->
       prerr_endline
         ("Reset called with state "^(Libnames.string_of_path (fst sp)));
-      Vernacentries.abort_refine Lib.reset_to_state sp
+      Lib.reset_to_state sp
 
 let reset_to_mod id = 
   prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); 
-  Vernacentries.abort_refine Lib.reset_mod (Util.dummy_loc,id)
+  Lib.reset_mod (Util.dummy_loc,id)
 
 let raw_interp s =
   Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s))
@@ -410,14 +408,12 @@ let interp_with_options verbosely options s =
   match pe with 
     | None -> assert false
     | Some((loc,vernac) as last) ->
-	if is_vernac_goal_starting_command vernac & is_in_proof_mode () then
-	  user_error_loc loc (str "CoqIDE do not support nested goals");
 	if is_vernac_debug_command vernac then
 	  user_error_loc loc (str "Debug mode not available within CoqIDE");
 	if is_vernac_navigation_command vernac then
 	  user_error_loc loc (str "Use CoqIDE navigation instead");
 	if is_vernac_known_option_command vernac then
-	  user_error_loc loc (str "Use CoqIDE buttons instead");
+	  user_error_loc loc (str "Use CoqIDE display menu instead");
 	if is_vernac_query_command vernac then 
 	  !flash_info
 	    "Warning: query commands should not be inserted in scripts";
diff --git a/ide/coq.mli b/ide/coq.mli
index 930687eae..cec86ab78 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -35,7 +35,7 @@ type reset_mark =
 type reset_info =
   | NoReset
   | ResetAtSegmentStart of Names.identifier * bool ref 
-  | ResetAtStatement of reset_mark * bool ref
+  | ResetAtStatement of bool ref
   | ResetAtRegisteredObject of reset_mark * bool ref
 
 val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
diff --git a/ide/coqide.ml b/ide/coqide.ml
index a0ea02523..6ac5c779b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -160,7 +160,7 @@ object('self)
   method activate : unit -> unit
   method active_keypress_handler : GdkEvent.Key.t -> bool
   method backtrack_to : GText.iter -> unit
-  method backtrack_to_no_lock : GText.iter -> reset_mark option -> unit
+  method backtrack_to_no_lock : GText.iter -> unit
   method clear_message : unit
   method deactivate : unit -> unit
   method disconnected_keypress_handler : GdkEvent.Key.t -> bool
@@ -507,7 +507,7 @@ let update_on_end_of_proof () =
     | { reset_info = ResetAtRegisteredObject (_, r) } -> 
 	prerr_endline "Toggling Frozen State info to false";
 	r := false
-    | { reset_info = ResetAtStatement (_, r) } when not !r ->
+    | { reset_info = ResetAtStatement r } when not !r ->
 	prerr_endline "Toggling Reset info to true";
 	r := true; raise Exit
     | { ast = _, (VernacAbort _ | VernacAbortAll | VernacGoal _) } -> raise Exit
@@ -519,7 +519,7 @@ let update_on_end_of_segment id =
   let lookup_section = function 
     | { reset_info = ResetAtSegmentStart (id', r) } when id = id' -> raise Exit
     | { reset_info = ResetAtSegmentStart (_, r) } -> r := false
-    | { reset_info = ResetAtStatement (_, r) } -> r := false
+    | { reset_info = ResetAtStatement r } -> r := false
     | { reset_info = ResetAtRegisteredObject (_, r) } -> r := false
     | _ -> ()
   in
@@ -550,6 +550,66 @@ let repush_phrase reset_info x =
   end;
   push x
 
+type backtrack =
+| BacktrackToNextActiveMark
+| BacktrackToMark of reset_mark
+| BacktrackToModSec of Names.identifier
+| NoBacktrack
+
+let add_undo (n,a,b) = (n+1,a,b)
+let add_abort (n,a,b) = (n,a+1,b)
+let add_backtrack (n,a,b) b' = (n,a,b')
+
+let pop_command undos t =
+  let undos = 
+    match t with
+    | {ast=(_,com)} when is_vernac_tactic_command com ->
+        add_undo undos
+    | {reset_info=ResetAtRegisteredObject (mark,{contents=true})} ->
+        add_backtrack undos (BacktrackToMark mark)
+    | {reset_info=ResetAtSegmentStart (id, {contents=true})} ->
+        add_backtrack undos (BacktrackToModSec id)
+    | {reset_info=ResetAtStatement {contents=false}} ->
+	prerr_endline ("Statement " ^ if Pfedit.refining () then "proof" else "none");
+        if Pfedit.refining () then add_abort undos
+        else add_backtrack undos BacktrackToNextActiveMark
+    | {ast=(_,com)} ->
+        if is_vernac_state_preserving_command com then undos
+        else add_backtrack undos BacktrackToNextActiveMark in
+  ignore (pop ());
+  undos
+
+let rec apply_backtrack = function
+  | BacktrackToMark mark -> reset_to mark
+  | NoBacktrack -> ()
+  | BacktrackToModSec id -> reset_to_mod id
+  | BacktrackToNextActiveMark ->
+      (* re-synchronize Coq to the current state of the stack *)
+      if is_empty () then
+        Coq.reset_initial ()
+      else
+        begin
+          let t = top () in
+          let (_,_,b) = pop_command (0,0,BacktrackToNextActiveMark) t in
+          apply_backtrack b;
+          let reset_info = Coq.compute_reset_info (snd t.ast) in
+          interp_last t.ast;
+          repush_phrase reset_info t
+        end
+
+let rec apply_undos (n,a,b) =
+  (* Undos *)
+  if n<>0 then 
+    (prerr_endline ("Applying "^string_of_int n^" undos");
+     try Pfedit.undo n
+     with _ -> apply_undos (n,a,BacktrackToNextActiveMark));
+  (* Aborts *)
+  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
+  (try Util.repeat a Pfedit.delete_current_proof ()
+   with e ->
+     begin prerr_endline "WARNING : found a closed environment"; raise e end);
+  (* Reset *)
+  apply_backtrack b
 
 (* For electric handlers *)
 exception Found
@@ -1275,71 +1335,28 @@ object(self)
     Coq.reset_initial ()
 
   (* backtrack Coq to the phrase preceding iterator [i] *)
-  method backtrack_to_no_lock i oldest_id_to_reset =
+  method backtrack_to_no_lock i =
     prerr_endline "Backtracking_to iter starts now.";
-    let was_refining = Pfedit.refining () in
-    (* re-synchronize Coq to the current state of the stack *)
-    let rec synchro oldest_decl_in_middle_of_proof inproof =
-      if is_empty () then
-	Coq.reset_initial ()
-      else begin
-	  let t = pop () in
-	    begin match t.reset_info with
-	      | ResetAtSegmentStart (id, {contents=true}) ->
-		  reset_to_mod id
-	      | ResetAtRegisteredObject (mark, {contents=true}) ->
-		  if inproof then synchro (Some mark) inproof
-		  else reset_to mark
-	      | ResetAtStatement (mark, {contents=true}) ->
-		  assert (not inproof);
-		  reset_to (Option.default mark oldest_decl_in_middle_of_proof)
-	      | ResetAtStatement (mark, {contents=false}) ->
-		  if inproof then
-		    if oldest_decl_in_middle_of_proof = None then
-		      match mark with
-		      | ResetToId _ -> synchro None false
-		      | ResetToState _ -> reset_to mark 
-		    else
-		      (* reset oldest decl found before theorem started what *)
-		      (* resets back just before the proof was started *)
-		      reset_to (Option.get oldest_decl_in_middle_of_proof)
-		  else
-		    synchro (Some mark) inproof
-	      | _ ->
-		  synchro oldest_decl_in_middle_of_proof inproof
-	    end;
-	    let reset_info = Coq.compute_reset_info (snd t.ast) in
-	    interp_last t.ast;
-	    repush_phrase reset_info t
-	end
-    in
-    let add_undo t = match t with | Some n -> Some (succ n) | None -> None
-    in
-      (* pop Coq commands until we reach iterator [i] *)
+    (* pop Coq commands until we reach iterator [i] *)
     let  rec pop_commands done_smthg undos =
       if is_empty () then 
 	done_smthg, undos
       else
 	let t = top () in 
-	  if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then begin
+	if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then
+          begin
 	    prerr_endline "Popped top command";
-	      ignore (pop ());
-	      let undos =
-		if is_vernac_tactic_command (snd t.ast) then add_undo undos
-		else None in
-	      pop_commands true undos
-	    end else
-	    done_smthg, undos
+	    pop_commands true (pop_command undos t)
+	  end
+        else
+	  done_smthg, undos
     in
-    let done_smthg, undos = pop_commands false (Some 0) in
+    let done_smthg, undos = pop_commands false (0,0,NoBacktrack) in
       prerr_endline "Popped commands";
       if done_smthg then
-	begin 
-	  try 
-	    (match undos with 
-	       | None -> synchro oldest_id_to_reset was_refining
-	       | Some n -> try Pfedit.undo n with _ -> 
-		   synchro oldest_id_to_reset was_refining);
+        begin 
+          try 
+            apply_undos undos;
             sync (fun _ ->
 		    let start =
 		      if is_empty () then input_buffer#start_iter 
@@ -1368,7 +1385,7 @@ Please restart and report NOW.";
   method backtrack_to i = 
     if Mutex.try_lock coq_may_stop then 
       (!push_info "Undoing...";
-       self#backtrack_to_no_lock i None; Mutex.unlock coq_may_stop;
+       self#backtrack_to_no_lock i; Mutex.unlock coq_may_stop;
        !pop_info ())
     else prerr_endline "backtrack_to : discarded (lock is busy)"
 
@@ -1403,38 +1420,9 @@ Please restart and report NOW.";
 	      self#show_goals;
 	      self#clear_message
 	    in
-	      begin match last_command with 
-		| {ast=_,com} when is_vernac_tactic_command com -> 
-		    begin 
-		      try Pfedit.undo 1; ignore (pop ()); sync update_input () 
-		      with _ -> self#backtrack_to_no_lock start None
-		    end
-
-		| {reset_info=ResetAtRegisteredObject (mark,{contents=true})} ->
-		    if Pfedit.refining () then
-		      self#backtrack_to_no_lock start (Some mark)
-		    else
-		      (ignore (pop ()); reset_to mark; sync update_input ())
-		| {reset_info=ResetAtSegmentStart (id, {contents=true})} ->
-		    ignore (pop ());
-		    reset_to_mod id;
-		    sync update_input ()
-		| {reset_info=ResetAtStatement (_, {contents=false})} ->
-		    ignore (pop ());
-		    (try 
-			 Pfedit.delete_current_proof () 
-		     with e ->
-		       begin 
-			 prerr_endline "WARNING : found a closed environment";
-			 raise e
-		       end);
-		    sync update_input ()
-		| { ast = (_, a) } when is_vernac_state_preserving_command a ->
-		    ignore (pop ());
-		    sync update_input ()
-		| _ -> 
-		    self#backtrack_to_no_lock start None
-	      end;
+              let undo = pop_command (0,0,NoBacktrack) last_command in
+              apply_undos undo;
+              sync update_input ()
 	with
 	  | Size 0 -> (* !flash_info "Nothing to Undo"*)()
        );
@@ -2887,40 +2875,39 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					  in
 
 					  let _ = ignore (view_factory#add_check_item 
-							    "Toggle printing of _implicit arguments" 
+							    "Display _implicit arguments" 
 							    ~key:GdkKeysyms._i
 							    ~callback:(fun _ -> printing_state.printing_implicit <- not printing_state.printing_implicit; do_or_activate (fun a -> a#show_goals) ())) in
 
 					  let _ = ignore (view_factory#add_check_item 
-							    "Toggle printing of _coercions"
+							    "Display _coercions"
 							    ~key:GdkKeysyms._c
 							    ~callback:(fun _ -> printing_state.printing_coercions <- not printing_state.printing_coercions; do_or_activate (fun a -> a#show_goals) ())) in
 
 					  let _ = ignore (view_factory#add_check_item
-							    "Toggle printing of raw _matching expressions"
+							    "Display raw _matching expressions"
 							    ~key:GdkKeysyms._m
 							    ~callback:(fun _ -> printing_state.printing_raw_matching <- not printing_state.printing_raw_matching; do_or_activate (fun a -> a#show_goals) ())) in
 
 					  let _ = ignore (view_factory#add_check_item  
-							    "Toggle deactivation of _notations"
+							    "Deactivate _notations display"
 							    ~key:GdkKeysyms._n
 							    ~callback:(fun _ -> printing_state.printing_no_notation <- not printing_state.printing_no_notation; do_or_activate (fun a -> a#show_goals) ())) in
 
-					  let _ = ignore (view_factory#add_check_item  
-							    "Toggle _full low-level printing"
-							    ~key:GdkKeysyms._f
-							    ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in 
-					   
 					  let _ = ignore (view_factory#add_check_item     
-							    "Toggle printing of _existential variable instances"
+							    "Display _existential variable instances"
 							    ~key:GdkKeysyms._e
 					    		    ~callback:(fun _ -> printing_state.printing_evar_instances <- not printing_state.printing_evar_instances; do_or_activate (fun a -> a#show_goals) ())) in
 
 					  let _ = ignore (view_factory#add_check_item  
-							    "Toggle printing of _universe levels"
+							    "Display _universe levels"
 							    ~key:GdkKeysyms._u
 					    		    ~callback:(fun _ -> printing_state.printing_universes <- not printing_state.printing_universes; do_or_activate (fun a -> a#show_goals) ())) in
 
+					  let _ = ignore (view_factory#add_check_item  
+							    "Display _all low-level contents"
+							    ~key:GdkKeysyms._a
+							    ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in 
 
 					  (* Unicode *)
 (*
@@ -3073,7 +3060,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					  let configuration_menu = factory#add_submenu "_Windows" in
 					  let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"<CoqIde MenuBar>/Windows" ~accel_group
 					  in
-					  let _ = 
+					  let _ =
 					    configuration_factory#add_check_item 
 					      "Show/Hide _Query Pane"
 					      (*
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 802a0c1fe..253c56788 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -453,10 +453,14 @@ let configure ?(apply=(fun () -> ())) () =
       (if !current.encoding_use_utf8 then "UTF-8" 
        else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual)
   in
+  let help_string = 
+    "Press a set of modifiers and an extra key together (needs then a restart to apply!)"
+  in
   let modifier_for_tactics = 
     modifiers
       ~allow:!current.modifiers_valid
       ~f:(fun l -> !current.modifier_for_tactics <- l)
+      ~help:help_string
       "Modifiers for Tactics Menu"
       !current.modifier_for_tactics
   in
@@ -464,6 +468,7 @@ let configure ?(apply=(fun () -> ())) () =
     modifiers
       ~allow:!current.modifiers_valid
       ~f:(fun l -> !current.modifier_for_templates <- l)
+      ~help:help_string
       "Modifiers for Templates Menu"
       !current.modifier_for_templates
   in
@@ -471,6 +476,7 @@ let configure ?(apply=(fun () -> ())) () =
     modifiers
       ~allow:!current.modifiers_valid
       ~f:(fun l -> !current.modifier_for_navigation <- l)
+      ~help:help_string
       "Modifiers for Navigation Menu"
       !current.modifier_for_navigation
   in
@@ -478,6 +484,7 @@ let configure ?(apply=(fun () -> ())) () =
     modifiers
       ~allow:!current.modifiers_valid
       ~f:(fun l -> !current.modifier_for_display <- l)
+      ~help:help_string
       "Modifiers for Display Menu"
       !current.modifier_for_display
   in
@@ -487,12 +494,6 @@ let configure ?(apply=(fun () -> ())) () =
       "Allowed modifiers"
       !current.modifiers_valid
   in
-  let mod_msg = 
-    string
-      "Needs restart to apply!"
-      ~editable:false
-      ""
-  in
   let cmd_editor = 
     let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in
     combo
@@ -570,7 +571,7 @@ let configure ?(apply=(fun () -> ())) () =
 	     [automatic_tactics]);
      Section("Shortcuts",
 	     [modifiers_valid; modifier_for_tactics;
-	      modifier_for_templates; modifier_for_display; modifier_for_navigation;mod_msg]);
+	      modifier_for_templates; modifier_for_display; modifier_for_navigation]);
      Section("Misc",
 	     misc)]
   in