Imported Upstream version 8.5~beta3+dfsg

27 files changed, 476 insertions, 149 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c9018c9e..5dedb0d0 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -42,6 +42,8 @@ module M = Map.Make(String)
 type data = string M.t
 type aux_file = data H.t
 
+let contents x = x
+
 let empty_aux_file = H.empty
 
 let get aux loc key = M.find key (H.find (Loc.unloc loc) aux)
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index e340fc65..b672d3db 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -13,6 +13,10 @@ val get : aux_file -> Loc.t -> string -> string
 val empty_aux_file : aux_file
 val set : aux_file -> Loc.t -> string -> string -> aux_file
 
+module H : Map.S with type key = int * int
+module M : Map.S with type key = string
+val contents : aux_file -> string M.t H.t
+
 val start_aux_file_for : string -> unit
 val stop_aux_file : unit -> unit 
 val recording : unit -> bool
diff --git a/lib/cThread.ml b/lib/cThread.ml
index 2d1f10bf..9cbdf5a9 100644
--- a/lib/cThread.ml
+++ b/lib/cThread.ml
@@ -8,22 +8,12 @@
 
 type thread_ic = in_channel
 
-let prepare_in_channel_for_thread_friendly_io ic =
-  Unix.set_nonblock (Unix.descr_of_in_channel ic); ic
-
-let safe_wait_timed_read fd time =
-  try Thread.wait_timed_read fd time
-  with Unix.Unix_error (Unix.EINTR, _, _) ->
-    (** On Unix, the above function may raise this exception when it is
-        interrupted by a signal. (It uses Unix.select internally.) *)
-    false
+let prepare_in_channel_for_thread_friendly_io ic = ic
 
 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 0.05) do Thread.yield () done;
-      loop ()
+    with Unix.Unix_error(Unix.EINTR,_,_) -> loop ()
   in 
     loop ()
 
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 2da81c95..7ff1d293 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -29,6 +29,7 @@ Util
 Stateid
 Feedback
 Pp
+Ppstyle
 Xml_lexer
 Xml_parser
 Xml_printer
diff --git a/lib/dyn.ml b/lib/dyn.ml
index a5e8fb9c..056b6873 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 a4ec357e..c1d224df 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 **)
 
@@ -118,3 +120,22 @@ let noncritical = function
   | Timeout | Drop | Quit -> false
   | Invalid_argument "equal: functional value" -> false
   | _ -> true
+
+(** Check whether an exception is handled *)
+
+exception Bottom
+
+let handled e =
+  let bottom _ = raise Bottom in
+  try let _ = print_gen bottom !handle_stack e in true
+  with Bottom -> false
+
+(** Prints info which is either an error or
+   an anomaly and then exits with the appropriate
+   error code *)
+
+let fatal_error info anomaly =
+  let msg = info ++ fnl () in
+  pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
+  flush_all ();
+  exit (if anomaly then 129 else 1)
diff --git a/lib/errors.mli b/lib/errors.mli
index 03caa6a9..e5dad93f 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
@@ -87,3 +88,12 @@ val print_no_report : exn -> Pp.std_ppcmds
     Typical example: [Sys.Break], [Assert_failure], [Anomaly] ...
 *)
 val noncritical : exn -> bool
+
+(** Check whether an exception is handled by some toplevel printer. The
+    [Anomaly] exception is never handled. *)
+val handled : exn -> bool
+
+(** Prints info which is either an error or
+   an anomaly and then exits with the appropriate
+   error code *)
+val fatal_error : Pp.std_ppcmds -> bool -> 'a
diff --git a/lib/flags.ml b/lib/flags.ml
index c8e7f7af..ab4ac03f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -48,6 +48,8 @@ let batch_mode = ref false
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 let compilation_mode = ref BuildVo
 
+let test_mode = ref false
+
 type async_proofs = APoff | APonLazy | APon
 let async_proofs_mode = ref APoff
 type cache = Force
@@ -160,7 +162,7 @@ let make_polymorphic_flag b =
 let program_mode = ref false
 let is_program_mode () = !program_mode
 
-let warn = ref true
+let warn = ref false
 let make_warn flag = warn := flag;  ()
 let if_warn f x = if !warn then f x
 
@@ -206,10 +208,14 @@ let inline_level = ref default_inline_level
 let set_inline_level = (:=) inline_level
 let get_inline_level () = !inline_level
 
