Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

19 files changed, 267 insertions, 177 deletions

diff --git a/lib/cArray.ml b/lib/cArray.ml
index 16034543..bb1e3354 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -13,6 +13,7 @@ sig
   include S
   val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
   val is_empty : 'a array -> bool
   val exists : ('a -> bool) -> 'a array -> bool
   val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
@@ -85,19 +86,22 @@ let compare cmp v1 v2 =
       in
       loop (len - 1)
 
+let equal_norefl cmp t1 t2 =
+  let len = Array.length t1 in
+  if not (Int.equal len (Array.length t2)) then false
+  else
+    let rec aux i =
+      if i < 0 then true
+      else
+        let x = uget t1 i in
+        let y = uget t2 i in
+        cmp x y && aux (pred i)
+    in
+    aux (len - 1)
+
 let equal cmp t1 t2 =
-  if t1 == t2 then true else
-    let len = Array.length t1 in
-    if not (Int.equal len (Array.length t2)) then false
-    else
-      let rec aux i =
-        if i < 0 then true
-        else
-          let x = uget t1 i in
-          let y = uget t2 i in
-          cmp x y && aux (pred i)
-      in
-      aux (len - 1)
+  if t1 == t2 then true else equal_norefl cmp t1 t2
+    
 
 let is_empty array = Int.equal (Array.length array) 0
 
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 39c35e2d..7e5c93b5 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -17,6 +17,11 @@ sig
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
   (** Lift equality to array type. *)
 
+  val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  (** Like {!equal} but does not assume that equality is reflexive: no
+      optimisation is performed if both arrays are physically the
+      same. *)
+
   val is_empty : 'a array -> bool
   (** True whenever the array is empty. *)
 
diff --git a/lib/cString.ml b/lib/cString.ml
index 250b7cee..e9006860 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -135,7 +135,14 @@ let plural n s = if n<>1 then s^"s" else s
 let conjugate_verb_to_be n = if n<>1 then "are" else "is"
 
 let ordinal n =
-  let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+  let s =
+    if (n / 10) mod 10 = 1 then "th"
+    else match n mod 10 with
+    | 1 -> "st"
+    | 2 -> "nd"
+    | 3 -> "rd"
+    | _ -> "th"
+  in
   string_of_int n ^ s
 
 (* string parsing *)
diff --git a/lib/cThread.ml b/lib/cThread.ml
index 55bb6fd6..2d1f10bf 100644
--- a/lib/cThread.ml
+++ b/lib/cThread.ml
@@ -22,7 +22,7 @@ let thread_friendly_read_fd fd s ~off ~len =
   let rec loop () =
     try Unix.read fd s off len
     with Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN|Unix.EINTR),_,_) ->
-      while not (safe_wait_timed_read fd 1.0) do Thread.yield () done;
+      while not (safe_wait_timed_read fd 0.05) do Thread.yield () done;
       loop ()
   in 
     loop ()
@@ -43,6 +43,18 @@ let really_read_fd fd s off len =
     i := !i + r
   done
 
+let really_read_fd_2_oc fd oc len =
+  let i = ref 0 in
+  let size = 4096 in
+  let s = String.create size in
+  while !i < len do
+    let len = len - !i in
+    let r = thread_friendly_read_fd fd s ~off:0 ~len:(min len size) in
+    if r = 0 then raise End_of_file;
+    i := !i + r;
+    output oc s 0 r;
+  done
+
 let thread_friendly_really_read ic s ~off ~len =
   try
     let fd = Unix.descr_of_in_channel ic in
@@ -68,9 +80,26 @@ let thread_friendly_input_value ic =
     let header = String.create Marshal.header_size in
     really_read_fd fd header 0 Marshal.header_size;
     let body_size = Marshal.data_size header 0 in
