diff options
-rw-r--r-- | .depend | 12 | ||||
-rw-r--r-- | dev/TODO | 9 | ||||
-rw-r--r-- | library/lib.ml | 32 | ||||
-rw-r--r-- | library/lib.mli | 3 | ||||
-rw-r--r-- | proofs/pfedit.ml | 6 | ||||
-rw-r--r-- | proofs/pfedit.mli | 1 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 19 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 2 |
8 files changed, 52 insertions, 32 deletions
@@ -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 \ @@ -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 |