-(* Disabling native code compilation for conversion and normalization *)
-let no_native_compiler = ref Coq_config.no_native_compiler
+(* Native code compilation for conversion and normalization *)
+let native_compiler = ref false
 
 (* Print the mod uid associated to a vo file by the native compiler *)
 let print_mod_uid = ref false
 
 let tactic_context_compat = ref false
+
+let dump_bytecode = ref false
+let set_dump_bytecode = (:=) dump_bytecode
+let get_dump_bytecode () = !dump_bytecode
diff --git a/lib/flags.mli b/lib/flags.mli
index 756d3b85..8e371365 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -15,6 +15,8 @@ val batch_mode : bool ref
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 val compilation_mode : compilation_mode ref
 
+val test_mode : bool ref
+
 type async_proofs = APoff | APonLazy | APon
 val async_proofs_mode : async_proofs ref
 type cache = Force
@@ -128,12 +130,17 @@ val set_inline_level : int -> unit
 val get_inline_level : unit -> int
 val default_inline_level : int
 
-(* Disabling native code compilation for conversion and normalization *)
-val no_native_compiler : bool ref
+(** Native code compilation for conversion and normalization *)
+val native_compiler : bool ref
 
-(* Print the mod uid associated to a vo file by the native compiler *)
+(** Print the mod uid associated to a vo file by the native compiler *)
 val print_mod_uid : bool ref
 
 val tactic_context_compat : bool ref
 (** Set to [true] to trigger the compatibility bugged context matching (old
     context vs. appcontext) is set. *)
+
+(** Dump the bytecode after compilation (for debugging purposes) *)
+val dump_bytecode : bool ref
+val set_dump_bytecode : bool -> unit
+val get_dump_bytecode : unit -> bool
diff --git a/lib/future.ml b/lib/future.ml
index 02d3702d..78a15826 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -11,21 +11,27 @@ 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 of string
-exception NotHere of string
-let _ = Errors.register_handler (function
-  | NotReady name ->
+let not_ready_msg = ref (fun 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 and don't pass \"-quick\" to "^
-                "coqc.")
-  | NotHere name ->
+                "coqc."))
+let not_here_msg = ref (fun 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 and don't pass \"-quick\" to "^
-                "coqc.")
+                "coqc."))
+
+let customize_not_ready_msg f = not_ready_msg := f
+let customize_not_here_msg f = not_here_msg := f
+
+exception NotReady of string
+exception NotHere of string
+let _ = Errors.register_handler (function
+  | NotReady name -> !not_ready_msg name
+  | NotHere name -> !not_here_msg name
   | _ -> raise Errors.Unhandled)
 
 type fix_exn = Exninfo.iexn -> Exninfo.iexn
diff --git a/lib/future.mli b/lib/future.mli
index 324d5f7d..adc15e49 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -91,13 +91,13 @@ val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
  * When a future enters the environment a corresponding hook is run to perform
  * some work.  If this fails, then its failure has to be annotated with the
  * same state id that corresponds to the future computation end.  I.e. Qed
- * is split into two parts, the lazy one (the future) and the eagher one
+ * is split into two parts, the lazy one (the future) and the eager one
  * (the hook), both performing some computations for the same state id. *)
 val fix_exn_of : 'a computation -> fix_exn
 
 (* Run remotely, returns the function to assign.
    If not blocking (the default) it raises NotReady if forced before the
-   delage assigns it. *)
+   delegate assigns it. *)
 type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 val create_delegate :
   ?blocking:bool -> name:string ->
@@ -161,3 +161,6 @@ val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
    Thy are set for the outermos layer of the system, since they have to
    deal with the whole system state. *)
 val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
+
+val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit
+val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit
diff --git a/lib/pp.ml b/lib/pp.ml
index 76046a7f..4ed4b177 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 "\"")
 
@@ -372,11 +362,11 @@ let emacs_quote_info_start = "<infomsg>"
 let emacs_quote_info_end = "</infomsg>"
 
 let emacs_quote g =
-  if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end
+  if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
   else hov 0 g
 
 let emacs_quote_info g =
-  if !print_emacs then str emacs_quote_info_start++fnl() ++ hov 0 g ++ str emacs_quote_info_end
+  if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
   else hov 0 g
 
 
@@ -434,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
@@ -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 5dd2686d..3b1123a9 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/pp_control.ml b/lib/pp_control.ml
index 0d224c03..969c1550 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -20,7 +20,7 @@ let dflt_gp = {
   margin     = 78;
   max_indent = 50;
   max_depth  = 50;
-  ellipsis   = ".." }
+  ellipsis   = "..." }
 
 (* A deeper pretty-printer to print proof scripts *)
 