-    let msg = String.create (body_size + Marshal.header_size) in
-    String.blit header 0 msg 0 Marshal.header_size;
-    really_read_fd fd msg Marshal.header_size body_size;
-    Marshal.from_string msg 0
-  with Unix.Unix_error _ -> raise End_of_file
+    let desired_size = body_size + Marshal.header_size in
+    if desired_size <= Sys.max_string_length then begin
+      let msg = String.create desired_size in
+      String.blit header 0 msg 0 Marshal.header_size;
+      really_read_fd fd msg Marshal.header_size body_size;
+      Marshal.from_string msg 0
+    end else begin
+      (* Workaround for 32 bit systems and data > 16M *)
+      let name, oc =
+        Filename.open_temp_file ~mode:[Open_binary] "coq" "marshal" in
+      try
+        output oc header 0 Marshal.header_size;
+        really_read_fd_2_oc fd oc body_size;
+        close_out oc;
+        let ic = open_in_bin name in
+        let data = Marshal.from_channel ic in
+        close_in ic;
+        Sys.remove name;
+        data
+      with e -> Sys.remove name; raise e
+    end
+  with Unix.Unix_error _ | Sys_error _ -> raise End_of_file
 
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 63def9a1..a5e8fb9c 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -47,3 +47,5 @@ let tag (s,_) =
     anomaly msg
 
 let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2
+
+let dump () = Int.Map.bindings !dyntab
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 4a713472..cac912ac 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -14,3 +14,4 @@ val create : string -> ('a -> t) * (t -> 'a)
 val tag : t -> string
 val has_tag : t -> string -> bool
 val pointer_equal : t -> t -> bool
+val dump : unit -> (int * string) list
diff --git a/lib/errors.ml b/lib/errors.ml
index ab331d6a..a4ec357e 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -108,7 +108,7 @@ let _ = register_handler begin function
   | _ -> raise Unhandled
 end
 
-(** Critical exceptions shouldn't be catched and ignored by mistake
+(** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
     only at the very end of interp, to be displayed to the user. *)
 
diff --git a/lib/errors.mli b/lib/errors.mli
index e4096a7e..03caa6a9 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -81,7 +81,7 @@ val iprint : Exninfo.iexn -> Pp.std_ppcmds
     isn't printed (used in Ltac debugging). *)
 val print_no_report : exn -> Pp.std_ppcmds
 
-(** Critical exceptions shouldn't be catched and ignored by mistake
+(** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
     only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user.
     Typical example: [Sys.Break], [Assert_failure], [Anomaly] ...
diff --git a/lib/future.ml b/lib/future.ml
index 2f1ce5e4..02d3702d 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -11,19 +11,21 @@ let freeze = ref (fun () -> assert false : unit -> Dyn.t)
 let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
 let set_freeze f g = freeze := f; unfreeze := g
 
-exception NotReady
-exception NotHere
+exception NotReady of string
+exception NotHere of string
 let _ = Errors.register_handler (function
-  | NotReady ->
-      Pp.strbrk("The value you are asking for is not ready yet. " ^
+  | NotReady name ->
+      Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
                 "Please wait or pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
-                "asynchronous script processing.")
-  | NotHere ->
-      Pp.strbrk("The value you are asking for is not available "^
+                "asynchronous script processing and don't pass \"-quick\" to "^
+                "coqc.")
+  | NotHere name ->
+      Pp.strbrk("The value you are asking for ("^name^") is not available "^
                 "in this process. If you really need this, pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
-                "asynchronous script processing.")
+                "asynchronous script processing and don't pass \"-quick\" to "^
+                "coqc.")
   | _ -> raise Errors.Unhandled)
 
 type fix_exn = Exninfo.iexn -> Exninfo.iexn
@@ -54,67 +56,69 @@ and 'a comp =
   | Exn of Exninfo.iexn  (* Invariant: this exception is always "fixed" as in fix_exn *)
 
 and 'a comput =
-  | Ongoing of (UUID.t * fix_exn * 'a comp ref) Ephemeron.key
+  | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) Ephemeron.key
   | Finished of 'a
 
 and 'a computation = 'a comput ref
 
-let create ?(uuid=UUID.fresh ()) f x =
-  ref (Ongoing (Ephemeron.create (uuid, f, Pervasives.ref x)))
+let unnamed = "unnamed"
+
+let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x =
+  ref (Ongoing (name, Ephemeron.create (uuid, f, Pervasives.ref x)))
 let get x =
   match !x with
-  | Finished v -> UUID.invalid, id, ref (Val (v,None))
-  | Ongoing x ->
-      try Ephemeron.get x
+  | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None))
+  | Ongoing (name, x) ->
+      try let uuid, fix, c = Ephemeron.get x in name, uuid, fix, c
       with Ephemeron.InvalidKey ->
