debug reset

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

8 files changed, 52 insertions, 32 deletions

diff --git a/.depend b/.depend
index da97bf991..d45d94eab 100644
--- a/.depend
+++ b/.depend
@@ -844,14 +844,14 @@ toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmi \
     lib/options.cmx lib/pp.cmx lib/system.cmx toplevel/toplevel.cmx \
     toplevel/vernac.cmx toplevel/coqinit.cmi 
 toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
-    toplevel/errors.cmi library/library.cmi toplevel/mltop.cmi \
-    lib/options.cmi lib/pp.cmi parsing/printer.cmi lib/profile.cmi \
-    library/states.cmi lib/system.cmi toplevel/toplevel.cmi \
+    toplevel/errors.cmi library/lib.cmi library/library.cmi \
+    toplevel/mltop.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \
+    lib/profile.cmi library/states.cmi lib/system.cmi toplevel/toplevel.cmi \
     toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi 
 toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
-    toplevel/errors.cmx library/library.cmx toplevel/mltop.cmi \
-    lib/options.cmx lib/pp.cmx parsing/printer.cmx lib/profile.cmx \
-    library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
+    toplevel/errors.cmx library/lib.cmx library/library.cmx \
+    toplevel/mltop.cmi lib/options.cmx lib/pp.cmx parsing/printer.cmx \
+    lib/profile.cmx library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
     toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx 
 toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \
     kernel/constant.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
diff --git a/dev/TODO b/dev/TODO
index 563d0d1a1..1c9d706cd 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -1,8 +1,4 @@
 
- o Discharge
-     - conserver les constantes dans leur section de définition
-       et redéfinir des constantes déchargées à la sortie
-
  o Lib
      - écrire une fonction d'export qui supprimme les FrozenState,
        vérifie qu'il n'y a pas de section ouverte, et présente les
@@ -24,10 +20,7 @@
      - un cache pour type_of_const, type_of_inductive, type_of_constructor,
        lookup_mind_specif
 
- o Lexer
-     à compléter
-
  o Toplevel
-     - parsing de la ligne de commande : utiliser Arg ?
+     - parsing de la ligne de commande : utiliser Arg ???
 
 
diff --git a/library/lib.ml b/library/lib.ml
index f7f6f1a51..f79c22c58 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -163,17 +163,19 @@ let reset_to sp =
   let (_,_,before) = split_lib sp in
   lib_stk := before;
   recalc_path_prefix ();
-  let (spf,frozen) = match find_entry_p is_frozen_state with
-    | (sp, FrozenState f) -> sp,f
+  let spf = match find_entry_p is_frozen_state with
+    | (sp, FrozenState f) -> unfreeze_summaries f; sp
     | _ -> assert false
   in
-  unfreeze_summaries frozen;
   let (after,_,_) = split_lib spf in
   recache_context (List.rev after)
 
 let reset_name id =
-  let (sp,_) = find_entry_p (fun (sp,_) -> id = basename sp) in
-  reset_to sp
+  try
+    let (sp,_) = find_entry_p (fun (sp,_) -> id = basename sp) in
+    reset_to sp
+  with Not_found ->
+    error (string_of_id id ^ ": no such entry")
 
 let is_section_p sp = list_prefix_of (wd_of_sp sp) !path_prefix
 
@@ -193,4 +195,24 @@ let init () =
   path_prefix := [];
   init_summaries()
 
+(* Initial state. *)
+
+let initial_state = ref (None : section_path option)
+
+let declare_initial_state () = 
+  let sp = add_anonymous_entry (FrozenState (freeze_summaries())) in
+  initial_state := Some sp
+
+let reset_initial () =
+  match !initial_state with
+    | None -> init ()
+    | Some sp -> 
+  	begin match split_lib sp with
+	  | (_,(_,FrozenState fs as hd),before) ->
+	      lib_stk := hd::before;
+	      recalc_path_prefix ();
+	      unfreeze_summaries fs
+	  | _ -> assert false
+	end
+
 
diff --git a/library/lib.mli b/library/lib.mli
index 7261ba7e6..2fe172f9f 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -57,3 +57,6 @@ val freeze : unit -> frozen
 val unfreeze : frozen -> unit
 
 val init : unit -> unit
+
+val declare_initial_state : unit -> unit
+val reset_initial : unit -> unit
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e2f5ce94b..6ff3deb70 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -236,12 +236,8 @@ and save_state = abort_refine States.raw_save_state
 and restore_state = abort_refine States.raw_restore_state
 and restore_last_saved_state = abort_refine States.raw_restore_last_saved_state
 ***)
-and reset_all = abort_refine Lib.init
+and reset_initial = abort_refine Lib.reset_initial
 
-(***TODO
-let reset_prelude () = restore_state "Prelude"
-and reset_initial () = restore_state "Initial"
-***)
    
 (*********************************************************************)
 (*              Modifying the current prooftree                      *)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 9a528f555..ab9dc3e43 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -52,6 +52,7 @@ val proof_term : unit -> constr
 val start_proof : string -> strength -> Coqast.t -> unit
 val start_proof_constr : string -> strength -> constr -> unit
 val reset_name : identifier -> unit
+val reset_initial : unit -> unit
 
 val save_named : bool -> unit
 val save_anonymous : bool -> string -> 'a -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e35e9f6ba..282039d98 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -22,29 +22,33 @@ let remove_top_ml () = Mltop.remove ()
 
 let inputstate = ref "barestate.coq"
 let set_inputstate s = inputstate:= s
-let inputstate () =if !inputstate <> "" then intern_state !inputstate
+let inputstate () =
+  if !inputstate <> "" then begin
+    intern_state !inputstate;
+    Lib.declare_initial_state()
+  end
 
 let outputstate = ref ""
 let set_outputstate s = outputstate:=s
 let outputstate () = if !outputstate <> "" then extern_state !outputstate
 
-let load_vernacular_list = ref ([]:string list)
+let load_vernacular_list = ref ([] : string list)
 let add_load_vernacular s =
-  load_vernacular_list := (make_suffix s ".v")::(!load_vernacular_list)
+  load_vernacular_list := (make_suffix s ".v") :: !load_vernacular_list
 let load_vernacular () =
   List.iter
     (fun s -> Vernac.load_vernac false s)
     (List.rev !load_vernacular_list)
 
-let load_vernacular_obj = ref ([]:string list)
-let add_vernac_obj s = load_vernacular_obj := s::(!load_vernacular_obj)
+let load_vernacular_obj = ref ([] : string list)
+let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
 let load_vernac_obj () = 
   List.iter
     (fun s -> Library.load_module (Filename.basename s) (Some s))
     (List.rev !load_vernacular_obj)
 
-let require_list = ref ([]:string list)
-let add_require s = require_list := s::(!require_list)
+let require_list = ref ([] : string list)
+let add_require s = require_list := s :: !require_list
 let require () =
   List.iter
     (fun s -> Library.require_module None (Filename.basename s) (Some s) false)
@@ -144,6 +148,7 @@ let start () =
   if not !initialized then begin
     initialized := true;
     Sys.catch_break false;
+    Lib.init();
     try
       parse_args ();
       print_header ();
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e1396fb3a..ce3b0e957 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -234,13 +234,13 @@ let _ =
 
 (* Resetting *)
 
-(***
 let _ =
   add "ResetInitial"
     (function 
        | [] -> (fun () -> reset_initial ())
        | _  -> bad_vernac_args "ResetInitial")
 
+(***
 let _ =
   add "ResetSection"
     (function