@@ -84,5 +84,10 @@ let set_margin v =
   let v = match v with None -> default_margin | Some v -> v in
   Format.pp_set_margin Format.str_formatter v;
   Format.pp_set_margin !std_ft v;
-  Format.pp_set_margin !deep_ft v
-
+  Format.pp_set_margin !deep_ft v;
+  (* Heuristic, based on usage: the column on the right of max_indent
+     column is 20% of width, capped to 30 characters *)
+  let m = max (64 * v / 100) (v-30) in
+  Format.pp_set_max_indent Format.str_formatter m;
+  Format.pp_set_max_indent !std_ft m;
+  Format.pp_set_max_indent !deep_ft m
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
new file mode 100644
index 00000000..fb334c70
--- /dev/null
+++ b/lib/ppstyle.ml
@@ -0,0 +1,149 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+
+type t = string
+(** We use the concatenated string, with dots separating each string. We
+    forbid the use of dots in the strings. *)
+
+let tags : Terminal.style option String.Map.t ref = ref String.Map.empty
+
+let make ?style tag =
+  let check s = if String.contains s '.' then invalid_arg "Ppstyle.make" in
+  let () = List.iter check tag in
+  let name = String.concat "." tag in
+  let () = assert (not (String.Map.mem name !tags)) in
+  let () = tags := String.Map.add name style !tags in
+  name
+
+let repr t = String.split '.' t
+
+let get_style tag =
+  try String.Map.find tag !tags with Not_found -> assert false
+
+let set_style tag st =
+  try tags := String.Map.update tag st !tags with Not_found -> assert false
+
+let clear_styles () =
+  tags := String.Map.map (fun _ -> None) !tags
+
+let dump () = String.Map.bindings !tags
+
+let parse_config s =
+  let styles = Terminal.parse s in
+  let set accu (name, st) =
+    try String.Map.update name (Some st) accu with Not_found -> accu
+  in
+  tags := List.fold_left set !tags styles
+
+let tag = Pp.Tag.create "ppstyle"
+
+(** Default tag is to reset everything *)
+let default = Terminal.({
+  fg_color = Some `DEFAULT;
+  bg_color = Some `DEFAULT;
+  bold = Some false;
+  italic = Some false;
+  underline = Some false;
+  negative = Some false;
+})
+
+let empty = Terminal.make ()
+
+let make_style_stack style_tags =
+  (** Not thread-safe. We should put a lock somewhere if we print from
+      different threads. Do we? *)
+  let style_stack = ref [] in
+  let peek () = match !style_stack with
+  | [] -> default (** Anomalous case, but for robustness *)
+  | st :: _ -> st
+  in
+  let push tag =
+    let style =
+      try
+        begin match String.Map.find tag style_tags with
+        | None -> empty
+        | Some st -> st
+        end
+      with Not_found -> empty
+    in
+    (** Use the merging of the latest tag and the one being currently pushed.
+    This may be useful if for instance the latest tag changes the background and
+    the current one the foreground, so that the two effects are additioned. *)
+    let style = Terminal.merge (peek ()) style in
+    let () = style_stack := style :: !style_stack in
+    Terminal.eval style
+  in
+  let pop _ = match !style_stack with
+  | [] ->
+    (** Something went wrong, we fallback *)
+    Terminal.eval default
+  | _ :: rem ->
+    let () = style_stack := rem in
+    Terminal.eval (peek ())
+  in
+  let clear () = style_stack := [] in
+  push, pop, clear
+
+let error_tag =
+  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in
+  make ~style ["message"; "error"]
+
+let warning_tag =
+  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW () in
+  make ~style ["message"; "warning"]
+
+let debug_tag =
+  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in
+  make ~style ["message"; "debug"]
+
+let pp_tag t = match Pp.Tag.prj t tag with
+| None -> ""
+| Some key -> key
+
+let init_color_output () =
+  let push_tag, pop_tag, clear_tag = make_style_stack !tags in
+  let tag_handler = {
+    Format.mark_open_tag = push_tag;
+    Format.mark_close_tag = pop_tag;
+    Format.print_open_tag = ignore;
+    Format.print_close_tag = ignore;
+  } in
+  let open Pp_control in
+  let () = Format.pp_set_mark_tags !std_ft true in
+  let () = Format.pp_set_mark_tags !err_ft true in
+  let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in
+  let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in
+  let pptag = tag in
+  let open Pp in
+  let msg ?header ft strm =
+    let strm = match header with
+    | None -> hov 0 strm
+    | Some (h, t) ->
+      let tag = Pp.Tag.inj t pptag in
+      let h = Pp.tag tag (str h ++ str ":") in
+      hov 0 (h ++ spc () ++ strm)
+    in
+    pp_with ~pp_tag ft strm;
+    Format.pp_print_newline ft ();
+    Format.pp_print_flush ft ();
+    (** In case something went wrong, we reset the stack *)
+    clear_tag ();
+  in
+  let logger level strm = match level with
+  | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm
+  | Info -> msg !std_ft strm
+  | Notice -> msg !std_ft strm
+  | Warning ->
+    let header = ("Warning", warning_tag) in
+    Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
+  | Error -> msg ~header:("Error", error_tag) !err_ft strm
+  in
+  let () = set_logger logger in
+  ()
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
new file mode 100644
index 00000000..f5d6184c
--- /dev/null
+++ b/lib/ppstyle.mli
@@ -0,0 +1,70 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Highlighting of printers. Used for pretty-printing terms that should be
+    displayed on a color-capable terminal. *)
+
+(** {5 Style tags} *)
+
+type t
+(** Style tags *)
+
+val make : ?style:Terminal.style -> string list -> t
+(** Create a new tag with the given name. Each name must be unique. The optional
+    style is taken as the default one. *)
+
+val repr : t -> string list
+(** Gives back the original name of the style tag where each string has been
+    concatenated and separated with a dot. *)
+
+val tag : t Pp.Tag.key
+(** An annotation for styles *)
+
+(** {5 Manipulating global styles} *)
+
+val get_style : t -> Terminal.style option
+(** Get the style associated to a tag. *)
+
+val set_style : t -> Terminal.style option -> unit
+(** Set a style associated to a tag. *)
+
+val clear_styles : unit -> unit
+(** Clear all styles. *)
+
+val parse_config : string -> unit
+(** Add all styles from the given string as parsed by {!Terminal.parse}.
+    Unregistered tags are ignored. *)
+
+val dump : unit -> (t * Terminal.style option) list
+(** Recover the list of known tags together with their current style. *)
+
+(** {5 Setting color output} *)
+
+val init_color_output : unit -> unit
+(** Once called, all tags defined here will use their current style when
+    printed. To this end, this function redefines the loggers used when sending
+    messages to the user. The program will in particular use the formatters
+    {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages,
+    with additional syle information provided by this module. Be careful this is
+    not compatible with the Emacs mode! *)
+
+val pp_tag : Pp.tag_handler
+(** Returns the name of a style tag that is understandable by the formatters
+    that have been inititialized through {!init_color_output}. To be used with
+    {!Pp.pp_with}. *)
+
+(** {5 Tags} *)
+
+val error_tag : t
+(** Tag used by the {!Pp.msg_error} function. *)
+
+val warning_tag : t
+(** Tag used by the {!Pp.msg_warning} function. *)
+
+val debug_tag : t
+(** Tag used by the {!Pp.msg_debug} function. *)
diff --git a/lib/richpp.mli b/lib/richpp.mli
index bf80c8dc..a0d3c374 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -20,7 +20,7 @@ type 'annotation located = {
     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. *)