-        UUID.invalid, id, ref (Exn (NotHere, Exninfo.null))
+        name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null))
 
 type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn  ]
 
-let is_over kx = let _, _, x = get kx in match !x with
+let is_over kx = let _, _, _, x = get kx in match !x with
   | Val _ | Exn _ -> true
   | Closure _ | Delegated _ -> false
 
-let is_val kx = let _, _, x = get kx in match !x with
+let is_val kx = let _, _, _, x = get kx in match !x with
   | Val _ -> true
   | Exn _ | Closure _ | Delegated _ -> false
 
-let is_exn kx = let _, _, x = get kx in match !x with
+let is_exn kx = let _, _, _, x = get kx in match !x with
   | Exn _ -> true
   | Val _ | Closure _ | Delegated _ -> false
 
-let peek_val kx = let _, _, x = get kx in match !x with
+let peek_val kx = let _, _, _, x = get kx in match !x with
   | Val (v, _) -> Some v
   | Exn _ | Closure _ | Delegated _ -> None
 
-let uuid kx = let id, _, _ = get kx in id
+let uuid kx = let _, id, _, _ = get kx in id
 
 let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None))
 let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
 
-let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn
+let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
 
-let create_delegate ?(blocking=true) fix_exn =
+let create_delegate ?(blocking=true) ~name fix_exn =
   let assignement signal ck = fun v ->
-    let _, fix_exn, c = get ck in
+    let _, _, fix_exn, c = get ck in
     assert (match !c with Delegated _ -> true | _ -> false);
     begin match v with
     | `Val v -> c := Val (v, None)
     | `Exn e -> c := Exn (fix_exn e)
-    | `Comp f -> let _, _, comp = get f in c := !comp end;
+    | `Comp f -> let _, _, _, comp = get f in c := !comp end;
     signal () in
   let wait, signal =
-    if not blocking then (fun () -> raise NotReady), ignore else
+    if not blocking then (fun () -> raise (NotReady name)), ignore else
     let lock = Mutex.create () in
     let cond = Condition.create () in
     (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock),
     (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in
-  let ck = create fix_exn (Delegated wait) in
+  let ck = create ~name fix_exn (Delegated wait) in
   ck, assignement signal ck
 
 (* TODO: get rid of try/catch to be stackless *)
 let rec compute ~pure ck : 'a value =
-  let _, fix_exn, c = get ck in
+  let _, _, fix_exn, c = get ck in
   match !c with
   | Val (x, _) -> `Val x
   | Exn (e, info) -> `Exn (e, info)
@@ -128,7 +132,7 @@ let rec compute ~pure ck : 'a value =
         let e = Errors.push e in
         let e = fix_exn e in
         match e with
-        | (NotReady, _) -> `Exn e
+        | (NotReady _, _) -> `Exn e
         | _ -> c := Exn e; `Exn e
 
 let force ~pure x = match compute ~pure x with
@@ -136,8 +140,8 @@ let force ~pure x = match compute ~pure x with
   | `Exn e -> Exninfo.iraise e
 
 let chain ~pure ck f =
-  let uuid, fix_exn, c = get ck in
-  create ~uuid fix_exn (match !c with
+  let name, uuid, fix_exn, c = get ck in
+  create ~uuid ~name fix_exn (match !c with
   | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck))
   | Exn _ as x -> x
   | Val (v, None) when pure -> Closure (fun () -> f v)
@@ -156,7 +160,7 @@ let chain ~pure ck f =
 let create fix_exn f = create fix_exn (Closure f)
 
 let replace kx y =
-  let _, _, x = get kx in
+  let _, _, _, x = get kx in
   match !x with
   | Exn _ -> x := Closure (fun () -> force ~pure:false y)
   | _ -> Errors.anomaly
@@ -207,10 +211,10 @@ let map2 ?greedy f x l =
 
 let print f kx =
   let open Pp in
-  let (uid, _, x) = get kx in
+  let name, uid, _, x = get kx in
   let uid =
-    if UUID.equal uid UUID.invalid then str "[#]"
-    else str "[" ++ int uid ++ str "]"
+    if UUID.equal uid UUID.invalid then str "[#:" ++ str name ++ str "]"
+    else str "[" ++ int uid ++ str":" ++ str name ++ str "]"
   in
   match !x with
   | Delegated _ -> str "Delegated" ++ uid
diff --git a/lib/future.mli b/lib/future.mli
index 8a4fa0bd..324d5f7d 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -63,7 +63,7 @@ end
 module UUIDMap : Map.S with type key = UUID.t
 module UUIDSet : Set.S with type elt = UUID.t
 
-exception NotReady
+exception NotReady of string
 
 type 'a computation
 type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ]
