Merge branch 'v8.5'

6 files changed, 60 insertions, 45 deletions

diff --git a/lib/dyn.ml b/lib/dyn.ml
index a5e8fb9c2b..056b687313 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Pp
 
 (* Dynamics, programmed with DANGER !!! *)
 
@@ -23,7 +24,7 @@ let create (s : string) =
   let () =
     if Int.Map.mem hash !dyntab then
       let old = Int.Map.find hash !dyntab in
-      let msg = Pp.str ("Dynamic tag collision: " ^ s ^ " vs. " ^ old) in
+      let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in
       anomaly ~label:"Dyn.create" msg
   in
   let () = dyntab := Int.Map.add hash s !dyntab in
@@ -31,8 +32,7 @@ let create (s : string) =
   let outfun (nh, rv) =
     if Int.equal hash nh then Obj.magic rv
     else
-      let msg = (Pp.str ("dyn_out: expected " ^ s)) in
-      anomaly msg
+      anomaly (str "dyn_out: expected " ++ str s)
   in
   (infun, outfun)
 
@@ -43,8 +43,7 @@ let has_tag (s, _) tag =
 let tag (s,_) =
   try Int.Map.find s !dyntab
   with Not_found ->
-    let msg = Pp.str ("Unknown dynamic tag " ^ (string_of_int s)) in
-    anomaly msg
+    anomaly (str "Unknown dynamic tag " ++ int s)
 
 let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2
 
diff --git a/lib/errors.ml b/lib/errors.ml
index a4ec357ee4..999d99ee08 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -69,12 +69,12 @@ let rec print_gen bottom stk e =
 let where = function
 | None -> mt ()
 | Some s ->
-  if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
+  if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt ()
 
 let raw_anomaly e = match e with
   | Anomaly (s, pps) -> where s ++ pps ++ str "."
-  | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
-  | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
+  | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "."
+  | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "."
 
 let print_backtrace e = match Backtrace.get_backtrace e with
 | None -> mt ()
@@ -99,6 +99,8 @@ let iprint (e, info) = print ~info e
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+let iprint_no_report (e, info) =
+  print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info
 
 (** Predefined handlers **)
 
