- Prise en compte des frozen state de Coq autant que possible pour

  améliorer l'efficacité du undo. Restent les Qed et les End dont le
  undo peut nécessiter de rejouer un segment arbitrairement complexe
  (pour le undo du Qed, il faudrait typiquement que Coq se souvienne
  de l'entrelacement de déclarations et de tactiques).
- Code mort concernant les mots-clés dans coq.ml.


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

5 files changed, 135 insertions, 115 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 4e0150918..17f80b0ec 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -271,6 +271,57 @@ let is_vernac_state_preserving_command com =
 let is_vernac_tactic_command com =
   List.mem SolveCommand (attribute_of_vernac_command com)
 
+type reset_mark =
+  | ResetToId of Names.identifier
+  | ResetToState of  Libnames.object_name
+
+type reset_info =
+  | NoReset
+  | ResetAtDecl of reset_mark * bool ref
+  | ResetAtSegmentStart of Names.identifier * bool ref 
+  | ResetAtFrozenState of Libnames.object_name * bool ref
+
+let reset_mark id = match Lib.has_top_frozen_state () with
+  | Some sp -> ResetToState sp
+  | None -> ResetToId id
+
+let compute_reset_info = function 
+  | VernacBeginSection id 
+  | VernacDefineModule (_,id, _, _, _) 
+  | VernacDeclareModule (_,id, _, _)
+  | VernacDeclareModuleType (id, _, _) ->
+      ResetAtSegmentStart (snd id, ref true)
+
+  | VernacDefinition (_, (_,id), DefineBody _, _)
+  | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
+  | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
+      ResetAtDecl (reset_mark id, ref true)
+
+  | VernacDefinition (_, (_,id), ProveBody _, _)
+  | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
+      ResetAtDecl (reset_mark id, ref false)
+
+  | VernacEndProof _ -> NoReset
+  | _ -> match Lib.has_top_frozen_state () with
+      | Some sp -> ResetAtFrozenState (sp, ref true)
+      | None -> NoReset
+
+let reset_initial () = 
+  prerr_endline "Reset initial called"; flush stderr;
+  Vernacentries.abort_refine Lib.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)
+  | ResetToState sp ->
+      Vernacentries.abort_refine 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)
+
+
 let interp verbosely s = 
   prerr_endline "Starting interp...";
   prerr_endline s;
@@ -291,10 +342,11 @@ let interp verbosely s =
 	if not (is_vernac_goal_printing_command vernac) then
 	  (* Verbose if in small step forward and not a tactic *)
 	  Flags.make_silent (not verbosely);
+	let reset_info = compute_reset_info vernac in
 	Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
 	Flags.make_silent true;
 	prerr_endline ("...Done with interp of : "^s);
-	last
+	reset_info,last
 
 let interp_and_replace s = 
   let result = interp false s in
@@ -425,79 +477,6 @@ let print_no_goal () =
     msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls)
 
 
