Merge branch 'v8.5'

3 files changed, 41 insertions, 45 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 01df2510cf..51bd70a499 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
diff --git a/lib/system.ml b/lib/system.ml
index e4a60eccb7..7a62d5603e 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -215,48 +215,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;
-    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)
+let raw_extern_state magic filename =
+  let channel = open_trapping_failure filename in
+  output_binary_int channel magic;
+  channel
 
-let extern_intern ?(warn=true) magic =
-  let (raw_extern,raw_intern) = raw_extern_intern magic in
-  let extern_state name val_0 =
-    try
-      let (filename,channel) = raw_extern name 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 paths name =
+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
+  with
+  | End_of_file -> error_corrupted filename "premature end of file"
+  | Failure s | Sys_error s -> error_corrupted filename s
+
+let extern_state magic filename val_0 =
+  try
+    let channel = raw_extern_state magic filename in
     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;
-      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 6ed4503266..2e773fe96f 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -66,11 +66,13 @@ val find_file_in_path :
 
 exception Bad_magic_number of string
 
-val raw_extern_intern : int ->
-  (string -> string * out_channel) * (string -> in_channel)
+val raw_extern_state : int -> string -> out_channel
 
-val extern_intern : ?warn:bool -> int ->
-  (string -> 'a -> unit) * (CUnix.load_path -> 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