From 82a618e8a4945752698a7900c8af7a51091f7b1b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:05:45 +0200 Subject: Prevent States.intern_state and System.extern_intern from looking up files in the loadpath. This patch causes a bit of code duplication (because of the .coq suffix added to state files) but it makes it clear which part of the code is looking up files in the loadpath and for what purpose. Also it makes the interface of System.extern_intern and System.raw_extern_intern much saner. --- lib/system.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'lib/system.ml') 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; -- cgit v1.2.3