-type word_class = Normal | Kwd | Reserved
-
-
-let kwd = [(* "Compile";"Inductive";"Qed";"Type";"end";"Axiom";
-	      "Definition";"Load";"Quit";"Variable";"in";"Cases";"FixPoint";
-	      "Parameter";"Set";"of";"CoFixpoint";"Grammar";"Proof";"Syntax";
-	      "using";"CoInductive";"Hypothesis";"Prop";"Theorem";
-	   *)
-  "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
-  "CoInductive"; "Defined"; "Definition"; 
-  "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
-  "Hypothesis"; "Immediate"; "Implicits"; "Import"; "Inductive"; 
-  "Infix"; "Lemma"; "Load"; "Local"; 
-  "Match"; "Module"; "Module Type";
-  "Mutual"; "Parameter"; "Print"; "Proof"; "Qed";
-  "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
-  "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
-  "Unset"; "Variable"; "Variables"; 
-]
-	    
-let reserved = []
-
-module SHashtbl = 
-  Hashtbl.Make 
-    (struct 
-       type t = string
-       let equal = ( = )
-       let hash = Hashtbl.hash
-     end)
-
-
-let word_tbl = SHashtbl.create 37
-let _ = 
-  List.iter (fun w -> SHashtbl.add word_tbl w Kwd) kwd;
-  List.iter (fun w -> SHashtbl.add word_tbl w Reserved) reserved
-
-let word_class s = 
-  try
-    SHashtbl.find word_tbl s
-  with Not_found -> Normal
-
-type reset_info =
-  | NoReset
-  | ResetAtDecl of Names.identifier * bool ref 
-  | ResetAtSegmentStart of Names.identifier * bool ref
-
-let compute_reset_info = function 
-  | VernacBeginSection id 
-  | VernacDefineModule (_,id, _, _, _) 
-  | VernacDeclareModule (_,id, _, _)
-  | VernacDeclareModuleType (id, _, _) ->
-      ResetAtSegmentStart (snd id, ref true)
-  | VernacDefinition (_, (_,id), DefineBody _, _)
-  | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
-  | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
-      ResetAtDecl (id, ref true)
-  | VernacDefinition (_, (_,id), ProveBody _, _)
-  | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
-      ResetAtDecl (id, ref false)
-  | _ -> NoReset
-
-let reset_initial () = 
-  prerr_endline "Reset initial called"; flush stderr;
-  Vernacentries.abort_refine Lib.reset_initial ()
-
-let reset_to id = 
-  prerr_endline ("Reset called with "^(string_of_id id));
-  Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id)
-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)
-
-
 let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
   [("clear "^ident),("clear "^ident^".");
    
diff --git a/ide/coq.mli b/ide/coq.mli
index 9c8e27320..5ded2b573 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -15,10 +15,26 @@ open Evd
 
 val version : unit -> string
 
+type reset_mark =
+  | ResetToId of Names.identifier
+  | ResetToState of  Libnames.object_name
+
+type reset_info =
+  | NoReset
+  | ResetAtDecl of reset_mark * bool ref
+  | ResetAtSegmentStart of Names.identifier * bool ref 
+  | ResetAtFrozenState of Libnames.object_name * bool ref
+
+val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
+val reset_initial : unit -> unit
+val reset_to : reset_mark -> unit
+val reset_to_mod : identifier -> unit
+
 val init : unit -> string list 
-val interp : bool -> string -> Util.loc * Vernacexpr.vernac_expr
+val interp : bool -> string -> reset_info * (Util.loc * Vernacexpr.vernac_expr)
 val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
-val interp_and_replace : string -> (Util.loc * Vernacexpr.vernac_expr) * string
+val interp_and_replace : string -> 
+      (reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string
 
 val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool
 val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool
@@ -42,16 +58,6 @@ val print_no_goal : unit -> string
 
 val process_exn : exn -> string*(Util.loc option)
 
-type reset_info =
-  | NoReset
-  | ResetAtDecl of Names.identifier * bool ref 
-  | ResetAtSegmentStart of Names.identifier * bool ref
-
-val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
-val reset_initial : unit -> unit
-val reset_to : identifier -> unit
-val reset_to_mod : identifier -> unit
-
 val hyp_menu : hyp -> (string * string) list
 val concl_menu : concl -> (string * string) list
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 7cfeb694d..4e5223b02 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -159,7 +159,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 -> Names.identifier option -> unit
+  method backtrack_to_no_lock : GText.iter -> reset_mark option -> unit
   method clear_message : unit
   method deactivate : unit -> unit
   method disconnected_keypress_handler : GdkEvent.Key.t -> bool
@@ -182,7 +182,8 @@ object('self)
   method reset_initial : unit
   method send_to_coq :
     bool -> bool -> string ->
-    bool -> bool -> bool -> (bool*(Util.loc * Vernacexpr.vernac_expr)) option
+    bool -> bool -> bool ->
+    (bool*(reset_info*(Util.loc * Vernacexpr.vernac_expr))) option
   method set_message : string -> unit
   method show_pm_goal : unit
   method show_goals : unit
@@ -502,6 +503,9 @@ let is_empty () = Stack.is_empty processed_stack
 
 let update_on_end_of_proof () =
   let lookup_lemma = function
+    | { reset_info = ResetAtFrozenState (_, r) } -> 
+	prerr_endline "Toggling Frozen State info to false";
+	r := false
     | { reset_info = ResetAtDecl (_, r) } ->
 	if not !r then begin
 	    prerr_endline "Toggling Reset info to true";
@@ -521,15 +525,16 @@ let update_on_end_of_segment id =
     | { reset_info = ResetAtSegmentStart (id', r) } when id = id' -> raise Exit
     | { reset_info = ResetAtSegmentStart (_, r) } -> r := false
     | { reset_info = ResetAtDecl (_, r) } -> r := false
+    | { reset_info = ResetAtFrozenState (_, r) } -> r := false
     | _ -> ()
   in
     try Stack.iter lookup_section processed_stack with Exit -> ()
 
-let push_phrase start_of_phrase_mark end_of_phrase_mark ast = 
+let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast = 
   let x = {start = start_of_phrase_mark;
 	   stop = end_of_phrase_mark;
 	   ast = ast;
-	   reset_info = Coq.compute_reset_info (snd ast)
+	   reset_info = reset_info
 	  } in
   begin
     match snd ast with
@@ -540,8 +545,8 @@ let push_phrase start_of_phrase_mark end_of_phrase_mark ast =
   push x
 
 
-let repush_phrase x =
-  let x = { x with reset_info = Coq.compute_reset_info (snd x.ast) } in
+let repush_phrase reset_info x =
+  let x = { x with reset_info = reset_info } in
   begin
     match snd x.ast with
       | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof ()
@@ -1143,7 +1148,7 @@ object(self)
 	  input_view#set_editable true;
 	  !pop_info ();
 	end in
-      let mark_processed complete (start,stop) ast =
+      let mark_processed reset_info complete (start,stop) ast =
         let b = input_buffer in
 	b#move_mark ~where:stop (`NAME "start_of_input");
 	b#apply_tag_by_name 
@@ -1155,7 +1160,8 @@ object(self)
 	  end;
 	let start_of_phrase_mark = `MARK (b#create_mark start) in
 	let end_of_phrase_mark = `MARK (b#create_mark stop) in
-	push_phrase 
+	push_phrase
+          reset_info 
 	  start_of_phrase_mark 
 	  end_of_phrase_mark ast;
 	if display_goals then self#show_goals;
@@ -1165,14 +1171,14 @@ object(self)
             None -> false
           | Some (loc,phrase) ->
             (match self#send_to_coq verbosely false phrase true true true with
-	      | Some (complete,ast) -> 
-		  sync (mark_processed complete) loc ast; true
+	      | Some (complete,(reset_info,ast)) -> 
+		  sync (mark_processed reset_info complete) loc ast; true
 	      | None -> sync remove_tag loc; false)
       end
     
   method insert_this_phrase_on_success 
     show_output show_msg localize coqphrase insertphrase = 
-    let mark_processed complete ast =
+    let mark_processed reset_info complete ast =
       let stop = self#get_start_of_input in
       if stop#starts_line then
 	input_buffer#insert ~iter:stop insertphrase
@@ -1185,7 +1191,7 @@ object(self)
 	input_buffer#place_cursor stop;
       let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in
       let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
-      push_phrase start_of_phrase_mark end_of_phrase_mark ast;
+      push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast;
       self#show_goals;
       (*Auto insert save on success... 
       try (match Coq.get_current_goals () with 
@@ -1206,13 +1212,15 @@ object(self)
                       `MARK (input_buffer#create_mark start) in
 	            let end_of_phrase_mark =
                       `MARK (input_buffer#create_mark stop) in
-	            push_phrase start_of_phrase_mark end_of_phrase_mark ast
+	            push_phrase
+	              reset_info start_of_phrase_mark end_of_phrase_mark ast
 	          end
 	      | None -> ())
 	| _ -> ())
       with _ -> ()*) in
     match self#send_to_coq false false coqphrase show_output show_msg localize with
-      | Some (complete,ast) -> sync (mark_processed complete) ast; true
+      | Some (complete,(reset_info,ast)) ->
+	  sync (mark_processed reset_info complete) ast; true
       | None ->
           sync
             (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
@@ -1284,28 +1292,35 @@ object(self)
 	    begin match t.reset_info with
 	      | ResetAtSegmentStart (id, {contents=true}) ->
 		  reset_to_mod id
-	      | ResetAtDecl (id, {contents=true}) ->
+	      | ResetAtFrozenState (sp, {contents=true}) ->
 		  if inproof then
-		    (prerr_endline ("Skipping "^Names.string_of_id id);
-		    synchro (Some id) inproof)
+		    synchro (Some (ResetToState sp)) inproof
 		  else
-		    reset_to (Option.default id oldest_decl_in_middle_of_proof)
-	      | ResetAtDecl (id, {contents=false}) ->
+		    reset_to (ResetToState sp)
+	      | ResetAtDecl (mark, {contents=true}) ->
+		  if inproof then
+		    synchro (Some mark) inproof
+		  else
+		    reset_to
+		      (Option.default mark oldest_decl_in_middle_of_proof)
+	      | ResetAtDecl (mark, {contents=false}) ->
 		  if inproof then
 		    if oldest_decl_in_middle_of_proof = None then
-		      synchro None false
+		      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
-		    (prerr_endline ("Skipping "^Names.string_of_id id);
-		    synchro (Some id) inproof)
+		    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 t
+	    repush_phrase reset_info t
 	end
     in
     let add_undo t = match t with | Some n -> Some (succ n) | None -> None
@@ -1400,23 +1415,25 @@ Please restart and report NOW.";
 	    in
 	      begin match last_command with 
 		| {ast=_,com} when is_vernac_tactic_command com -> 
-prerr_endline "TACT";
 		    begin 
 		      try Pfedit.undo 1; ignore (pop ()); sync update_input () 
 		      with _ -> self#backtrack_to_no_lock start None
 		    end
 
+		| {reset_info=ResetAtFrozenState (sp, {contents=true})} ->
+		    ignore (pop ());
+		    Lib.reset_to_state sp;
+		    sync update_input ()
 		| {reset_info=ResetAtSegmentStart (id, {contents=true})} ->
-prerr_endline "SEG";
 		    ignore (pop ());
 		    reset_to_mod id;
 		    sync update_input ()
-		| {reset_info=ResetAtDecl (id, {contents=true})} ->
+		| {reset_info=ResetAtDecl (mark, {contents=true})} ->
 		    if Pfedit.refining () then
-		      self#backtrack_to_no_lock start (Some id)
+		      self#backtrack_to_no_lock start (Some mark)
 		    else
-		      (ignore (pop ()); reset_to id; sync update_input ())
-		| {reset_info=ResetAtDecl (id,{contents=false})} ->
+		      (ignore (pop ()); reset_to mark; sync update_input ())
+		| {reset_info=ResetAtDecl (_, {contents=false})} ->
 		    ignore (pop ());
 		    (try 
 			 Pfedit.delete_current_proof () 
diff --git a/library/lib.ml b/library/lib.ml
index ae1a41ca1..5e22c4d22 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -584,6 +584,13 @@ let recache_context ctx =
 
 let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
 
+let has_top_frozen_state () =
+  let rec aux = function
+  | (sp, FrozenState _)::_ -> Some sp
+  | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t
+  | _ -> None
+  in aux !lib_stk 
+
 let set_lib_stk new_lib_stk =
   lib_stk := new_lib_stk;
   recalc_path_prefix ();
@@ -603,6 +610,14 @@ let reset_to_gen test =
 
 let reset_to sp = reset_to_gen (fun x -> (fst x) = sp)
 
+let reset_to_state sp =
+  let (_,eq,before) = split_lib sp in
+  (* if eq a frozen state, we'll reset to it *)
+  match eq with
+  | [_,FrozenState f] -> lib_stk := eq@before;  unfreeze_summaries f
+  | _ -> error "Not a frozen state"
+
+
 (* LEM: TODO
  * We will need to muck with frozen states in after, too!
  * Not only FrozenState, but also those embedded in Opened(Section|Module|Modtype)
diff --git a/library/lib.mli b/library/lib.mli
index da8ace048..f3fa9a4b3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -145,6 +145,9 @@ val reset_to : object_name -> unit
 val reset_name : identifier located -> unit
 val remove_name : identifier located -> unit
 val reset_mod : identifier located -> unit
+val reset_to_state : object_name -> unit
+
+val has_top_frozen_state : unit -> object_name option
 
 (* [back n] resets to the place corresponding to the $n$-th call of 
    [mark_end_of_command] (counting backwards) *)