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 +++++------ lib/system.mli | 6 +++--- 2 files changed, 8 insertions(+), 9 deletions(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index d1cdd8efc9..139effd9fa 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 a3d66d577a..5797502e9f 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 -- cgit v1.2.3 From 05ab666a1283de5500dbc0520d18bdb05d95f286 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:45:27 +0200 Subject: Make the interface of System.raw_extern_intern much saner. There is no reason (any longer?) to create simultaneous closures for interning and externing files. This patch makes the code more readable by separating both functions and their signatures. --- lib/system.ml | 71 +++++++++++++++++++++++++++------------------------------- lib/system.mli | 10 +++++---- 2 files changed, 39 insertions(+), 42 deletions(-) (limited to 'lib') 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 -- cgit v1.2.3 From 832ef36c5b066f5cb50a85b9a1450eaf7dcb9e44 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 2 Oct 2015 14:41:29 +0200 Subject: emacs output mode: Added tag to debug messages. So that they display in response buffer. --- lib/pp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/pp.ml b/lib/pp.ml index 30bc30a9ad..1711008ead 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -424,7 +424,7 @@ type logger = message_level -> std_ppcmds -> unit let make_body info s = emacs_quote (hov 0 (info ++ spc () ++ s)) -let debugbody strm = hov 0 (str "Debug:" ++ spc () ++ strm) +let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm)) let warnbody strm = make_body (str "Warning:") strm let errorbody strm = make_body (str "Error:") strm let infobody strm = emacs_quote_info strm -- cgit v1.2.3