diff --git a/lib/errors.mli b/lib/errors.mli
index 03caa6a9f8..5bd5724746 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -80,6 +80,7 @@ val iprint : Exninfo.iexn -> Pp.std_ppcmds
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 val print_no_report : exn -> Pp.std_ppcmds
+val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds
 
 (** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
diff --git a/lib/pp.ml b/lib/pp.ml
index 76046a7f91..30bc30a9ad 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -8,13 +8,9 @@
 
 module Glue : sig
 
-  (* A left associative glue implements efficient glue operator
-     when used as left associative.  If glue is denoted ++ then
+  (** The [Glue] module implements a container data structure with
+      efficient concatenation. *)
 
-        a ++ b ++ c ++ d = ((a ++ b) ++ c) ++ d = [d] @ ([c] @ ([b] @  [a]))
-
-     I.e. if the short list is the second argument
-  *)
   type 'a t
 
   val atom : 'a -> 'a t
@@ -22,19 +18,28 @@ module Glue : sig
   val empty : 'a t
   val is_empty : 'a t -> bool
   val iter : ('a -> unit) -> 'a t -> unit
-  val map : ('a -> 'b) -> 'a t -> 'b t
 
 end = struct
 
-  type 'a t = 'a list
+  type 'a t = GEmpty | GLeaf of 'a | GNode of 'a t * 'a t
+
+  let atom x = GLeaf x
+
+  let glue x y =
+    match x, y with
+    | GEmpty, _ -> y
+    | _, GEmpty -> x
+    | _, _ -> GNode (x,y)
+
+  let empty = GEmpty
 
-  let atom x = [x]
-  let glue x y = y @ x
-  let empty = []
-  let is_empty x = x = []
+  let is_empty x = x = GEmpty
+
+  let rec iter f = function
+    | GEmpty -> ()
+    | GLeaf x -> f x
+    | GNode (x,y) -> iter f x; iter f y
 
-  let iter f g = List.iter f (List.rev g)
-  let map = List.map
 end
 
 module Tag :
@@ -145,21 +150,6 @@ let app = Glue.glue
 
 let is_empty g = Glue.is_empty g
 
-let rewrite f p =
-  let strtoken = function
-    | Str_len (s, n) ->
-      let s' = f s in
-      Str_len (s', String.length s')
-    | Str_def s ->
-      Str_def (f s)
-  in
-  let rec ppcmd_token = function
-    | Ppcmd_print x -> Ppcmd_print (strtoken x)
-    | Ppcmd_box (bt, g) -> Ppcmd_box (bt, Glue.map ppcmd_token g)
-    | p -> p
-  in
-  Glue.map ppcmd_token p
-
 (* Compute length of an UTF-8 encoded string
    Rem 1 : utf8_length <= String.length (equal if pure ascii)
    Rem 2 : if used for an iso8859_1 encoded string, the result is
@@ -259,7 +249,7 @@ let escape_string s =
     else escape_at s (i-1) in
   escape_at s (String.length s - 1)
 
-let qstring s = str ("\""^escape_string s^"\"")
+let qstring s = str "\"" ++ str (escape_string s) ++ str "\""
 let qs = qstring
 let quote s = h 0 (str "\"" ++ s ++ str "\"")
 
@@ -458,6 +448,27 @@ let logger = ref std_logger
 let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger
 let make_pp_nonemacs() = print_emacs:=false; logger := std_logger
 
+let ft_logger old_logger ft ~id level mesg = match level with
+  | Debug _ -> msgnl_with ft (debugbody mesg)
+  | Info -> msgnl_with ft (infobody mesg)
+  | Notice -> msgnl_with ft mesg
+  | Warning -> old_logger ~id:id level mesg
+  | Error -> old_logger ~id:id level mesg
+
+let with_output_to_file fname func input =
+  let old_logger = !logger in
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
+  try
+    let output = func input in
+    logger := old_logger;
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    logger := old_logger;
+    close_out channel;
+    Exninfo.iraise reraise
 
 let feedback_id = ref (Feedback.Edit 0)
 let feedback_route = ref Feedback.default_route
diff --git a/lib/pp.mli b/lib/pp.mli
index 5dd2686d14..3b1123a9dc 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -12,6 +12,8 @@
 val make_pp_emacs:unit -> unit
 val make_pp_nonemacs:unit -> unit
 
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
 (** Pretty-printers. *)
 
 type std_ppcmds
@@ -46,9 +48,6 @@ val eval_ppcmds : std_ppcmds -> std_ppcmds
 val is_empty : std_ppcmds -> bool
 (** Test emptyness. *)
 
-val rewrite : (string -> string) -> std_ppcmds -> std_ppcmds
-(** [rewrite f pps] applies [f] to all strings that appear in [pps]. *)
-
 (** {6 Derived commands} *)
 
 val spc : unit -> std_ppcmds
diff --git a/lib/system.ml b/lib/system.ml
index 70f5904629..e4a60eccb7 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -159,7 +159,8 @@ let is_in_system_path filename =
 
 let open_trapping_failure name =
   try open_out_bin name
-  with e when Errors.noncritical e -> error ("Can't open " ^ name)
+  with e when Errors.noncritical e ->
+    errorlabstrm "System.open" (str "Can't open " ++ str name)
 
 let try_remove filename =
   try Sys.remove filename
@@ -167,7 +168,8 @@ let try_remove filename =
     msg_warning
       (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
-let error_corrupted file s = error (file ^": " ^ s ^ ". Try to rebuild it.")
+let error_corrupted file s =
+  errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
 
 let input_binary_int f ch =
   try input_binary_int ch
@@ -242,7 +244,8 @@ let extern_intern ?(warn=true) magic =
 	let reraise = Errors.push reraise in
         let () = try_remove filename in
         iraise reraise
-    with Sys_error s -> error ("System error: " ^ s)
+    with Sys_error s ->
+      errorlabstrm "System.extern_state" (str "System error: " ++ str s)
   and intern_state paths name =
     try
       let _,filename = find_file_in_path ~warn paths name in
@@ -251,7 +254,7 @@ let extern_intern ?(warn=true) magic =
       close_in channel;
       v
     with Sys_error s ->
-      error("System error: " ^ s)
+      errorlabstrm "System.intern_state" (str "System error: " ++ str s)
   in
   (extern_state,intern_state)