@@ -100,7 +100,8 @@ val fix_exn_of : 'a computation -> fix_exn
    delage assigns it. *)
 type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 val create_delegate :
-  ?blocking:bool -> fix_exn -> 'a computation * ('a assignement -> unit)
+  ?blocking:bool -> name:string ->
+  fix_exn -> 'a computation * ('a assignement -> unit)
 
 (* Given a computation that is_exn, replace it by another one *)
 val replace : 'a computation -> 'a computation -> unit
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 752e2634..46ba0b62 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -43,6 +43,7 @@ module type S =
     type table
     val generate : u -> table
     val hcons : table -> t -> t
+    val stats : table -> Hashset.statistics
   end
 
 module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
@@ -67,6 +68,8 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
       let y = X.hashcons u x in
       Htbl.repr (X.hash y) y tab
 
+    let stats (tab, _) = Htbl.stats tab
+
   end
 
 (* A few usefull wrappers:
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 60a9ee01..8d0adc3f 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -56,6 +56,8 @@ module type S =
     (** This create a hashtable of the hashconsed objects. *)
     val hcons : table -> t -> t
     (** Perform the hashconsing of the given object within the table. *)
+    val stats : table -> Hashset.statistics
+    (** Recover statistics of the hashconsing table. *)
   end
 
 module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u)
diff --git a/lib/hashset.ml b/lib/hashset.ml
index 6bec81c7..1ca6cc64 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -19,12 +19,20 @@ module type EqType = sig
   val equal : t -> t -> bool
 end
 
+type statistics = {
+  num_bindings: int;
+  num_buckets: int;
+  max_bucket_length: int;
+  bucket_histogram: int array
+}
+
 module type S = sig
   type elt
   type t
   val create : int -> t
   val clear : t -> unit
   val repr : int -> elt -> t -> elt
+  val stats : t -> statistics
 end
 
 module Make (E : EqType) =
@@ -185,6 +193,24 @@ module Make (E : EqType) =
     let ifnotfound index = add_aux t Weak.set (Some d) h index; d in
     find_or h t d ifnotfound
 
+  let stats t =
+    let fold accu bucket = max (count_bucket 0 bucket 0) accu in
+    let max_length = Array.fold_left fold 0 t.table in
+    let histogram = Array.make (max_length + 1) 0 in
+    let iter bucket =
+      let len = count_bucket 0 bucket 0 in
+      histogram.(len) <- succ histogram.(len)
+    in
+    let () = Array.iter iter t.table in
+    let fold (num, len, i) k = (num + k * i, len + k, succ i) in
+    let (num, len, _) = Array.fold_left fold (0, 0, 0) histogram in
+    {
+      num_bindings = num;
+      num_buckets = len;
+      max_bucket_length = Array.length histogram;
+      bucket_histogram = histogram;
+    }
+
 end
 
 module Combine = struct
