diff options
| -rw-r--r-- | lib/system.ml | 11 | ||||
| -rw-r--r-- | lib/system.mli | 6 | ||||
| -rw-r--r-- | library/library.ml | 6 | ||||
| -rw-r--r-- | library/states.ml | 6 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 10 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
6 files changed, 23 insertions, 18 deletions
diff --git a/lib/system.ml b/lib/system.ml index d1cdd8efc..139effd9f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -178,7 +178,7 @@ let raw_extern_intern magic = let extern_state filename = let channel = open_trapping_failure filename in output_binary_int channel magic; - filename, channel + channel and intern_state filename = try let channel = open_in_bin filename in @@ -191,11 +191,11 @@ let raw_extern_intern magic = in (extern_state,intern_state) -let extern_intern ?(warn=true) magic = +let extern_intern magic = let (raw_extern,raw_intern) = raw_extern_intern magic in - let extern_state name val_0 = + let extern_state filename val_0 = try - let (filename,channel) = raw_extern name in + let channel = raw_extern filename in try marshal_out channel val_0; close_out channel @@ -205,9 +205,8 @@ let extern_intern ?(warn=true) magic = iraise reraise with Sys_error s -> errorlabstrm "System.extern_state" (str "System error: " ++ str s) - and intern_state paths name = + and intern_state filename = try - let _,filename = find_file_in_path ~warn paths name in let channel = raw_intern filename in let v = marshal_in filename channel in close_in channel; diff --git a/lib/system.mli b/lib/system.mli index a3d66d577..5797502e9 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -37,10 +37,10 @@ val find_file_in_path : exception Bad_magic_number of string val raw_extern_intern : int -> - (string -> string * out_channel) * (string -> in_channel) + (string -> out_channel) * (string -> in_channel) -val extern_intern : ?warn:bool -> int -> - (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a) +val extern_intern : int -> + (string -> 'a -> unit) * (string -> 'a) val with_magic_number_check : ('a -> 'b) -> 'a -> 'b diff --git a/library/library.ml b/library/library.ml index f5c7f6335..0fb938e9b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -742,7 +742,8 @@ let save_library_to ?todo dir f otab = if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then error_recursively_dependent_library dir; (* Open the vo file and write the magic number *) - let (f',ch) = raw_extern_library f in + let f' = f in + let ch = raw_extern_library f' in try (* Writing vo payload *) System.marshal_out_segment f' ch (sd : seg_sum); @@ -765,7 +766,8 @@ let save_library_to ?todo dir f otab = iraise reraise let save_library_raw f sum lib univs proofs = - let (f',ch) = raw_extern_library (f^"o") in + let f' = f^".o" in + let ch = raw_extern_library f' in System.marshal_out_segment f' ch (sum : seg_sum); System.marshal_out_segment f' ch (lib : seg_lib); System.marshal_out_segment f' ch (Some univs : seg_univ option); diff --git a/library/states.ml b/library/states.ml index 96a487b16..4e55f0cdc 100644 --- a/library/states.ml +++ b/library/states.ml @@ -22,16 +22,12 @@ let unfreeze (fl,fs) = Summary.unfreeze_summaries fs let (extern_state,intern_state) = - let ensure_suffix f = CUnix.make_suffix f ".coq" in let (raw_extern, raw_intern) = extern_intern Coq_config.state_magic_number in (fun s -> - let s = ensure_suffix s in raw_extern s (freeze ~marshallable:`Yes)), (fun s -> - let s = ensure_suffix s in - let paths = Loadpath.get_paths () in - unfreeze (with_magic_number_check (raw_intern paths) s); + unfreeze (with_magic_number_check raw_intern s); Library.overwrite_library_filenames s) (* Rollback. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4031a161b..7562c29f7 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -144,13 +144,19 @@ let inputstate = ref "" let set_inputstate s = let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in inputstate:=s -let inputstate () = if not (String.is_empty !inputstate) then intern_state !inputstate +let inputstate () = + if not (String.is_empty !inputstate) then + let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in + intern_state fname let outputstate = ref "" let set_outputstate s = let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in outputstate:=s -let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate +let outputstate () = + if not (String.is_empty !outputstate) then + let fname = CUnix.make_suffix !outputstate ".coq" in + extern_state fname let set_include d p implicit = let p = dirpath_of_string p in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index ec81a3f1a..8ae6ac2bc 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -929,10 +929,12 @@ let vernac_chdir = function let vernac_write_state file = Pfedit.delete_all_proofs (); + let file = CUnix.make_suffix file ".coq" in States.extern_state file let vernac_restore_state file = Pfedit.delete_all_proofs (); + let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in States.intern_state file (************) |