diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 71 | ||||
| -rw-r--r-- | lib/system.mli | 10 |
2 files changed, 39 insertions, 42 deletions
diff --git a/lib/system.ml b/lib/system.ml index 139effd9fa..ddc56956c5 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -174,47 +174,42 @@ let skip_in_segment f ch = exception Bad_magic_number of string -let raw_extern_intern magic = - let extern_state filename = - let channel = open_trapping_failure filename in - output_binary_int channel magic; +let raw_extern_state magic filename = + let channel = open_trapping_failure filename in + output_binary_int channel magic; + channel + +let raw_intern_state magic filename = + try + let channel = open_in_bin filename in + if not (Int.equal (input_binary_int filename channel) magic) then + raise (Bad_magic_number filename); channel - and intern_state filename = - try - let channel = open_in_bin filename in - if not (Int.equal (input_binary_int filename channel) magic) then - raise (Bad_magic_number filename); - channel - with - | End_of_file -> error_corrupted filename "premature end of file" - | Failure s | Sys_error s -> error_corrupted filename s - in - (extern_state,intern_state) + with + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s | Sys_error s -> error_corrupted filename s -let extern_intern magic = - let (raw_extern,raw_intern) = raw_extern_intern magic in - let extern_state filename val_0 = - try - let channel = raw_extern filename in - try - marshal_out channel val_0; - close_out channel - with reraise -> - let reraise = Errors.push reraise in - let () = try_remove filename in - iraise reraise - with Sys_error s -> - errorlabstrm "System.extern_state" (str "System error: " ++ str s) - and intern_state filename = +let extern_state magic filename val_0 = + try + let channel = raw_extern_state magic filename in try - let channel = raw_intern filename in - let v = marshal_in filename channel in - close_in channel; - v - with Sys_error s -> - errorlabstrm "System.intern_state" (str "System error: " ++ str s) - in - (extern_state,intern_state) + marshal_out channel val_0; + close_out channel + with reraise -> + let reraise = Errors.push reraise in + let () = try_remove filename in + iraise reraise + with Sys_error s -> + errorlabstrm "System.extern_state" (str "System error: " ++ str s) + +let intern_state magic filename = + try + let channel = raw_intern_state magic filename in + let v = marshal_in filename channel in + close_in channel; + v + with Sys_error s -> + errorlabstrm "System.intern_state" (str "System error: " ++ str s) let with_magic_number_check f a = try f a diff --git a/lib/system.mli b/lib/system.mli index 5797502e9f..247d528b97 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -36,11 +36,13 @@ val find_file_in_path : exception Bad_magic_number of string -val raw_extern_intern : int -> - (string -> out_channel) * (string -> in_channel) +val raw_extern_state : int -> string -> out_channel -val extern_intern : int -> - (string -> 'a -> unit) * (string -> 'a) +val raw_intern_state : int -> string -> in_channel + +val extern_state : int -> string -> 'a -> unit + +val intern_state : int -> string -> 'a val with_magic_number_check : ('a -> 'b) -> 'a -> 'b |