diff --git a/lib/hashset.mli b/lib/hashset.mli
index 537f3418..a455eec6 100644
--- a/lib/hashset.mli
+++ b/lib/hashset.mli
@@ -19,6 +19,13 @@ module type EqType = sig
   val equal : t -> t -> bool
 end
 
+type statistics = {
+  num_bindings: int;
+  num_buckets: int;
+  max_bucket_length: int;
+  bucket_histogram: int array
+}
+
 module type S = sig
   type elt
   (** Type of hashsets elements. *)
@@ -34,6 +41,8 @@ module type S = sig
       specific representation that is stored in [set]. Otherwise,
       [constr] is stored in [set] and will be used as the canonical
       representation of this value in the future. *)
+  val stats : t -> statistics
+  (** Recover statistics on the table. *)
 end
 
 module Make (E : EqType) : S with type elt = E.t
diff --git a/lib/monad.ml b/lib/monad.ml
index 4a52684d..a1714a41 100644
--- a/lib/monad.ml
+++ b/lib/monad.ml
@@ -111,7 +111,7 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct
       | [a] ->
           M.map (fun a' -> [a']) (f a)
       | a::b::l ->
-          map f l >>= fun l' ->
+          map_right f l >>= fun l' ->
           f b >>= fun b' ->
           M.map (fun a' -> a'::b'::l') (f a)
 
diff --git a/lib/pp.ml b/lib/pp.ml
index 234d2344..76046a7f 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -387,8 +387,6 @@ let pp_with ?pp_tag ft strm =
 let ppnl_with ft strm =
   pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ())))
 
-let pp_flush_with ft = Format.pp_print_flush ft
-
 (* pretty printing functions WITH FLUSH *)
 let msg_with ft strm =
   pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush))
@@ -519,8 +517,17 @@ let pr_arg pr x = spc () ++ pr x
 let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
 let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
 
+(** TODO: merge with CString.ordinal *)
 let pr_nth n =
-  int n ++ str (match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th")
+  let s =
+    if (n / 10) mod 10 = 1 then "th"
+    else match n mod 10 with
+    | 1 -> "st"
+    | 2 -> "nd"
+    | 3 -> "rd"
+    | _ -> "th"
+  in
+  int n ++ str s
 
 (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
 
diff --git a/lib/richpp.ml b/lib/richpp.ml
index 745b7d2a..c4a9c39d 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Xml_datatype
 
 type 'annotation located = {
@@ -14,129 +15,117 @@ type 'annotation located = {
   endpos     : int
 }
 
+type 'a stack =
+| Leaf
+| Node of string * 'a located gxml list * int * 'a stack
+
+type 'a context = {
+  mutable stack : 'a stack;
+  (** Pending opened nodes *)
+  mutable offset : int;
+  (** Quantity of characters printed so far *)
+  mutable annotations : 'a option Int.Map.t;
+  (** Map associating annotations to indexes *)
+  mutable index : int;
+  (** Current index of annotations *)
+}
+
+(** We use Format to introduce tags inside the pretty-printed document.
+    Each inserted tag is a fresh index that we keep in sync with the contents
+    of annotations.
+
+    We build an XML tree on the fly, by plugging ourselves in Format tag
+    marking functions. As those functions are called when actually writing to
+    the device, the resulting tree is correct.
+*)
 let rich_pp annotate ppcmds =
-  (** First, we use Format to introduce tags inside
-      the pretty-printed document.
-
-      Each inserted tag is a fresh index that we keep in sync with the contents
-      of annotations.
-  *)
-  let annotations = ref [] in
-  let index = ref (-1) in
+
+  let context = {
+    stack = Leaf;
+    offset = 0;
+    annotations = Int.Map.empty;
+    index = (-1);
+  } in
+
   let pp_tag obj =