+    annotation. *)
 val rich_pp :
   (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds ->
   'annotation located Xml_datatype.gxml
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 9b63be70..851c6a22 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -45,26 +45,38 @@ end
 (* Common code *)
 let assert_ b s = if not b then Errors.anomaly (Pp.str s)
 
+(* According to http://caml.inria.fr/mantis/view.php?id=5325
+ * you can't use the same socket for both writing and reading (may change
+ * in 4.03 *)
 let mk_socket_channel () =
   let open Unix in
-  let s = socket PF_INET SOCK_STREAM 0 in
-  bind s (ADDR_INET (inet_addr_loopback,0));
-  listen s 1;
-  match getsockname s with
-  | ADDR_INET(host, port) ->
-      s, string_of_inet_addr host ^":"^ string_of_int port
+  let sr = socket PF_INET SOCK_STREAM 0 in
+  bind sr (ADDR_INET (inet_addr_loopback,0)); listen sr 1;
+  let sw = socket PF_INET SOCK_STREAM 0 in
+  bind sw (ADDR_INET (inet_addr_loopback,0)); listen sw 1;
+  match getsockname sr, getsockname sw with
+  | ADDR_INET(host, portr), ADDR_INET(_, portw) ->
+      (sr, sw),
+      string_of_inet_addr host
+        ^":"^ string_of_int portr ^":"^ string_of_int portw
   | _ -> assert false
 
-let accept s =
-  let r, _, _ = Unix.select [s] [] [] accept_timeout in
+let accept (sr,sw) =
+  let r, _, _ = Unix.select [sr] [] [] accept_timeout in
   if r = [] then raise (Failure (Printf.sprintf
     "The spawned process did not connect back in %2.1fs" accept_timeout));
-  let cs, _ = Unix.accept s in
-  Unix.close s;
-  let cin, cout = Unix.in_channel_of_descr cs, Unix.out_channel_of_descr cs in
+  let csr, _ = Unix.accept sr in
+  Unix.close sr;
+  let cin = Unix.in_channel_of_descr csr in
   set_binary_mode_in cin true;
+  let w, _, _ = Unix.select [sw] [] [] accept_timeout in
+  if w = [] then raise (Failure (Printf.sprintf
+    "The spawned process did not connect back in %2.1fs" accept_timeout));
+  let csw, _ = Unix.accept sw in
+  Unix.close sw;
+  let cout = Unix.out_channel_of_descr csw in
   set_binary_mode_out cout true;
-  cs, cin, cout
+  (csr, csw), cin, cout
 
 let handshake cin cout =
   try
@@ -116,7 +128,7 @@ let spawn_pipe env prog args =
   let cout = Unix.out_channel_of_descr master2worker_w in
   set_binary_mode_in cin true;
   set_binary_mode_out cout true;
-  pid, cin, cout, worker2master_r
+  pid, cin, cout, (worker2master_r, master2worker_w)
 
 let filter_args args =
   let rec aux = function
@@ -180,10 +192,10 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
 =
   let pid, oob_resp, oob_req, cin, cout, main, is_sock =
     spawn_with_control prefer_sock env prog args in
-  Unix.set_nonblock main;
+  Unix.set_nonblock (fst main);
   let gchan =
-    if is_sock then ML.async_chan_of_socket main
-    else ML.async_chan_of_file main in
+    if is_sock then ML.async_chan_of_socket (fst main)
+    else ML.async_chan_of_file (fst main) in
   let alive, watch = true, None in
   let p = { cin; cout; gchan; pid; oob_resp; oob_req; alive; watch } in
   p.watch <- Some (
diff --git a/lib/system.ml b/lib/system.ml
index 73095f9c..ddc56956 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -118,7 +118,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
@@ -126,7 +127,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
@@ -172,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;
-    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 -> error ("System error: " ^ 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 ->
-      error("System error: " ^ 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 a3d66d57..247d528b 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 -> 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
 
diff --git a/lib/terminal.ml b/lib/terminal.ml
index 0f6b23af..58851ed2 100644
--- a/lib/terminal.ml
+++ b/lib/terminal.ml
@@ -117,7 +117,7 @@ let is_extended = function
 | `INDEX _ | `RGB _ -> true
 | _ -> false
 
-let eval st =
+let repr st =
   let fg = match st.fg_color with
   | None -> []
   | Some c ->
@@ -152,7 +152,10 @@ let eval st =
   | Some true -> [7]
   | Some false -> [27]
   in
-  let tags = fg @ bg @ bold @ italic @ underline @ negative in
+  fg @ bg @ bold @ italic @ underline @ negative
+
+let eval st =
+  let tags = repr st in
   let tags = List.map string_of_int tags in
   Printf.sprintf "\027[%sm" (String.concat ";" tags)
 
diff --git a/lib/terminal.mli b/lib/terminal.mli
index f308ede3..49172e3c 100644
--- a/lib/terminal.mli
+++ b/lib/terminal.mli
@@ -46,6 +46,9 @@ val make : ?fg_color:color -> ?bg_color:color ->
 val merge : style -> style -> style
 (** [merge s1 s2] returns [s1] with all defined values of [s2] overwritten. *)
 
+val repr : style -> int list
+(** Generate the ANSI code representing the given style. *)
+
 val eval : style -> string
 (** Generate an escape sequence from a style. *)
 
diff --git a/lib/util.ml b/lib/util.ml
index a8c25f74..a20dba0f 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -132,3 +132,14 @@ let map_union f g = function
 type iexn = Exninfo.iexn
 
 let iraise = Exninfo.iraise
+
+let open_utf8_file_in fname =
+  let is_bom s =
+    Int.equal (Char.code s.[0]) 0xEF &&
+    Int.equal (Char.code s.[1]) 0xBB &&
+    Int.equal (Char.code s.[2]) 0xBF
+  in
+  let in_chan = open_in fname in
+  let s = "   " in
+  if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
+  in_chan
diff --git a/lib/util.mli b/lib/util.mli
index 4fce809c..1dc405fc 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -110,3 +110,6 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
 
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
+
+val open_utf8_file_in : string -> in_channel
+(** Open an utf-8 encoded file and skip the byte-order mark if any. *)
diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
index a33be9da..290f2c89 100644
--- a/lib/xml_lexer.mll
+++ b/lib/xml_lexer.mll
@@ -88,7 +88,8 @@ let error lexbuf e =
 let newline = ['\n']
 let break = ['\r']
 let space = [' ' '\t']
-let identchar =  ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-']
+let identchar =  ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.']
+let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar*
 let entitychar = ['A'-'Z' 'a'-'z']
 let pcchar = [^ '\r' '\n' '<' '>' '&']
 
@@ -226,7 +227,7 @@ and entity = parse
                 { raise (Error EUnterminatedEntity) }
 
 and ident_name = parse
-        | identchar+
+        | ident
                 { lexeme lexbuf }
         | _ | eof
                 { error lexbuf EIdentExpected }
@@ -252,7 +253,7 @@ and attributes = parse
                 }
 
 and attribute = parse
-        | identchar+
+        | ident
                 { lexeme lexbuf }
         | _ | eof
                 { error lexbuf EAttributeNameExpected }
@@ -281,6 +282,11 @@ and dq_string = parse
                         Buffer.add_char tmp (lexeme_char lexbuf 1);
                         dq_string lexbuf
                 }
+        | '&'
+                {
+                        Buffer.add_string tmp (entity lexbuf);
+                        dq_string lexbuf
+                }
         | eof
                 { raise (Error EUnterminatedString) }
         | _
@@ -297,6 +303,11 @@ and q_string = parse
                         Buffer.add_char tmp (lexeme_char lexbuf 1);
                         q_string lexbuf
                 }
+        | '&'
+                {
+                        Buffer.add_string tmp (entity lexbuf);
+                        q_string lexbuf
+                }
         | eof
                 { raise (Error EUnterminatedString) }
         | _
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
index cefb4af8..ac2eab35 100644
--- a/lib/xml_parser.mli
+++ b/lib/xml_parser.mli
@@ -36,10 +36,10 @@ type t
 
 (** Several exceptions can be raised when parsing an Xml document : {ul
         {li {!Xml.Error} is raised when an xml parsing error occurs. the
-                {!Xml.error_msg} tells you which error occured during parsing
-                and the {!Xml.error_pos} can be used to retreive the document
-                location where the error occured at.}
-        {li {!Xml.File_not_found} is raised when and error occured while
+                {!Xml.error_msg} tells you which error occurred during parsing
+                and the {!Xml.error_pos} can be used to retrieve the document
+                location where the error occurred at.}
+        {li {!Xml.File_not_found} is raised when an error occurred while
                 opening a file with the {!Xml.parse_file} function.}
         }
  *)
@@ -71,13 +71,13 @@ val error : error -> string
 (** Get the Xml error message as a string. *)
 val error_msg : error_msg -> string
 
-(** Get the line the error occured at. *)
+(** Get the line the error occurred at. *)
 val line : error_pos -> int
 
-(** Get the relative character range (in current line) the error occured at.*)
+(** Get the relative character range (in current line) the error occurred at.*)
 val range : error_pos -> int * int
 
-(** Get the absolute character range the error occured at. *)
+(** Get the absolute character range the error occurred at. *)
 val abs_range : error_pos -> int * int
 
 val pos : Lexing.lexbuf -> error_pos
@@ -98,7 +98,7 @@ val make : source -> t
  in the original Xmllight)}. *)
 val check_eof : t -> bool -> unit
 
-(** Once the parser is configurated, you can run the parser on a any kind
+(** Once the parser is configured, you can run the parser on a any kind
     of xml document source to parse its contents into an Xml data structure.
 
     When [do_not_canonicalize] is set, the XML document is given as
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
index eeddd53c..bbb7b51b 100644
--- a/lib/xml_printer.ml
+++ b/lib/xml_printer.ml
@@ -46,6 +46,8 @@ let buffer_attr tmp (n,v) =
     match v.[p] with
       | '\\' -> output "\\\\"
       | '"' -> output "\\\""
+      | '<' -> output "&lt;"
+      | '&' -> output "&amp;"
       | c -> output' c
   done;
   output' '"'