-    let () = incr index in
-    let () = annotations := obj :: !annotations in
-    string_of_int !index
+    let index = context.index + 1 in
+    let () = context.index <- index in
+    let obj = annotate obj in
+    let () = context.annotations <- Int.Map.add index obj context.annotations in
+    string_of_int index
+  in
+
+  let pp_buffer = Buffer.create 13 in
+
+  let push_pcdata () =
+    (** Push the optional PCData on the above node *)
+    let len = Buffer.length pp_buffer in
+    if len = 0 then ()
+    else match context.stack with
+    | Leaf -> assert false
+    | Node (node, child, pos, ctx) ->
+      let data = Buffer.contents pp_buffer in
+      let () = Buffer.clear pp_buffer in
+      let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in
+      context.offset <- context.offset + len
   in
 
-  let tagged_pp = Format.(
-
-    (** Warning: The following instructions are valid only if
-        [str_formatter] is not used for another purpose in
-        Pp.pp_with. *)
-
-    let ft = str_formatter in
-
-    (** We reuse {!Format} standard way of producing tags
-        inside pretty-printing. *)
-    pp_set_tags ft true;
-
-    (** The whole output must be a valid document. To that
-        end, we nest the document inside a tag named <pp>. *)
-    pp_open_tag ft "pp";
-
-    (** XML ignores spaces. The problem is that our pretty-printings
-        are based on spaces to indent. To solve that problem, we
-        systematically output non-breakable spaces, which are properly
-        honored by XML.
-
-        To do so, we reconfigure the [str_formatter] temporarily by
-        hijacking the function that output spaces. *)
-    let out, flush, newline, std_spaces =
-      pp_get_all_formatter_output_functions ft ()
-    in
-    let set = pp_set_all_formatter_output_functions ft ~out ~flush ~newline in
-    set ~spaces:(fun k ->
-      for i = 0 to k - 1 do
-        Buffer.add_string stdbuf "&nbsp;"
-      done
-    );
-
-    (** Some characters must be escaped in XML. This is done by the
-        following rewriting of the strings held by pretty-printing
-        commands. *)
-    Pp.(pp_with ~pp_tag ft (rewrite Xml_printer.pcdata_to_string ppcmds));
-
-    (** Insert </pp>. *)
-    pp_close_tag ft ();
-
-    (** Get the final string. *)
-    let output = flush_str_formatter () in
-
-    (** Finalize by restoring the state of the [str_formatter] and the
-        default behavior of Format. By the way, there may be a bug here:
-        there is no {!Format.pp_get_tags} and therefore if the tags flags
-        was already set to true before executing this piece of code, the
-        state of Format is not restored. *)
-    set ~spaces:std_spaces;
-    pp_set_tags ft false;
-    output
-  )
+  let open_xml_tag tag =
+    let () = push_pcdata () in
+    context.stack <- Node (tag, [], context.offset, context.stack)
   in
-  (** Second, we retrieve the final function that relates
-      each tag to an annotation. *)
-  let objs = CArray.rev_of_list !annotations in
-  let get index = annotate objs.(index) in
-
-  (** Third, we parse the resulting string. It is a valid XML
-      document (in the sense of Xml_parser). As blanks are
-      meaningful we deactivate canonicalization in the XML
-      parser. *)
-  let xml_pp =
-    try
-      Xml_parser.(parse ~do_not_canonicalize:true (make (SString tagged_pp)))
-    with Xml_parser.Error e ->
-      Printf.eprintf
-        "Broken invariant (RichPp): \n\
-         The output semi-structured pretty-printing is ill-formed.\n\
-         Please report.\n\
-         %s"
-        (Xml_parser.error e);
-      exit 1
+
+  let close_xml_tag tag =
+    let () = push_pcdata () in
+    match context.stack with
+    | Leaf -> assert false
+    | Node (node, child, pos, ctx) ->
+      let () = assert (String.equal tag node) in
+      let annotation =
+        try Int.Map.find (int_of_string node) context.annotations
+        with _ -> None
+      in
+      let annotation = {
+        annotation = annotation;
+        startpos = pos;
+        endpos = context.offset;
+      } in
+      let xml = Element (node, annotation, List.rev child) in
+      match ctx with
+      | Leaf ->
+        (** Final node: we keep the result in a dummy context *)
+        context.stack <- Node ("", [xml], 0, Leaf)
+      | Node (node, child, pos, ctx) ->
+        context.stack <- Node (node, xml :: child, pos, ctx)
   in
 
-  (** Fourth, the low-level XML is turned into a high-level
-      semi-structured document that contains a located annotation in
-      every node. During the traversal of the low-level XML document,
-      we build a raw string representation of the pretty-print. *)
-  let rec node buffer = function
-    | Element (index, [], cs) ->
-      let startpos, endpos, cs = children buffer cs in
-      let annotation = try get (int_of_string index) with _ -> None in
-      (Element (index, { annotation; startpos; endpos }, cs), endpos)
+  let open Format in
 
-    | PCData s ->
-      Buffer.add_string buffer s;
-      (PCData s, Buffer.length buffer)
+  let ft = formatter_of_buffer pp_buffer in
 
-    | _ ->
-      assert false (* Because of the form of XML produced by Format. *)
-
-  and children buffer cs =
-    let startpos   = Buffer.length buffer in
-    let cs, endpos =
-      List.fold_left (fun (cs, endpos) c ->
-        let c, endpos = node buffer c in
-        (c :: cs, endpos)
-      ) ([], startpos) cs
-    in
-    (startpos, endpos, List.rev cs)
-  in
-  let pp_buffer = Buffer.create 13 in
-  let xml, _ = node pp_buffer xml_pp in
+  let tag_functions = {
+    mark_open_tag = (fun tag -> let () = open_xml_tag tag in "");
+    mark_close_tag = (fun tag -> let () = close_xml_tag tag in "");
+    print_open_tag = ignore;
+    print_close_tag = ignore;
+  } in
+
+  pp_set_formatter_tag_functions ft tag_functions;
+  pp_set_mark_tags ft true;
+
+  (** The whole output must be a valid document. To that
+      end, we nest the document inside <pp> tags. *)
+  pp_open_tag ft "pp";
+  Pp.(pp_with ~pp_tag ft ppcmds);
+  pp_close_tag ft ();
+
+  (** Get the resulting XML tree. *)
+  let () = pp_print_flush ft () in
+  let () = assert (Buffer.length pp_buffer = 0) in
+  match context.stack with
+  | Node ("", [xml], 0, Leaf) -> xml
+  | _ -> assert false
 
-  (** We return the raw pretty-printing and its annotations tree. *)
-  (Buffer.contents pp_buffer, xml)
 
 let annotations_positions xml =
   let rec node accu = function
diff --git a/lib/richpp.mli b/lib/richpp.mli
index 446ee1a0..bf80c8dc 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -17,13 +17,13 @@ type 'annotation located = {
 }
 
 (** [rich_pp get_annotations ppcmds] returns the interpretation
-    of [ppcmds] as a string as well as a semi-structured document
+    of [ppcmds] as a semi-structured document
     that represents (located) annotations of this string.
     The [get_annotations] function is used to convert tags into the desired
     annotation. If this function returns [None], then no annotation is put. *)
 val rich_pp :
   (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds ->
-  string * 'annotation located Xml_datatype.gxml
+  'annotation located Xml_datatype.gxml
 
 (** [annotations_positions ssdoc] returns a list associating each
     annotations with its position in the string from which [ssdoc] is
diff --git a/lib/terminal.ml b/lib/terminal.ml
index 1e6c2557..0f6b23af 100644
--- a/lib/terminal.ml
+++ b/lib/terminal.ml
@@ -167,7 +167,8 @@ let reset_style = {
   negative = Some false;
 }
 
-let has_style t = Unix.isatty t
+let has_style t =
+  Unix.isatty t && Sys.os_type = "Unix"
 
 let split c s =
   let len = String.length s in