Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

52 files changed, 859 insertions, 518 deletions

diff --git a/ide/FAQ b/ide/FAQ
index 07b818246a..c8b0a5d328 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -1,7 +1,7 @@
 			CoqIde FAQ
 
 Q0) What is CoqIde?
-R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more informations.
+R0: A powerful graphical interface for Coq. See http://coq.inria.fr. for more informations.
 
 Q1) How to enable Emacs keybindings?
 R1: Insert 
diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template
index e224e81204..fbe7773dd4 100644
--- a/ide/MacOS/Info.plist.template
+++ b/ide/MacOS/Info.plist.template
@@ -66,7 +66,7 @@
 	<key>CFBundleGetInfoString</key>
 	<string>Coq_vVERSION</string>
 	<key>NSHumanReadableCopyright</key>
-	<string>Copyright 1999-2015, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string>
+	<string>Copyright 1999-2016, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string>
 	<key>CFBundleHelpBookFolder</key>
 	<string>share/doc/coq/html/</string>
 	<key>CFAppleHelpAnchor</key>
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 3671535680..ac9cc57bc0 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coq.ml b/ide/coq.ml
index d061df6fd0..fa0adf979c 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -99,9 +99,6 @@ let display_coqtop_answer cmd lines =
      "Command was: "^cmd^"\n"^
      "Answer was: "^(String.concat "\n  " lines))
 
-let check_remaining_opt arg =
-  if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg)
-
 let rec filter_coq_opts args =
   let argstr = String.concat " " (List.map Filename.quote args) in
   let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in
@@ -200,8 +197,6 @@ module GlibMainLoop = struct
   let read_all = Ideutils.io_read_all
   let async_chan_of_file fd = Glib.Io.channel_of_descr fd
   let async_chan_of_socket s = !gio_channel_of_descr_socket s
-  let add_timeout ~sec callback =
-    ignore(Glib.Timeout.add ~ms:(sec * 1000) ~callback)
 end
 
 module CoqTop = Spawn.Async(GlibMainLoop)
@@ -302,13 +297,13 @@ let handle_intermediate_message handle xml =
   let logger = match handle.waiting_for with
     | Some (_, l) -> l 
     | None -> function
-        | Pp.Error -> Minilib.log ~level:`ERROR
-        | Pp.Info -> Minilib.log ~level:`INFO
-        | Pp.Notice -> Minilib.log ~level:`NOTICE
-        | Pp.Warning -> Minilib.log ~level:`WARNING
-        | Pp.Debug _ -> Minilib.log ~level:`DEBUG
+        | Pp.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s)
+        | Pp.Info -> fun s -> Minilib.log ~level:`INFO  (xml_to_string s)
+        | Pp.Notice -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
+        | Pp.Warning -> fun s -> Minilib.log ~level:`WARNING  (xml_to_string s)
+        | Pp.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s)
   in
-  logger level content
+  logger level (Richpp.richpp_of_xml content)
 
 let handle_feedback feedback_processor xml =
   let feedback = Feedback.to_feedback xml in
@@ -336,7 +331,7 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
   let lex = Lexing.from_string s in
   let p = Xml_parser.make (Xml_parser.SLexbuf lex) in
   let rec loop () =
-    let xml = Xml_parser.parse p in
+    let xml = Xml_parser.parse ~do_not_canonicalize:true p in
     let l_end = Lexing.lexeme_end lex in
     state.fragment <- String.sub s l_end (String.length s - l_end);
     state.lexerror <- None;
@@ -465,10 +460,6 @@ let close_coqtop coqtop =
 
 let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop
 
-let break_coqtop coqtop =
-  try !interrupter (CoqTop.unixpid coqtop.handle.proc)
-  with _ -> Minilib.log "Error while sending Ctrl-C"
-
 let get_arguments coqtop = coqtop.sup_args
 
 let set_arguments coqtop args =
@@ -518,6 +509,17 @@ let search flags = eval_call (Xmlprotocol.search flags)
 let init x = eval_call (Xmlprotocol.init x)
 let stop_worker x = eval_call (Xmlprotocol.stop_worker x)
 
+let break_coqtop coqtop workers =
+  if coqtop.status = Busy then
+    try !interrupter (CoqTop.unixpid coqtop.handle.proc)
+    with _ -> Minilib.log "Error while sending Ctrl-C"
+  else
+    let rec aux = function
+    | [] -> Void
+    | w :: ws -> stop_worker w coqtop.handle (fun _ -> aux ws)
+    in
+      let Void = aux workers in ()
+
 module PrintOpt =
 struct
   type t = string list
diff --git a/ide/coq.mli b/ide/coq.mli
index a72c67b43e..7cef6a4d0a 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -16,7 +16,7 @@ type coqtop
     Liveness management of coqtop is automatic. Whenever a coqtop dies abruptly,
     this module is responsible for relaunching the whole process. The reset
     handler set through [set_reset_handler] will be called after such an
-    abrupt failure. It is also called when explicitely requesting coqtop to
+    abrupt failure. It is also called when explicitly requesting coqtop to
     reset. *)
 
 type 'a task
@@ -29,7 +29,7 @@ type 'a task
     ([is_computing] will answer [true]), and any other task submission
     will be rejected by [try_grab].
 
-    Any exception occuring within the task will trigger a coqtop reset.
+    Any exception occurring within the task will trigger a coqtop reset.
 
     Beware, because of the GTK scheduler, you never know when a task will
     actually be executed. If you need to sequentialize imperative actions, you
@@ -43,7 +43,7 @@ val bind : 'a task -> ('a -> 'b task) -> 'b task
 (** Monadic binding of tasks *)
 
 val lift : (unit -> 'a) -> 'a task
-(** Return the impertative computation waiting to be processed. *)
+(** Return the imperative computation waiting to be processed. *)
 
 val seq : unit task -> 'a task -> 'a task
 (** Sequential composition *)
@@ -70,8 +70,8 @@ val init_coqtop : coqtop -> unit task -> unit
 (** Finish initializing a freshly spawned coqtop, by running a first task on it.
     The task should run its inner continuation at the end. *)
 
-val break_coqtop : coqtop -> unit
-(** Interrupt the current computation of coqtop. *)
+val break_coqtop : coqtop -> string list -> unit
+(** Interrupt the current computation of coqtop or the worker if coqtop it not running. *)
 
 val close_coqtop : coqtop -> unit
 (** Close coqtop. Subsequent requests will be discarded. Hook ignored. *)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 2cffdf816e..aa1a75db60 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -164,8 +164,65 @@ let flags_to_color f =
   else if List.mem `INCOMPLETE f then `NAME "gray"
   else `NAME Preferences.processed_color#get
 
+let validate s =
+  let open Xml_datatype in
+  let rec validate = function
+  | PCData s -> Glib.Utf8.validate s
+  | Element (_, _, children) -> List.for_all validate children
+  in
+  validate (Richpp.repr s)
+
 module Doc = Document
 
+let segment_model (doc : sentence Doc.document) : Wg_Segment.model =
+object (self)
+
+  val mutable cbs = []
+
+  val mutable document_length = 0
+
+  method length = document_length
+
+  method changed ~callback = cbs <- callback :: cbs
+
+  method fold : 'a. ('a -> Wg_Segment.color -> 'a) -> 'a -> 'a = fun f accu ->
+    let fold accu _ _ s =
+      let flags = List.map mem_flag_of_flag s.flags in
+      f accu (flags_to_color flags)
+    in
+    Doc.fold_all doc accu fold
+
+  method private on_changed (i, f) =
+    let data = (i, flags_to_color f) in
+    List.iter (fun f -> f (`SET data)) cbs
+
+  method private on_push s ctx =
+    let after = match ctx with
+    | None -> []
+    | Some (l, _) -> l
+    in
+    List.iter (fun s -> set_index s (s.index + 1)) after;
+    set_index s (document_length - List.length after);
+    ignore ((SentenceId.connect s)#changed self#on_changed);
+    document_length <- document_length + 1;
+    List.iter (fun f -> f `INSERT) cbs
+
+  method private on_pop s ctx =
+    let () = match ctx with
+    | None -> ()
+    | Some (l, _) -> List.iter (fun s -> set_index s (s.index - 1)) l
+    in
+    set_index s (-1);
+    document_length <- document_length - 1;
+    List.iter (fun f -> f `REMOVE) cbs
+
+  initializer
+    let _ = (Doc.connect doc)#pushed self#on_push in
+    let _ = (Doc.connect doc)#popped self#on_pop in
+    ()
+
+end
+
 class coqops
   (_script:Wg_ScriptView.script_view)
   (_pv:Wg_ProofView.proof_view)
@@ -198,20 +255,8 @@ object(self)
     script#misc#set_has_tooltip true;
     ignore(script#misc#connect#query_tooltip ~callback:self#tooltip_callback);
     feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback;
-    let on_changed (i, f) = segment#add i (flags_to_color f) in
-    let on_push s =
-      set_index s document_length;
-      (SentenceId.connect s)#changed on_changed;
-      document_length <- succ document_length;
-      segment#set_length document_length;
-      let flags = List.map mem_flag_of_flag s.flags in
-      segment#add s.index (flags_to_color flags);
-    in
-    let on_pop s =
-      set_index s (-1);
-      document_length <- pred document_length;
-      segment#set_length document_length;
-    in
+    let md = segment_model document in
+    segment#set_model md;
     let on_click id =
       let find _ _ s = Int.equal s.index id in
       let sentence = Doc.find document find in
@@ -227,8 +272,6 @@ object(self)
       script#buffer#place_cursor iter;
       ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
     in
-    let _ = (Doc.connect document)#pushed on_push in
-    let _ = (Doc.connect document)#popped on_pop in
     let _ = segment#connect#clicked on_click in
     ()
 
@@ -319,7 +362,7 @@ object(self)
   method raw_coq_query phrase =
     let action = log "raw_coq_query starting now" in
     let display_error s =
-      if not (Glib.Utf8.validate s) then
+      if not (validate s) then
         flash_info "This error is so nasty that I can't even display it."
       else messages#add s;
     in
@@ -328,7 +371,7 @@ object(self)
     let next = function
     | Fail (_, _, err) -> display_error err; Coq.return ()
     | Good msg ->
-      messages#add msg; Coq.return ()
+      messages#add_string msg; Coq.return ()
     in
     Coq.bind (Coq.seq action query) next
 
@@ -556,7 +599,7 @@ object(self)
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
         | `Skip(start,stop), [] ->
-            logger Pp.Error "You muse close the proof with Qed or Admitted";
+            logger Pp.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
             self#discard_command_queue queue;
             conclude [] 
         | `Skip(start,stop), (_,s) :: topstack ->
@@ -572,7 +615,7 @@ object(self)
             let handle_answer = function
               | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
                   Doc.assign_tip_id document id;
-                  logger Pp.Notice msg;
+                  logger Pp.Notice (Richpp.richpp_of_string msg);
                   self#commit_queue_transaction sentence;
                   loop id []
               | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -580,7 +623,7 @@ object(self)
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
                   self#cleanup (Doc.cut_at document tip);
-                  logger Pp.Notice msg;
+                  logger Pp.Notice (Richpp.richpp_of_string msg);
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
                   else loop tip (List.rev topstack)
@@ -599,7 +642,7 @@ object(self)
    let next = function
      | Good _ ->
          messages#clear;
-         messages#push Pp.Info "All proof terms checked by the kernel";
+         messages#push Pp.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
          Coq.return ()
      | Fail x -> self#handle_failure x in
    Coq.bind (Coq.status ~logger:messages#push true) next
@@ -693,7 +736,7 @@ object(self)
           self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
-          if loc <> None then messages#push Pp.Error "Fixme LOC";
+          if loc <> None then messages#push Pp.Error (Richpp.richpp_of_string "Fixme LOC");
           messages#push Pp.Error msg;
           if Stateid.equal safe_id Stateid.dummy then self#show_goals
           else undo safe_id
@@ -769,7 +812,7 @@ object(self)
       self#show_goals
     in
     let display_error (loc, s) =
-      if not (Glib.Utf8.validate s) then
+      if not (validate s) then
         flash_info "This error is so nasty that I can't even display it."
       else messages#add s
     in
@@ -779,10 +822,10 @@ object(self)
       let next = function
       | Fail (_, l, str) -> (* FIXME: check *)
         display_error (l, str);
-        messages#add ("Unsuccessfully tried: "^phrase);
+        messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase));
         more
       | Good msg ->
-        messages#add msg;
+        messages#add_string msg;
         stop Tags.Script.processed
       in
       Coq.bind (Coq.seq action query) next
@@ -826,7 +869,10 @@ object(self)
   method initialize =
     let get_initial_state =
       let next = function
-      | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return ()
+      | Fail (_, _, message) ->
+        let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in
+        let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in
+        ignore (popup#run ()); exit 1
       | Good id -> initial_state <- id; Coq.return () in
       Coq.bind (Coq.init (get_filename ())) next in
     Coq.seq get_initial_state Coq.PrintOpt.enforce
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 8e76d3b270..4a37a1fa55 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 37e38a5464..d55e7f9dd7 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index e333c0b24c..b6286c49fb 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 6769ce768b..1fe393d2b9 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -318,10 +318,10 @@ let export kind sn =
         local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^
         (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
       in
-      sn.messages#set ("Running: "^cmd);
+      sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
       let finally st = flash_info (cmd ^ pr_exit_status st)
       in
-      run_command sn.messages#add finally cmd
+      run_command (fun msg -> sn.messages#add_string msg) finally cmd
 
 let export kind = cb_on_current_term (export kind)
 
@@ -431,9 +431,9 @@ let compile sn =
 	^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
-      sn.messages#set ("Running: "^cmd);
+      sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
       let display s =
-        sn.messages#add s;
+        sn.messages#add_string s;
         Buffer.add_string buf s
       in
       let finally st =
@@ -441,8 +441,8 @@ let compile sn =
           flash_info (f ^ " successfully compiled")
         else begin
           flash_info (f ^ " failed to compile");
-          sn.messages#set "Compilation output:\n";
-          sn.messages#add (Buffer.contents buf);
+          sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
+          sn.messages#add (Richpp.richpp_of_string (Buffer.contents buf));
         end
       in
       run_command display finally cmd
@@ -464,13 +464,13 @@ let make sn =
     |Some f ->
       File.saveall ();
       let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in
-      sn.messages#set "Compilation output:\n";
+      sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
       Buffer.reset last_make_buf;
       last_make := "";
       last_make_index := 0;
       last_make_dir := Filename.dirname f;
       let display s =
-        sn.messages#add s;
+        sn.messages#add_string s;
         Buffer.add_string last_make_buf s
       in
       let finally st = flash_info (cmd_make#get ^ pr_exit_status st)
@@ -508,11 +508,11 @@ let next_error sn =
     let stopi = b#get_iter_at_byte ~line:(line-1) stop in
     b#apply_tag Tags.Script.error ~start:starti ~stop:stopi;
     b#place_cursor ~where:starti;
-    sn.messages#set error_msg;
+    sn.messages#set (Richpp.richpp_of_string error_msg);
     sn.script#misc#grab_focus ()
   with Not_found ->
     last_make_index := 0;
-    sn.messages#set "No more errors.\n"
+    sn.messages#set (Richpp.richpp_of_string "No more errors.\n")
 
 let next_error = cb_on_current_term next_error
 
@@ -570,7 +570,7 @@ module Nav = struct
   let restart _ = on_current_term restart
   let interrupt sn =
     Minilib.log "User break received";
-    Coq.break_coqtop sn.coqtop
+    Coq.break_coqtop sn.coqtop CString.(Set.elements (Map.domain sn.jobpage#data))
   let interrupt = cb_on_current_term interrupt
   let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document)
 end
@@ -718,7 +718,7 @@ let initial_about () =
     else ""
   in
   let msg = initial_string ^ version_info ^ log_file_message () in
-  on_current_term (fun term -> term.messages#add msg)
+  on_current_term (fun term -> term.messages#add_string msg)
 
 let coq_icon () =
   (* May raise Nof_found *)
@@ -783,7 +783,7 @@ let coqtop_arguments sn =
         let args = String.concat " " args in
         let msg = Printf.sprintf "Invalid arguments: %s" args in
         let () = sn.messages#clear in
-        sn.messages#push Pp.Error msg
+        sn.messages#push Pp.Error (Richpp.richpp_of_string msg)
     else dialog#destroy ()
   in
   let _ = entry#connect#activate ok_cb in
@@ -1059,8 +1059,8 @@ let build_ui () =
     ("Hide", "_Hide", `MISSING_IMAGE,
         ~callback:(fun _ -> let sess = notebook#current_term in
           toggle_proof_visibility sess.buffer sess.analyzed_view#get_insert), "Hide proof", "h"); *)
-    ("Previous", "_Previous", `GO_BACK, Nav.previous_occ, "Previous occurence", "less");
-    ("Next", "_Next", `GO_FORWARD, Nav.next_occ, "Next occurence", "greater");
+    ("Previous", "_Previous", `GO_BACK, Nav.previous_occ, "Previous occurrence", "less");
+    ("Next", "_Next", `GO_FORWARD, Nav.next_occ, "Next occurrence", "greater");
     ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f");
   ] end;
 
@@ -1140,17 +1140,17 @@ let build_ui () =
     item "Help" ~label:"_Help";
     item "Browse Coq Manual" ~label:"Browse Coq _Manual"
       ~callback:(fun _ ->
-        browse notebook#current_term.messages#add (doc_url ()));
+        browse notebook#current_term.messages#add_string (doc_url ()));
     item "Browse Coq Library" ~label:"Browse Coq _Library"
       ~callback:(fun _ ->
-        browse notebook#current_term.messages#add library_url#get);
+        browse notebook#current_term.messages#add_string library_url#get);
     item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP
       ~callback:(fun _ -> on_current_term (fun sn ->
-        browse_keyword sn.messages#add (get_current_word sn)));
+        browse_keyword sn.messages#add_string (get_current_word sn)));
     item "Help for μPG mode" ~label:"Help for μPG mode"
       ~callback:(fun _ -> on_current_term (fun sn ->
          sn.messages#clear;
-         sn.messages#add (NanoPG.get_documentation ())));
+         sn.messages#add_string (NanoPG.get_documentation ())));
     item "About Coq" ~label:"_About" ~stock:`ABOUT
       ~callback:MiscMenu.about
   ];
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 6691512845..744b974ffa 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index db69ec661f..534a3f179d 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/document.ml b/ide/document.ml
index 9823e7576c..62457fe56b 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -16,8 +16,8 @@ type id = Stateid.t
 
 class type ['a] signals =
   object
-    method popped : callback:('a -> unit) -> unit
-    method pushed : callback:('a -> unit) -> unit
+    method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit
+    method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit
   end
 
 class ['a] signal () =
@@ -32,14 +32,14 @@ end
 type 'a document = {
   mutable stack : 'a sentence list;
   mutable context : ('a sentence list * 'a sentence list) option;
-  pushed_sig : 'a signal;
-  popped_sig : 'a signal;
+  pushed_sig : ('a * ('a list * 'a list) option) signal;
+  popped_sig : ('a * ('a list * 'a list) option) signal;
 }
 
-let connect d =
+let connect d : 'a signals =
   object
-    method pushed ~callback = d.pushed_sig#connect callback
-    method popped ~callback = d.popped_sig#connect callback
+    method pushed ~callback = d.pushed_sig#connect (fun (x, ctx) -> callback x ctx)
+    method popped ~callback = d.popped_sig#connect (fun (x, ctx) -> callback x ctx)
   end
 
 let create () = {
@@ -49,6 +49,12 @@ let create () = {
   popped_sig = new signal ();
 }
 
+let repr_context s = match s.context with
+| None -> None
+| Some (cl, cr) ->
+  let map s = s.data in
+  Some (List.map map cl, List.map map cr)
+
 (* Invariant, only the tip is a allowed to have state_id = None *)
 let invariant l = l = [] || (List.hd l).state_id <> None
 
@@ -64,12 +70,13 @@ let tip_data = function
 let push d x =
   assert(invariant d.stack);
   d.stack <- { data = x; state_id = None } :: d.stack;
-  d.pushed_sig#call x
+  d.pushed_sig#call (x, repr_context d)
 
 let pop = function
   | { stack = [] } -> raise Empty
-  | { stack = { data }::xs } as s -> s.stack <- xs; s.popped_sig#call data; data
-  
+  | { stack = { data }::xs } as s ->
+    s.stack <- xs; s.popped_sig#call (data, repr_context s); data
+
 let focus d ~cond_top:c_start ~cond_bot:c_stop =
   assert(invariant d.stack);
   if d.context <> None then invalid_arg "focus";
@@ -124,12 +131,6 @@ let context d =
   let pair _ x y = try Option.get x, y with Option.IsNone -> assert false in
   List.map (flat pair true) top, List.map (flat pair true) bot
 
-let iter d f =
-  let a, s, b = to_lists d in
-  List.iter (flat f false) a;
-  List.iter (flat f true)  s;
-  List.iter (flat f false) b
-  
 let stateid_opt_equal = Option.equal Stateid.equal
 
 let is_in_focus d id =
@@ -154,7 +155,7 @@ let cut_at d id =
     if stateid_opt_equal state_id (Some id) then CSig.Stop (n, zone)
     else CSig.Cont (n + 1, data :: zone) in
   let n, zone = CList.fold_left_until aux (0, []) d.stack in
-  for i = 1 to n do ignore(pop d) done;
+  for _i = 1 to n do ignore(pop d) done;
   List.rev zone
 
 let find_id d f =
diff --git a/ide/document.mli b/ide/document.mli
index 0d803ff003..fb96cb6d76 100644
--- a/ide/document.mli
+++ b/ide/document.mli
@@ -108,8 +108,8 @@ val print :
 
 class type ['a] signals =
   object
-    method popped : callback:('a -> unit) -> unit
-    method pushed : callback:('a -> unit) -> unit
+    method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit
+    method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit
   end
 
 val connect : 'a document -> 'a signals
diff --git a/ide/fileOps.ml b/ide/fileOps.ml
index eccd61d0d9..7be1bdb927 100644
--- a/ide/fileOps.ml
+++ b/ide/fileOps.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/fileOps.mli b/ide/fileOps.mli
index 48b7c8f656..9f0b75ac56 100644
--- a/ide/fileOps.mli
+++ b/ide/fileOps.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index 79ccf61a43..f905053ddb 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 94f9c9a361..9a3e85e47d 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -130,7 +130,8 @@ let annotate phrase =
 
 (** Goal display *)
 
-let hyp_next_tac sigma env (id,_,ast) =
+let hyp_next_tac sigma env decl =
+  let (id,_,ast) = Context.Named.Declaration.to_tuple decl in
   let id_s = Names.Id.to_string id in
   let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in
   [
@@ -184,14 +185,19 @@ let process_goal sigma g =
   let id = Goal.uid g in
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-    string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in
+    Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
+  in
   let process_hyp d (env,l) =
-    let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in
-    let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
+    let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in
+    let d' = List.map (fun name -> let open Context.Named.Declaration in
+                                   match pi2 d with
+                                   | None -> LocalAssum (name, pi3 d)
+                                   | Some value -> LocalDef (name, value, pi3 d))
+                      (pi1 d) in
       (List.fold_right Environ.push_named d' env,
-       (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
+       (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in
   let (_env, hyps) =
-    Context.fold_named_list_context process_hyp
+    Context.NamedList.fold process_hyp
       (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
   { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
@@ -291,11 +297,13 @@ let export_option_value = function
   | Goptions.BoolValue b   -> Interface.BoolValue b
   | Goptions.IntValue x    -> Interface.IntValue x
   | Goptions.StringValue s -> Interface.StringValue s
+  | Goptions.StringOptValue s -> Interface.StringOptValue s
 
 let import_option_value = function
   | Interface.BoolValue b   -> Goptions.BoolValue b
   | Interface.IntValue x    -> Goptions.IntValue x
   | Interface.StringValue s -> Goptions.StringValue s
+  | Interface.StringOptValue s -> Goptions.StringOptValue s
 
 let export_option_state s = {
   Interface.opt_sync  = s.Goptions.opt_sync;
@@ -314,6 +322,8 @@ let set_options options =
   | BoolValue b -> Goptions.set_bool_option_value name b
   | IntValue i -> Goptions.set_int_option_value name i
   | StringValue s -> Goptions.set_string_option_value name s
+  | StringOptValue (Some s) -> Goptions.set_string_option_value name s
+  | StringOptValue None -> Goptions.unset_option_value_gen None name
   in
   List.iter iter options
 
@@ -329,10 +339,14 @@ let handle_exn (e, info) =
   let loc_of e = match Loc.get_loc e with
     | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
     | _ -> None in
-  let mk_msg () = read_stdout ()^"\n"^string_of_ppcmds (Errors.print ~info e) in
+  let mk_msg () =
+    let msg = read_stdout () in
+    let msg = str msg ++ fnl () ++ Errors.print ~info e in
+    Richpp.richpp_of_pp msg
+  in
   match e with
-  | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!"
-  | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!"
+  | Errors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!"
+  | Errors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!"
   | e ->
       match Stateid.get info with
       | Some (valid, _) -> valid, loc_of info, mk_msg ()
@@ -357,6 +371,7 @@ let init =
                0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
            else Stm.get_current_state (), `NewTip in
          Stm.set_compilation_hints file;
+         Stm.finish ();
          initial_id
    end
 
@@ -428,12 +443,12 @@ let print_xml =
 
 let slave_logger xml_oc level message =
   (* convert the message into XML *)
-  let msg = string_of_ppcmds (hov 0 message) in
+  let msg = hov 0 message in
   let message = {
     Pp.message_level = level;
-    Pp.message_content = msg;
+    Pp.message_content = (Richpp.repr (Richpp.richpp_of_pp msg));
   } in
-  let () = pr_debug (Printf.sprintf "-> %S" msg) in
+  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
   let xml = Pp.of_message message in
   print_xml xml_oc xml
 
@@ -465,7 +480,7 @@ let loop () =
     try
       let xml_query = Xml_parser.parse xml_ic in
 (*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
-      let q = Xmlprotocol.to_call xml_query in
+      let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in
       let () = pr_debug_call q in
       let r = eval_call xml_oc (slave_logger xml_oc Pp.Notice) q in
       let () = pr_debug_answer q r in
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 053bba805d..508881cad8 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,8 +9,6 @@
 
 open Preferences
 
-exception Forbidden
-
 let warn_image () =
   let img = GMisc.image () in
   img#set_stock `DIALOG_WARNING;
@@ -31,13 +29,40 @@ let push_info,pop_info,clear_info =
   let size = ref 0 in
   (fun s -> incr size; ignore (status_context#push s)),
   (fun () -> decr size; status_context#pop ()),
-  (fun () -> for i = 1 to !size do status_context#pop () done; size := 0)
+  (fun () -> for _i = 1 to !size do status_context#pop () done; size := 0)
 
 let flash_info =
   let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
-
+let xml_to_string xml =
+  let open Xml_datatype in
+  let buf = Buffer.create 1024 in
+  let rec iter = function
+  | PCData s -> Buffer.add_string buf s
+  | Element (_, _, children) ->
+    List.iter iter children
+  in
+  let () = iter (Richpp.repr xml) in
+  Buffer.contents buf
+
+let translate s = s
+
+let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg =
+  let open Xml_datatype in
+  let tag name =
+    let name = translate name in
+    match GtkText.TagTable.lookup buf#tag_table name with
+    | None -> raise Not_found
+    | Some tag -> new GText.tag tag
+  in
+  let rec insert tags = function
+  | PCData s -> buf#insert ~tags:(List.rev tags) s
+  | Element (t, _, children) ->
+    let tags = try tag t :: tags with Not_found -> tags in
+    List.iter (fun xml -> insert tags xml) children
+  in
+  insert tags (Richpp.repr msg)
 
 let set_location = ref  (function s -> failwith "not ready")
 
@@ -272,7 +297,7 @@ let textview_width (view : #GText.view_skel) =
   let char_width = GPango.to_pixels metrics#approx_char_width in
   pixel_width / char_width
 
-type logger = Pp.message_level -> string -> unit
+type logger = Pp.message_level -> Richpp.richpp -> unit
 
 let default_logger level message =
   let level = match level with
@@ -282,7 +307,7 @@ let default_logger level message =
   | Pp.Warning -> `WARNING
   | Pp.Error -> `ERROR
   in
-  Minilib.log ~level message
+  Minilib.log ~level (xml_to_string message)
 
 
 (** {6 File operations} *)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 1fb30e4d72..4e35a6f9fa 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -52,6 +52,11 @@ val pop_info : unit -> unit
 val clear_info : unit -> unit
 val flash_info : ?delay:int -> string -> unit
 
+val xml_to_string : Richpp.richpp -> string
+
+val insert_xml : ?tags:GText.tag list ->
+  #GText.buffer_skel -> Richpp.richpp -> unit
+
 val set_location : (string -> unit) ref
 
 (* In win32, when a command-line is to be executed via cmd.exe
@@ -64,9 +69,9 @@ val requote : string -> string
 val textview_width : #GText.view_skel -> int
 (** Returns an approximate value of the character width of a textview *)
 
-type logger = Pp.message_level -> string -> unit
+type logger = Pp.message_level -> Richpp.richpp -> unit
 
-val default_logger : Pp.message_level -> string -> unit
+val default_logger : logger
 (** Default logger. It logs messages that the casual user should not see. *)
 
 (** {6 I/O operations} *)
diff --git a/ide/interface.mli b/ide/interface.mli
index 464e851f6d..2a9b8b241f 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,14 +12,15 @@
 
 type raw = bool
 type verbose = bool
+type richpp = Richpp.richpp
 
 (** The type of coqtop goals *)
 type goal = {
   goal_id : string;
   (** Unique goal identifier *)
-  goal_hyp : string list;
+  goal_hyp : richpp list;
   (** List of hypotheses *)
-  goal_ccl : string;
+  goal_ccl : richpp;
   (** Goal conclusion *)
 }
 
@@ -61,6 +62,7 @@ type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
+  | StringOptValue of string option
 
 (** Summary of an option status *)
 type option_state = {
@@ -117,7 +119,7 @@ type edit_id = Feedback.edit_id
    should probably retract to that point *)
 type 'a value =
   | Good of 'a
-  | Fail of (state_id * location * string)
+  | Fail of (state_id * location * richpp)
 
 type ('a, 'b) union = ('a, 'b) Util.union
 
@@ -201,7 +203,7 @@ type about_sty = unit
 type about_rty = coq_info
 
 type handle_exn_sty = Exninfo.iexn
-type handle_exn_rty = state_id * location * string
+type handle_exn_rty = state_id * location * richpp
 
 (* Retrocompatibility stuff *)
 type interp_sty = (raw * verbose) * string
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml
index 0668ad09f4..93bdeb324c 100644
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 8520cce0d2..addea9074a 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -17,6 +17,14 @@ let style_manager = GSourceView2.source_style_scheme_manager ~default:true
 let () = style_manager#set_search_path
   ((Minilib.coqide_data_dirs ())@style_manager#search_path)
 
+type tag = {
+  tag_fg_color : string option;
+  tag_bg_color : string option;
+  tag_bold : bool;
+  tag_italic : bool;
+  tag_underline : bool;
+}
+
 (** Generic preferences *)
 
 type obj = {
@@ -170,6 +178,30 @@ object
   | _ -> None
 end
 
+let tag : tag repr =
+let _to s = if s = "" then None else Some s in
+let _of = function None -> "" | Some s -> s in
+object
+  method from tag = [
+    _of tag.tag_fg_color;
+    _of tag.tag_bg_color;
+    string_of_bool tag.tag_bold;
+    string_of_bool tag.tag_italic;
+    string_of_bool tag.tag_underline;
+  ]
+  method into = function
+  | [fg; bg; bd; it; ul] ->
+    (try Some {
+      tag_fg_color = _to fg;
+      tag_bg_color = _to bg;
+      tag_bold = bool_of_string bd;
+      tag_italic = bool_of_string it;
+      tag_underline = bool_of_string ul;
+      }
+    with _ -> None)
+  | _ -> None
+end
+
 end
 
 let get_config_file name =
@@ -248,8 +280,19 @@ let automatic_tactics =
 let cmd_print =
   new preference ~name:["cmd_print"] ~init:"lpr" ~repr:Repr.(string)
 
+let attach_modifiers (pref : string preference) prefix =
+  let cb mds =
+    let mds = str_to_mod_list mds in
+    let change ~path ~key ~modi ~changed =
+      if CString.is_sub prefix path 0 then
+        ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path)
+    in
+    GtkData.AccelMap.foreach change
+  in
+  pref#connect#changed cb
+
 let modifier_for_navigation =
-  new preference ~name:["modifier_for_navigation"] ~init:"<Control><Alt>" ~repr:Repr.(string)
+  new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string)
 
 let modifier_for_templates =
   new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string)
@@ -260,6 +303,11 @@ let modifier_for_tactics =
 let modifier_for_display =
   new preference ~name:["modifier_for_display"] ~init:"<Alt><Shift>" ~repr:Repr.(string)
 
+let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/"
+let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/"
+let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/"
+let _ = attach_modifiers modifier_for_display "<Actions>/View/"
+
 let modifiers_valid =
   new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string)
 
@@ -338,6 +386,89 @@ let processing_color =
 let _ = attach_bg processing_color Tags.Script.to_process
 let _ = attach_bg processing_color Tags.Script.incomplete
 
+let default_tag = {
+  tag_fg_color = None;
+  tag_bg_color = None;
+  tag_bold = false;
+  tag_italic = false;
+  tag_underline = false;
+}
+
+let tags = ref Util.String.Map.empty
+
+let list_tags () = !tags
+
+let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) () = {
+  tag_fg_color = fg;
+  tag_bg_color = bg;
+  tag_bold = bold;
+  tag_italic = italic;
+  tag_underline = underline;
+}
+
+let create_tag name default =
+  let pref = new preference ~name:[name] ~init:default ~repr:Repr.(tag) in
+  let set_tag tag =
+    begin match pref#get.tag_bg_color with
+    | None -> tag#set_property (`BACKGROUND_SET false)
+    | Some c ->
+      tag#set_property (`BACKGROUND_SET true);
+      tag#set_property (`BACKGROUND c)
+    end;
+    begin match pref#get.tag_fg_color with
+    | None -> tag#set_property (`FOREGROUND_SET false)
+    | Some c ->
+      tag#set_property (`FOREGROUND_SET true);
+      tag#set_property (`FOREGROUND c)
+    end;
+    begin match pref#get.tag_bold with
+    | false -> tag#set_property (`WEIGHT_SET false)
+    | true ->
+      tag#set_property (`WEIGHT_SET true);
+      tag#set_property (`WEIGHT `BOLD)
+    end;
+    begin match pref#get.tag_italic with
+    | false -> tag#set_property (`STYLE_SET false)
+    | true ->
+      tag#set_property (`STYLE_SET true);
+      tag#set_property (`STYLE `ITALIC)
+    end;
+    begin match pref#get.tag_underline with
+    | false -> tag#set_property (`UNDERLINE_SET false)
+    | true ->
+      tag#set_property (`UNDERLINE_SET true);
+      tag#set_property (`UNDERLINE `SINGLE)
+    end;
+  in
+  let iter table =
+    let tag = GText.tag ~name () in
+    table#add tag#as_tag;
+    pref#connect#changed (fun _ -> set_tag tag);
+    set_tag tag;
+  in
+  List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
+  tags := Util.String.Map.add name pref !tags
+
+let () =
+  let iter (name, tag) = create_tag name tag in
+  List.iter iter [
+    ("constr.evar", make_tag ());
+    ("constr.keyword", make_tag ~fg:"dark green" ());
+    ("constr.notation", make_tag ());
+    ("constr.path", make_tag ());
+    ("constr.reference", make_tag ~fg:"navy"());
+    ("constr.type", make_tag ~fg:"#008080" ());
+    ("constr.variable", make_tag ());
+    ("message.debug", make_tag ());
+    ("message.error", make_tag ());
+    ("message.warning", make_tag ());
+    ("module.definition", make_tag ~fg:"orange red" ~bold:true ());
+    ("module.keyword", make_tag ());
+    ("tactic.keyword", make_tag ());
+    ("tactic.primitive", make_tag ());
+    ("tactic.string", make_tag ());
+  ]
+
 let processed_color =
   new preference ~name:["processed_color"] ~init:"light green" ~repr:Repr.(string)
 
@@ -384,6 +515,74 @@ let highlight_current_line =
 let nanoPG =
   new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool)
 
+class tag_button (box : Gtk.box Gtk.obj) =
+object (self)
+
+  inherit GObj.widget box
+
+  val fg_color = GButton.color_button ()
+  val fg_unset = GButton.toggle_button ()
+  val bg_color = GButton.color_button ()
+  val bg_unset = GButton.toggle_button ()
+  val bold = GButton.toggle_button ()
+  val italic = GButton.toggle_button ()
+  val underline = GButton.toggle_button ()
+
+  method set_tag tag =
+    let track c but set = match c with
+    | None -> set#set_active true
+    | Some c ->
+      set#set_active false;
+      but#set_color (Tags.color_of_string c)
+    in
+    track tag.tag_bg_color bg_color bg_unset;
+    track tag.tag_fg_color fg_color fg_unset;
+    bold#set_active tag.tag_bold;
+    italic#set_active tag.tag_italic;
+    underline#set_active tag.tag_underline;
+
+  method tag =
+    let get but set =
+      if set#active then None
+      else Some (Tags.string_of_color but#color)
+    in
+    {
+      tag_bg_color = get bg_color bg_unset;
+      tag_fg_color = get fg_color fg_unset;
+      tag_bold = bold#active;
+      tag_italic = italic#active;
+      tag_underline = underline#active;
+    }
+
+  initializer
+    let box = new GPack.box box in
+    let set_stock button stock =
+      let stock = GMisc.image ~stock ~icon_size:`BUTTON () in
+      button#set_image stock#coerce
+    in
+    set_stock fg_unset `CANCEL;
+    set_stock bg_unset `CANCEL;
+    set_stock bold `BOLD;
+    set_stock italic `ITALIC;
+    set_stock underline `UNDERLINE;
+    box#pack fg_color#coerce;
+    box#pack fg_unset#coerce;
+    box#pack bg_color#coerce;
+    box#pack bg_unset#coerce;
+    box#pack bold#coerce;
+    box#pack italic#coerce;
+    box#pack underline#coerce;
+    let cb but obj = obj#set_sensitive (not but#active) in
+    let _ = fg_unset#connect#toggled (fun () -> cb fg_unset fg_color#misc) in
+    let _ = bg_unset#connect#toggled (fun () -> cb bg_unset bg_color#misc) in
+    ()
+
+end
+
+let tag_button () =
+  let box = GPack.hbox () in
+  new tag_button (Gobject.unsafe_cast box#as_widget)
+
 (** Old style preferences *)
 
 let save_pref () =
@@ -487,6 +686,40 @@ let configure ?(apply=(fun () -> ())) () =
     custom ~label box callback true
   in
 
+  let config_tags =
+    let box = GPack.vbox () in
+    let scroll = GBin.scrolled_window
+      ~hpolicy:`NEVER
+      ~vpolicy:`AUTOMATIC
+      ~packing:(box#pack ~expand:true)
+      ()
+    in
+    let table = GPack.table
+      ~row_spacings:5
+      ~col_spacings:5
+      ~border_width:2
+      ~packing:scroll#add_with_viewport ()
+    in
+    let i = ref 0 in
+    let cb = ref [] in
+    let iter text tag =
+      let label = GMisc.label
+        ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:!i) ()
+      in
+      let () = label#set_xalign 0. in
+      let button = tag_button () in
+      let callback () = tag#set button#tag in
+      button#set_tag tag#get;
+      table#attach ~left:1 ~top:!i button#coerce;
+      incr i;
+      cb := callback :: !cb;
+    in
+    let () = Util.String.Map.iter iter !tags in
+    let label = "Tag configuration" in
+    let callback () = List.iter (fun f -> f ()) !cb in
+    custom ~label box callback true
+  in
+
   let config_editor =
     let label = "Editor configuration" in
     let box = GPack.vbox () in
@@ -690,6 +923,8 @@ let configure ?(apply=(fun () -> ())) () =
 	     [config_font]);
      Section("Colors", Some `SELECT_COLOR,
              [config_color; source_language; source_style]);
+     Section("Tags", Some `SELECT_COLOR,
+             [config_tags]);
      Section("Editor", Some `EDIT, [config_editor]);
      Section("Files", Some `DIRECTORY,
 	     [global_auto_revert;global_auto_revert_delay;
diff --git a/ide/preferences.mli b/ide/preferences.mli
index d815c01ddf..1733091a58 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,6 +12,14 @@ val style_manager : GSourceView2.source_style_scheme_manager
 type project_behavior = Ignore_args | Append_args | Subst_args
 type inputenc = Elocale | Eutf8 | Emanual of string
 
+type tag = {
+  tag_fg_color : string option;
+  tag_bg_color : string option;
+  tag_bold : bool;
+  tag_italic : bool;
+  tag_underline : bool;
+}
+
 class type ['a] repr =
 object
   method into : string list -> 'a option
@@ -33,6 +41,8 @@ object
   method default : 'a
 end
 
+val list_tags : unit -> tag preference Util.String.Map.t
+
 val cmd_coqtop : string option preference
 val cmd_coqc : string preference
 val cmd_make : string preference
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index f7279f9cfe..081094e2b6 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -28,6 +28,7 @@ let rec parse_string = parser
 and parse_string2 = parser
   | [< ''"' >] -> ""
   | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
+  | [< >] -> raise Parsing_error
 and parse_skip_comment = parser
   | [< ''\n'; s >] -> s
   | [< 'c; s >] -> parse_skip_comment s
@@ -47,7 +48,7 @@ let parse f =
     res
 
 let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function
-  | [] -> opts,List.rev l
+  | [] -> opts, l
   | ("-h"|"--help") :: _ ->
     raise Parsing_error
   | ("-no-opt"|"-byte") :: r ->
@@ -85,7 +86,6 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
     process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r
   | "-I" :: d :: r ->
     process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r
-  | "-R" :: p :: "-as" :: lp :: r
   | "-R" :: p :: lp :: r ->
     process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r
   | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ ->
@@ -127,6 +127,10 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
 	  else if (Filename.check_suffix f ".mlpack") then MLPACK f
 	  else Subdir f) :: l) r
 
+let process_cmd_line orig_dir opts l args =
+  let (opts, l) = process_cmd_line orig_dir opts l args in
+  opts, List.rev l
+
 let rec post_canonize f =
   if Filename.basename f = Filename.current_dir_name
   then let dir = Filename.dirname f in
@@ -134,48 +138,44 @@ let rec post_canonize f =
   else f
 
 (* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *)
-let split_arguments =
-  let rec aux = function
-  | V n :: r ->
-	let (v,m,o,s),i,d = aux r in ((CUnix.remove_path_dot n::v,m,o,s),i,d)
-  | ML n :: r ->
-      let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in
-      ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d)
-  | MLI n :: r ->
-      let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in
-      ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d)
-  | ML4 n :: r ->
-      let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in
-      ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d)
-  | MLLIB n :: r ->
-      let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in
-      ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d)
-  | MLPACK n :: r ->
-      let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in
-      ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d)
-  | Special (n,dep,is_phony,c) :: r ->
-      let (v,m,o,s),i,d = aux r in ((v,m,(n,dep,is_phony,c)::o,s),i,d)
-  | Subdir n :: r ->
-      let (v,m,o,s),i,d = aux r in ((v,m,o,n::s),i,d)
-  | MLInclude p :: r ->
-      let t,(ml,q,r),d = aux r in (t,((CUnix.remove_path_dot (post_canonize p),
-                                   CUnix.canonical_path_name p)::ml,q,r),d)
-  | Include (p,l) :: r ->
-      let t,(ml,i,r),d = aux r in
-      let i_new = (CUnix.remove_path_dot (post_canonize p),l,
-		   CUnix.canonical_path_name p) in
-      (t,(ml,i_new::i,r),d)
-  | RInclude (p,l) :: r ->
-      let t,(ml,i,r),d = aux r in
-      let r_new = (CUnix.remove_path_dot (post_canonize p),l,
-		   CUnix.canonical_path_name p) in
-      (t,(ml,i,r_new::r),d)
-  | Def (v,def) :: r ->
-      let t,i,(args,defs) = aux r in (t,i,(args,(v,def)::defs))
-  | Arg a :: r ->
-      let t,i,(args,defs) = aux r in (t,i,(a::args,defs))
-  | [] -> ([],([],[],[],[],[]),[],[]),([],[],[]),([],[])
-  in aux
+let split_arguments args =
+  List.fold_right
+    (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t),
+            (ml_inc,q_inc,r_inc as i),(args,defs as d)) ->
+     match a with
+     | V n ->
+        ((CUnix.remove_path_dot n::v,m,o,s),i,d)
+     | ML n ->
+        ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d)
+     | MLI n ->
+        ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d)
+     | ML4 n ->
+        ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d)
+     | MLLIB n ->
+        ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d)
+     | MLPACK n ->
+        ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d)
+     | Special (n,dep,is_phony,c) ->
+        ((v,m,(n,dep,is_phony,c)::o,s),i,d)
+     | Subdir n ->
+        ((v,m,o,n::s),i,d)
+     | MLInclude p ->
+        let ml_new = (CUnix.remove_path_dot (post_canonize p),
+                      CUnix.canonical_path_name p) in
+        (t,(ml_new::ml_inc,q_inc,r_inc),d)
+     | Include (p,l) ->
+        let q_new = (CUnix.remove_path_dot (post_canonize p),l,
+		     CUnix.canonical_path_name p) in
+        (t,(ml_inc,q_new::q_inc,r_inc),d)
+     | RInclude (p,l) ->
+        let r_new = (CUnix.remove_path_dot (post_canonize p),l,
+		     CUnix.canonical_path_name p) in
+        (t,(ml_inc,q_inc,r_new::r_inc),d)
+     | Def (v,def) ->
+        (t,i,(args,(v,def)::defs))
+     | Arg a ->
+        (t,i,(a::args,defs)))
+    args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[]))
 
 let read_project_file f =
   split_arguments
diff --git a/ide/sentence.ml b/ide/sentence.ml
index dd6b10a461..6897779e80 100644
--- a/ide/sentence.ml
+++ b/ide/sentence.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -63,13 +63,13 @@ let grab_sentence_start (iter:GText.iter) soi =
 
 (** Search forward the first character immediately after a sentence end *)
 
-let rec grab_sentence_stop (start:GText.iter) =
+let grab_sentence_stop (start:GText.iter) =
   (forward_search is_sentence_end start)#forward_char
 
 (** Search forward the first character immediately after a "." sentence end
     (and not just a "\{" or "\}" or comment end *)
 
-let rec grab_ending_dot (start:GText.iter) =
+let grab_ending_dot (start:GText.iter) =
   let is_ending_dot s = is_sentence_end s && s#char = Char.code '.' in
   (forward_search is_ending_dot start)#forward_char
 
diff --git a/ide/sentence.mli b/ide/sentence.mli
index f0ba5d22c3..feb3c0ac03 100644
--- a/ide/sentence.mli
+++ b/ide/sentence.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/session.ml b/ide/session.ml
index e4cc177428..cdec392ecc 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -16,6 +16,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method data : 'a
   end
 
 class type control =
@@ -316,6 +317,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
           errs
       end
     method on_update ~callback:cb = callback := cb
+    method data = !last_update
   end
 
 let create_jobpage coqtop coqops : jobpage =
@@ -355,6 +357,7 @@ let create_jobpage coqtop coqops : jobpage =
           jobs
       end
     method on_update ~callback:cb = callback := cb
+    method data = !last_update
   end
 
 let create_proof () =
diff --git a/ide/session.mli b/ide/session.mli
index 3a6b458582..028a1f9de6 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -14,6 +14,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method data : 'a
   end
 
 class type control =
diff --git a/ide/tags.ml b/ide/tags.ml
index 09b562530b..9ccff9fb51 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/tags.mli b/ide/tags.mli
index 6418d1b2e5..5a932f3300 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll
index 621833ddea..5cc8cbc0d2 100644
--- a/ide/utf8_convert.mll
+++ b/ide/utf8_convert.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,7 +12,7 @@
 
 }
 
-(* Replace all occurences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *)
+(* Replace all occurrences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *)
 
 let digit = ['0'-'9''A'-'Z''a'-'z']
 let short = digit digit digit digit
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 163bd28b13..946aaf010d 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -100,11 +100,14 @@ object(self)
         if Str.string_match (Str.regexp "\\. *$") com 0 then com
         else com ^ " " ^ arg ^" . "
       in
-      let log level message = result#buffer#insert (message^"\n") in
+      let log level message =
+        Ideutils.insert_xml result#buffer message;
+        result#buffer#insert "\n";
+      in
       let process =
 	Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
-            result#buffer#insert str;
+            Ideutils.insert_xml result#buffer str;
             notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
 	    Coq.return ()
           | Interface.Good res ->
diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli
index 1f0e31988a..fa50ba5fdd 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index 7d77679ce5..6c53fc0133 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli
index c3cb230d79..dd496aa5f5 100644
--- a/ide/wg_Completion.mli
+++ b/ide/wg_Completion.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml
index 53c634d7e2..3d1b63dfae 100644
--- a/ide/wg_Detachable.ml
+++ b/ide/wg_Detachable.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/wg_Detachable.mli b/ide/wg_Detachable.mli
index 71f85ad828..a7e8f46763 100644
--- a/ide/wg_Detachable.mli
+++ b/ide/wg_Detachable.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index a0949ca0c8..3d847ddcc1 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type mode = [ `FIND | `REPLACE ]
-
 let b2c = Ideutils.byte_offset_to_char_offset
 
 class finder name (view : GText.view) =
diff --git a/ide/wg_Find.mli b/ide/wg_Find.mli
index 7811fc43ef..1ef1c4d499 100644
--- a/ide/wg_Find.mli
+++ b/ide/wg_Find.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 30bb48e3f3..7728ad2360 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,7 +12,7 @@ class type message_view_signals =
 object
   inherit GObj.misc_signals
   inherit GUtil.add_ml_signals
-  method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id
+  method pushed : callback:Ideutils.logger -> GtkSignal.id
 end
 
 class message_view_signals_impl obj (pushed : 'a GUtil.signal) : message_view_signals =
@@ -28,9 +28,10 @@ class type message_view =
     inherit GObj.widget
     method connect : message_view_signals
     method clear : unit
-    method add : string -> unit
-    method set : string -> unit
-    method push : Pp.message_level -> string -> unit
+    method add : Richpp.richpp -> unit
+    method add_string : string -> unit
+    method set : Richpp.richpp -> unit
+    method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
       (** for more advanced text edition *)
@@ -76,14 +77,21 @@ let message_view () : message_view =
       | Pp.Warning -> [Tags.Message.warning]
       | _ -> []
       in
-      if msg <> "" then begin
-        buffer#insert ~tags msg;
-        buffer#insert ~tags "\n";
+      let rec non_empty = function
+      | Xml_datatype.PCData "" -> false
+      | Xml_datatype.PCData _ -> true
+      | Xml_datatype.Element (_, _, children) -> List.exists non_empty children
+      in
+      if non_empty (Richpp.repr msg) then begin
+        Ideutils.insert_xml buffer ~tags msg;
+        buffer#insert (*~tags*) "\n";
         push#call (level, msg)
       end
 
     method add msg = self#push Pp.Notice msg
 
+    method add_string s = self#add (Richpp.richpp_of_string s)
+
     method set msg = self#clear; self#add msg
 
     method buffer = text_buffer
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 457ece0900..2d34533dee 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,7 @@ class type message_view_signals =
 object
   inherit GObj.misc_signals
   inherit GUtil.add_ml_signals
-  method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id
+  method pushed : callback:Ideutils.logger -> GtkSignal.id
 end
 
 class type message_view =
@@ -18,9 +18,10 @@ class type message_view =
     inherit GObj.widget
     method connect : message_view_signals
     method clear : unit
-    method add : string -> unit
-    method set : string -> unit
-    method push : Pp.message_level -> string -> unit
+    method add : Richpp.richpp -> unit
+    method add_string : string -> unit
+    method set : Richpp.richpp -> unit
+    method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
       (** for more advanced text edition *)
diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml
index 0611c3f396..08d7d19833 100644
--- a/ide/wg_Notebook.ml
+++ b/ide/wg_Notebook.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/wg_Notebook.mli b/ide/wg_Notebook.mli
index 15a2ba41e9..34eb1d11e3 100644
--- a/ide/wg_Notebook.mli
+++ b/ide/wg_Notebook.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 6402789ec3..4d95fdd0df 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,6 +8,7 @@
 
 open Util
 open Preferences
+open Ideutils
 
 class type proof_view =
   object
@@ -83,7 +84,8 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           let () = hook_tag_cb tag hint sel_cb on_hover in
           [tag], hints
         in
-        let () = proof#buffer#insert ~tags (hyp ^ "\n") in
+        let () = insert_xml ~tags proof#buffer hyp in
+        proof#buffer#insert "\n";
         insert_hyp rem_hints hs
       in
       let () = proof#buffer#insert head_str in
@@ -96,13 +98,14 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           else []
         in
         proof#buffer#insert (goal_str 1 goals_cnt);
-        proof#buffer#insert ~tags cur_goal;
+        insert_xml proof#buffer cur_goal;
         proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
       let fold_goal i _ { Interface.goal_ccl = g } =
         proof#buffer#insert (goal_str i goals_cnt);
-        proof#buffer#insert (g ^ "\n")
+        insert_xml proof#buffer g;
+        proof#buffer#insert "\n"
       in
       let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
 
@@ -111,17 +114,6 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
                          (Some Tags.Proof.goal)));
       ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT)
 
-let mode_cesar (proof : #GText.view_skel) = function
-  | [] -> assert false
-  | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ ->
-      proof#buffer#insert "    *** Declarative Mode ***\n";
-      List.iter
-        (fun hyp -> proof#buffer#insert (hyp^"\n"))
-        hyps;
-      proof#buffer#insert "______________________________________\n";
-      proof#buffer#insert ("thesis := \n "^cur_goal^"\n");
-      ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
-
 let rec flatten = function
 | [] -> []
 | (lg, rg) :: l ->
@@ -152,8 +144,8 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* The proof is finished, with the exception of given up goals. *)
       view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
       let iter goal =
-        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-        view#buffer#insert msg
+        insert_xml view#buffer goal.Interface.goal_ccl;
+        view#buffer#insert "\n"
       in
       List.iter iter given_up_goals;
       view#buffer#insert "\nYou need to go back and solve them."
@@ -161,8 +153,8 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* All the goals have been resolved but those on the shelf. *)
       view#buffer#insert "All the remaining goals are on the shelf:\n\n";
       let iter goal =
-        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-        view#buffer#insert msg
+        insert_xml view#buffer goal.Interface.goal_ccl;
+        view#buffer#insert "\n"
       in
       List.iter iter shelved_goals
     | _, _, _, _ ->
@@ -174,8 +166,8 @@ let display mode (view : #GText.view_skel) goals hints evars =
       view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
       let iter i goal =
         let () = view#buffer#insert (goal_str (succ i)) in
-        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-        view#buffer#insert msg
+        insert_xml view#buffer goal.Interface.goal_ccl;
+        view#buffer#insert "\n"
       in
       List.iteri iter bg
     end
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index c5e042ea52..b6eae48b39 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 14cbf92eb7..83fbda4874 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -141,7 +141,7 @@ object(self)
 
   (** We don't care about atomicity. Return:
     1. `OK when there was no error, `FAIL otherwise
-    2. `NOOP if no write occured, `WRITE otherwise
+    2. `NOOP if no write occurred, `WRITE otherwise
   *)
   method private process_action = function
   | Insert ins ->
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index 6e54c4452f..6cce5e5b43 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 2ee2884547..c2799e40b1 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -11,53 +11,13 @@ open Preferences
 
 type color = GDraw.color
 
-module Segment :
-sig
-  type +'a t
-  val length : 'a t -> int
-  val resize : 'a t -> int -> 'a t
-  val empty : 'a t
-  val add : int -> 'a -> 'a t -> 'a t
-  val remove : int -> 'a t -> 'a t
-  val fold : ('a -> 'a -> bool) -> (int -> int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-end =
-struct
-  type 'a t = {
-    length : int;
-    content : 'a Int.Map.t;
-  }
-
-  let empty = { length = 0; content = Int.Map.empty }
-
-  let length s = s.length
-
-  let resize s len =
-    if s.length <= len then { s with length = len }
-    else
-      let filter i v = i < len in
-      { length = len; content = Int.Map.filter filter s.content }
-
-  let add i v s =
-    if i < s.length then
-      { s with content = Int.Map.add i v s.content }
-    else s
-
-  let remove i s = { s with content = Int.Map.remove i s.content }
-
-  let fold eq f s accu =
-    let make k v (cur, accu) = match cur with
-    | None -> Some (k, k, v), accu
-    | Some (i, j, w) ->
-      if k = j + 1 && eq v w then Some (i, k, w), accu
-      else Some (k, k, v), (i, j, w) :: accu
-    in
-    let p, segments = Int.Map.fold make s.content (None, []) in
-    let segments = match p with
-    | None -> segments
-    | Some p -> p :: segments
-    in
-    List.fold_left (fun accu (i, j, v) -> f i j v accu) accu segments
+type model_event = [ `INSERT | `REMOVE | `SET of int * color ]
 
+class type model =
+object
+  method changed : callback:(model_event -> unit) -> unit
+  method length : int
+  method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a
 end
 
 let i2f = float_of_int
@@ -96,7 +56,7 @@ object (self)
 
   val mutable width = 1
   val mutable height = 20
-  val mutable data = Segment.empty
+  val mutable model : model option = None
   val mutable default : color = `WHITE
   val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
   val clicked = new GUtil.signal ()
@@ -114,10 +74,12 @@ object (self)
       end
     in
     let _ = box#misc#connect#size_allocate cb in
-    let clicked_cb ev =
+    let clicked_cb ev = match model with
+    | None -> true
+    | Some md ->
       let x = GdkEvent.Button.x ev in
       let (width, _) = pixmap#size in
-      let len = Segment.length data in
+      let len = md#length in
       let idx = f2i ((x *. i2f len) /. i2f width) in
       let () = clicked#call idx in
       true
@@ -128,17 +90,23 @@ object (self)
     (** Initial pixmap *)
     draw#set_pixmap pixmap
 
-  method length = Segment.length data
-
-  method set_length len =
-    data <- Segment.resize data len;
-    if self#misc#visible then self#refresh ()
+  method set_model md =
+    model <- Some md;
+    let changed_cb = function
+    | `INSERT | `REMOVE ->
+      if self#misc#visible then self#refresh ()
+    | `SET (i, color) ->
+      if self#misc#visible then self#fill_range color i (i + 1)
+    in
+    md#changed changed_cb
 
-  method private fill_range color i j =
+  method private fill_range color i j = match model with
+  | None -> ()
+  | Some md ->
     let i = i2f i in
     let j = i2f j in
     let width = i2f width in
-    let len = i2f (Segment.length data) in
+    let len = i2f md#length in
     let x = f2i ((i *. width) /. len) in
     let x' = f2i ((j *. width) /. len) in
     let w = x' - x in
@@ -146,14 +114,6 @@ object (self)
     pixmap#rectangle ~x ~y:0 ~width:w ~height ~filled:true ();
     draw#set_mask None;
 
-  method add i color =
-    data <- Segment.add i color data;
-    if self#misc#visible then self#fill_range color i (i + 1)
-
-  method remove i =
-    data <- Segment.remove i data;
-    if self#misc#visible then self#fill_range default i (i + 1)
-
   method set_default_color color = default <- color
   method default_color = default
 
@@ -162,11 +122,23 @@ object (self)
     draw#set_pixmap pixmap;
     self#refresh ();
 
-  method private refresh () =
+  method private refresh () = match model with
+  | None -> ()
+  | Some md ->
     pixmap#set_foreground default;
     pixmap#rectangle ~x:0 ~y:0 ~width ~height ~filled:true ();
-    let fold i j v () = self#fill_range v i (j + 1) in
-    Segment.fold color_eq fold data ();
+    let make (k, cur, accu) v = match cur with
+    | None -> pred k, Some (k, k, v), accu
+    | Some (i, j, w) ->
+      if k = j - 1 && color_eq v w then pred k, Some (k, i, w), accu
+      else pred k, Some (k, k, v), (i, j, w) :: accu
+    in
+    let _, p, segments = md#fold make (md#length - 1, None, []) in
+    let segments = match p with
+    | None -> segments
+    | Some p -> p :: segments
+    in
+    List.iter (fun (i, j, v) -> self#fill_range v i (j + 1)) segments;
     draw#set_mask None;
 
   method connect =
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli
index 0263856ae1..29cbbedacf 100644
--- a/ide/wg_Segment.mli
+++ b/ide/wg_Segment.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,6 +8,8 @@
 
 type color = GDraw.color
 
+type model_event = [ `INSERT | `REMOVE | `SET of int * color ]
+
 class type segment_signals =
 object
   inherit GObj.misc_signals
@@ -15,15 +17,19 @@ object
   method clicked : callback:(int -> unit) -> GtkSignal.id
 end
 
+class type model =
+object
+  method changed : callback:(model_event -> unit) -> unit
+  method length : int
+  method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a
+end
+
 class segment : unit ->
   object
     inherit GObj.widget
     val obj : Gtk.widget Gtk.obj
+    method set_model : model -> unit
     method connect : segment_signals
-    method length : int
-    method set_length : int -> unit
     method default_color : color
     method set_default_color : color -> unit
-    method add : int -> color -> unit
-    method remove : int -> unit
   end
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index d337a911d8..232630e5b2 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20140312"
+let protocol_version = "20150913"
 
 (** * Interface of calls to Coq by CoqIde *)
 
@@ -62,10 +62,12 @@ let of_option_value = function
   | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i]
   | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b]
   | StringValue s -> constructor "option_value" "stringvalue" [of_string s]
+  | StringOptValue s -> constructor "option_value" "stringoptvalue" [of_option of_string s]
 let to_option_value = do_match "option_value" (fun s args -> match s with
   | "intvalue" -> IntValue (to_option to_int (singleton args))
   | "boolvalue" -> BoolValue (to_bool (singleton args))
   | "stringvalue" -> StringValue (to_string (singleton args))
+  | "stringoptvalue" -> StringOptValue (to_option to_string (singleton args))
   | _ -> raise Marshal_error)
 
 let of_option_state s =
@@ -90,7 +92,7 @@ let of_value f = function
   | None -> []
   | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in
   let id = Stateid.to_xml id in
-  Element ("value", ["val", "fail"] @ loc, [id;PCData msg])
+  Element ("value", ["val", "fail"] @ loc, [id; Richpp.of_richpp msg])
 let to_value f = function
 | Element ("value", attrs, l) ->
   let ans = massoc "val" attrs in
@@ -103,8 +105,9 @@ let to_value f = function
         Some (loc_s, loc_e)
       with Marshal_error | Failure _ -> None
     in
-    let id = Stateid.of_xml (List.hd l) in
-    let msg = raw_string (List.tl l) in
+    let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise Marshal_error in
+    let id = Stateid.of_xml id in
+    let msg = Richpp.to_richpp msg in
     Fail (id, loc, msg)
   else raise Marshal_error
 | _ -> raise Marshal_error
@@ -131,14 +134,14 @@ let to_evar = function
   | _ -> raise Marshal_error
 
 let of_goal g =
-  let hyp = of_list of_string g.goal_hyp in
-  let ccl = of_string g.goal_ccl in
+  let hyp = of_list Richpp.of_richpp g.goal_hyp in
+  let ccl = Richpp.of_richpp g.goal_ccl in
   let id = of_string g.goal_id in
   Element ("goal", [], [id; hyp; ccl])
 let to_goal = function
   | Element ("goal", [], [id; hyp; ccl]) ->
-    let hyp = to_list to_string hyp in
-    let ccl = to_string ccl in
+    let hyp = to_list Richpp.to_richpp hyp in
+    let ccl = Richpp.to_richpp ccl in
     let id = to_string id in
     { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
   | _ -> raise Marshal_error
@@ -218,22 +221,31 @@ module ReifType : sig
 
 end = struct
 
-  type value_type =
-    | Unit | String | Int | Bool | Xml
+  type _ val_t =
+    | Unit : unit val_t
+    | String : string val_t
+    | Int : int val_t
+    | Bool : bool val_t
+    | Xml : Xml_datatype.xml val_t
 
-    | Option of value_type
-    | List of value_type
-    | Pair of value_type * value_type
-    | Union of value_type * value_type
+    | Option : 'a val_t -> 'a option val_t
+    | List : 'a val_t -> 'a list val_t
+    | Pair : 'a val_t * 'b val_t -> ('a * 'b) val_t
+    | Union : 'a val_t * 'b val_t -> ('a, 'b) union val_t
 
-    | Goals | Evar | State | Option_state | Option_value | Coq_info
-    | Coq_object of value_type
-    | State_id
-    | Search_cst
+    | Goals : goals val_t
+    | Evar : evar val_t
+    | State : status val_t
+    | Option_state : option_state val_t
+    | Option_value : option_value val_t
+    | Coq_info : coq_info val_t
+    | Coq_object : 'a val_t -> 'a coq_object val_t
+    | State_id : state_id val_t
+    | Search_cst : search_constraint val_t
 
-  type 'a val_t = value_type
+  type value_type = Value_type : 'a val_t -> value_type
 
-  let erase (x : 'a val_t) : value_type = x
+  let erase (x : 'a val_t) = Value_type x
 
   let unit_t         = Unit
   let string_t       = String
@@ -257,48 +269,48 @@ end = struct
   let search_cst_t   = Search_cst
 
   let of_value_type (ty : 'a val_t) : 'a -> xml =
-    let rec convert ty : 'a -> xml = match ty with
-      | Unit          -> Obj.magic of_unit
-      | Bool          -> Obj.magic of_bool
-      | Xml           -> Obj.magic (fun x -> x)
-      | String        -> Obj.magic of_string
-      | Int           -> Obj.magic of_int
-      | State         -> Obj.magic of_status
-      | Option_state  -> Obj.magic of_option_state
-      | Option_value  -> Obj.magic of_option_value
-      | Coq_info      -> Obj.magic of_coq_info
-      | Goals         -> Obj.magic of_goals
-      | Evar          -> Obj.magic of_evar
-      | List t        -> Obj.magic (of_list (convert t))
-      | Option t      -> Obj.magic (of_option (convert t))
-      | Coq_object t  -> Obj.magic (of_coq_object (convert t))
-      | Pair (t1,t2)  -> Obj.magic (of_pair (convert t1) (convert t2))
-      | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2))
-      | State_id      -> Obj.magic Stateid.to_xml
-      | Search_cst    -> Obj.magic of_search_cst
+    let rec convert : type a. a val_t -> a -> xml = function
+      | Unit          -> of_unit
+      | Bool          -> of_bool
+      | Xml           -> (fun x -> x)
+      | String        -> of_string
+      | Int           -> of_int
+      | State         -> of_status
+      | Option_state  -> of_option_state
+      | Option_value  -> of_option_value
+      | Coq_info      -> of_coq_info
+      | Goals         -> of_goals
+      | Evar          -> of_evar
+      | List t        -> (of_list (convert t))
+      | Option t      -> (of_option (convert t))
+      | Coq_object t  -> (of_coq_object (convert t))
+      | Pair (t1,t2)  -> (of_pair (convert t1) (convert t2))
+      | Union (t1,t2) -> (of_union (convert t1) (convert t2))
+      | State_id      -> Stateid.to_xml
+      | Search_cst    -> of_search_cst
     in
       convert ty
 
   let to_value_type (ty : 'a val_t) : xml -> 'a =
-    let rec convert ty : xml -> 'a = match ty with
-      | Unit          -> Obj.magic to_unit
-      | Bool          -> Obj.magic to_bool
-      | Xml           -> Obj.magic (fun x -> x)
-      | String        -> Obj.magic to_string
-      | Int           -> Obj.magic to_int
-      | State         -> Obj.magic to_status
-      | Option_state  -> Obj.magic to_option_state
-      | Option_value  -> Obj.magic to_option_value
-      | Coq_info      -> Obj.magic to_coq_info
-      | Goals         -> Obj.magic to_goals
-      | Evar          -> Obj.magic to_evar
-      | List t        -> Obj.magic (to_list (convert t))
-      | Option t      -> Obj.magic (to_option (convert t))
-      | Coq_object t  -> Obj.magic (to_coq_object (convert t))
-      | Pair (t1,t2)  -> Obj.magic (to_pair (convert t1) (convert t2))
-      | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2))
-      | State_id      -> Obj.magic Stateid.of_xml
-      | Search_cst    -> Obj.magic to_search_cst
+    let rec convert : type a. a val_t -> xml -> a = function
+      | Unit          -> to_unit
+      | Bool          -> to_bool
+      | Xml           -> (fun x -> x)
+      | String        -> to_string
+      | Int           -> to_int
+      | State         -> to_status
+      | Option_state  -> to_option_state
+      | Option_value  -> to_option_value
+      | Coq_info      -> to_coq_info
+      | Goals         -> to_goals
+      | Evar          -> to_evar
+      | List t        -> (to_list (convert t))
+      | Option t      -> (to_option (convert t))
+      | Coq_object t  -> (to_coq_object (convert t))
+      | Pair (t1,t2)  -> (to_pair (convert t1) (convert t2))
+      | Union (t1,t2) -> (to_union (convert t1) (convert t2))
+      | State_id      -> Stateid.of_xml
+      | Search_cst    -> to_search_cst
     in
       convert ty
 
@@ -318,10 +330,9 @@ end = struct
               (List.length lg + List.length rg) pr_focus l in
         Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
     else
-      let pr_menu s = s in
       let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
-        "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^
-            pr_menu goal ^ "]" in
+        "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^
+            Richpp.raw_print goal ^ "]" in
       String.concat " " (List.map pr_goal g.fg_goals)
   let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
   let pr_status (s : status) =
@@ -337,6 +348,8 @@ end = struct
     | IntValue None -> "none"
     | IntValue (Some i) -> string_of_int i
     | StringValue s -> s
+    | StringOptValue None -> "none"
+    | StringOptValue (Some s) -> s
     | BoolValue b -> if b then "true" else "false"
   let pr_option_state (s : option_state) =
     Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
@@ -346,6 +359,7 @@ end = struct
   let pr_coq_object (o : 'a coq_object) = "FIXME"
   let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")"
   let pr_union pr1 pr2 = function Inl x -> "Inl "^pr1 x | Inr x -> "Inr "^pr2 x
+  let pr_state_id = Stateid.to_string
 
   let pr_search_cst = function
     | Name_Pattern s -> "Name_Pattern " ^ s
@@ -354,30 +368,30 @@ end = struct
     | In_Module s -> "In_Module " ^ String.concat "." s
     | Include_Blacklist -> "Include_Blacklist"
 
-  let rec print = function
-  | Unit          -> Obj.magic pr_unit
-  | Bool          -> Obj.magic pr_bool
-  | String        -> Obj.magic pr_string
-  | Xml           -> Obj.magic Xml_printer.to_string_fmt
-  | Int           -> Obj.magic pr_int
-  | State         -> Obj.magic pr_status
-  | Option_state  -> Obj.magic pr_option_state
-  | Option_value  -> Obj.magic pr_option_value
-  | Search_cst    -> Obj.magic pr_search_cst
-  | Coq_info      -> Obj.magic pr_coq_info
-  | Goals         -> Obj.magic pr_goal
-  | Evar          -> Obj.magic pr_evar
-  | List t        -> Obj.magic (pr_list (print t))
-  | Option t      -> Obj.magic (pr_option (print t))
-  | Coq_object t  -> Obj.magic pr_coq_object
-  | Pair (t1,t2)  -> Obj.magic (pr_pair (print t1) (print t2))
-  | Union (t1,t2) -> Obj.magic (pr_union (print t1) (print t2))
-  | State_id      -> Obj.magic pr_int
+  let rec print : type a. a val_t -> a -> string = function
+  | Unit          -> pr_unit
+  | Bool          -> pr_bool
+  | String        -> pr_string
+  | Xml           -> Xml_printer.to_string_fmt
+  | Int           -> pr_int
+  | State         -> pr_status
+  | Option_state  -> pr_option_state
+  | Option_value  -> pr_option_value
+  | Search_cst    -> pr_search_cst
+  | Coq_info      -> pr_coq_info
+  | Goals         -> pr_goal
+  | Evar          -> pr_evar
+  | List t        -> (pr_list (print t))
+  | Option t      -> (pr_option (print t))
+  | Coq_object t  -> pr_coq_object
+  | Pair (t1,t2)  -> (pr_pair (print t1) (print t2))
+  | Union (t1,t2) -> (pr_union (print t1) (print t2))
+  | State_id      -> pr_state_id
 
   (* This is to break if a rename/refactoring makes the strings below outdated *)
   type 'a exists = bool
 
-  let rec print_type = function
+  let rec print_val_t : type a. a val_t -> string = function
   | Unit          -> "unit"
   | Bool          -> "bool"
   | String        -> "string"
@@ -390,33 +404,35 @@ end = struct
   | Coq_info      -> assert(true : coq_info exists); "Interface.coq_info"
   | Goals         -> assert(true : goals exists); "Interface.goals"
   | Evar          -> assert(true : evar exists); "Interface.evar"
-  | List t        -> Printf.sprintf "(%s list)" (print_type t)
-  | Option t      -> Printf.sprintf "(%s option)" (print_type t)
+  | List t        -> Printf.sprintf "(%s list)" (print_val_t t)
+  | Option t      -> Printf.sprintf "(%s option)" (print_val_t t)
   | Coq_object t  -> assert(true : 'a coq_object exists);
-                     Printf.sprintf "(%s Interface.coq_object)" (print_type t)
-  | Pair (t1,t2)  -> Printf.sprintf "(%s * %s)" (print_type t1) (print_type t2)
+                     Printf.sprintf "(%s Interface.coq_object)" (print_val_t t)
+  | Pair (t1,t2)  -> Printf.sprintf "(%s * %s)" (print_val_t t1) (print_val_t t2)
   | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists);
-                     Printf.sprintf "((%s, %s) CSig.union)" (print_type t1) (print_type t2)
+                     Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2)
   | State_id      -> assert(true : Stateid.t exists); "Stateid.t"
 
+  let print_type = function Value_type ty -> print_val_t ty
+
   let document_type_encoding pr_xml =
     Printf.printf "\n=== Data encoding by examples ===\n\n";
-    Printf.printf "%s:\n\n%s\n\n" (print_type Unit) (pr_xml (of_unit ()));
-    Printf.printf "%s:\n\n%s\n%s\n\n" (print_type Bool)
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t Unit) (pr_xml (of_unit ()));
+    Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t Bool)
       (pr_xml (of_bool true)) (pr_xml (of_bool false));
-    Printf.printf "%s:\n\n%s\n\n" (print_type String) (pr_xml (of_string "hello"));
-    Printf.printf "%s:\n\n%s\n\n" (print_type Int) (pr_xml (of_int 256));
-    Printf.printf "%s:\n\n%s\n\n" (print_type State_id) (pr_xml (Stateid.to_xml Stateid.initial));
-    Printf.printf "%s:\n\n%s\n\n" (print_type (List Int)) (pr_xml (of_list of_int [3;4;5]));
-    Printf.printf "%s:\n\n%s\n%s\n\n" (print_type (Option Int))
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t String) (pr_xml (of_string "hello"));
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t Int) (pr_xml (of_int 256));
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t State_id) (pr_xml (Stateid.to_xml Stateid.initial));
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t (List Int)) (pr_xml (of_list of_int [3;4;5]));
+    Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t (Option Int))
       (pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None));
-    Printf.printf "%s:\n\n%s\n\n" (print_type (Pair (Bool,Int)))
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t (Pair (Bool,Int)))
       (pr_xml (of_pair of_bool of_int (false,3)));
-    Printf.printf "%s:\n\n%s\n\n" (print_type (Union (Bool,Int)))
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int)))
       (pr_xml (of_union of_bool of_int (Inl false)));
     print_endline ("All other types are records represented by a node named like the OCaml\n"^
                    "type which contains a flattened n-tuple.  We provide one example.\n");
-    Printf.printf "%s:\n\n%s\n\n" (print_type Option_state)
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state)
       (pr_xml (of_option_state { opt_sync = true; opt_depr = false;
         opt_name = "name1"; opt_value = IntValue (Some 37) }));
 
@@ -492,27 +508,27 @@ let calls = [|
 |]
 
 type 'a call =
-  | Add        of add_sty
-  | Edit_at    of edit_at_sty
-  | Query      of query_sty
-  | Goal       of goals_sty
-  | Evars      of evars_sty
-  | Hints      of hints_sty
-  | Status     of status_sty
-  | Search     of search_sty
-  | GetOptions of get_options_sty
-  | SetOptions of set_options_sty
-  | MkCases    of mkcases_sty
-  | Quit       of quit_sty
-  | About      of about_sty
-  | Init       of init_sty
-  | StopWorker of stop_worker_sty
+  | Add        : add_sty -> add_rty call
+  | Edit_at    : edit_at_sty -> edit_at_rty call
+  | Query      : query_sty -> query_rty call
+  | Goal       : goals_sty -> goals_rty call
+  | Evars      : evars_sty -> evars_rty call
+  | Hints      : hints_sty -> hints_rty call
+  | Status     : status_sty -> status_rty call
+  | Search     : search_sty -> search_rty call
+  | GetOptions : get_options_sty -> get_options_rty call
+  | SetOptions : set_options_sty -> set_options_rty call
+  | MkCases    : mkcases_sty -> mkcases_rty call
+  | Quit       : quit_sty -> quit_rty call
+  | About      : about_sty -> about_rty call
+  | Init       : init_sty -> init_rty call
+  | StopWorker : stop_worker_sty -> stop_worker_rty call
   (* retrocompatibility *)
-  | Interp     of interp_sty
-  | PrintAst   of print_ast_sty
-  | Annotate   of annotate_sty
+  | Interp     : interp_sty -> interp_rty call
+  | PrintAst   : print_ast_sty -> print_ast_rty call
+  | Annotate   : annotate_sty -> annotate_rty call
 
-let id_of_call = function
+let id_of_call : type a. a call -> int = function
   | Add _        -> 0
   | Edit_at _    -> 1
   | Query _      -> 2
@@ -534,7 +550,7 @@ let id_of_call = function
 
 let str_of_call c = pi1 calls.(id_of_call c)
 
-type unknown
+type unknown_call = Unknown : 'a call -> unknown_call
 
 (** We use phantom types and GADT to protect ourselves against wild casts *)
 let add x         : add_rty call         = Add x
@@ -555,8 +571,8 @@ let stop_worker x : stop_worker_rty call = StopWorker x
 let print_ast   x : print_ast_rty call   = PrintAst x
 let annotate   x : annotate_rty call    = Annotate x
 
-let abstract_eval_call handler (c : 'a call) : 'a value =
-  let mkGood x : 'a value = Good (Obj.magic x) in
+let abstract_eval_call : type a. _ -> a call -> a value = fun handler c ->
+  let mkGood : type a. a -> a value = fun x -> Good x in
   try
     match c with
     | Add x        -> mkGood (handler.add x)
@@ -582,47 +598,47 @@ let abstract_eval_call handler (c : 'a call) : 'a value =
     Fail (handler.handle_exn any)
 
 (** brain dead code, edit if protocol messages are added/removed *)
-let of_answer (q : 'a call) (v : 'a value) : xml = match q with
-  | Add _        -> of_value (of_value_type add_rty_t        ) (Obj.magic v)
-  | Edit_at _    -> of_value (of_value_type edit_at_rty_t    ) (Obj.magic v)
-  | Query _      -> of_value (of_value_type query_rty_t      ) (Obj.magic v)
-  | Goal _       -> of_value (of_value_type goals_rty_t      ) (Obj.magic v)
-  | Evars _      -> of_value (of_value_type evars_rty_t      ) (Obj.magic v)
-  | Hints _      -> of_value (of_value_type hints_rty_t      ) (Obj.magic v)
-  | Status _     -> of_value (of_value_type status_rty_t     ) (Obj.magic v)
-  | Search _     -> of_value (of_value_type search_rty_t     ) (Obj.magic v)
-  | GetOptions _ -> of_value (of_value_type get_options_rty_t) (Obj.magic v)
-  | SetOptions _ -> of_value (of_value_type set_options_rty_t) (Obj.magic v)
-  | MkCases _    -> of_value (of_value_type mkcases_rty_t    ) (Obj.magic v)
-  | Quit _       -> of_value (of_value_type quit_rty_t       ) (Obj.magic v)
-  | About _      -> of_value (of_value_type about_rty_t      ) (Obj.magic v)
-  | Init _       -> of_value (of_value_type init_rty_t       ) (Obj.magic v)
-  | Interp _     -> of_value (of_value_type interp_rty_t     ) (Obj.magic v)
-  | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) (Obj.magic v)
-  | PrintAst _   -> of_value (of_value_type print_ast_rty_t  ) (Obj.magic v)
-  | Annotate _   -> of_value (of_value_type annotate_rty_t   ) (Obj.magic v)
-
-let to_answer (q : 'a call) (x : xml) : 'a value = match q with
-  | Add _        -> Obj.magic (to_value (to_value_type add_rty_t        ) x)
-  | Edit_at _    -> Obj.magic (to_value (to_value_type edit_at_rty_t    ) x)
-  | Query _      -> Obj.magic (to_value (to_value_type query_rty_t      ) x)
-  | Goal _       -> Obj.magic (to_value (to_value_type goals_rty_t      ) x)
-  | Evars _      -> Obj.magic (to_value (to_value_type evars_rty_t      ) x)
-  | Hints _      -> Obj.magic (to_value (to_value_type hints_rty_t      ) x)
-  | Status _     -> Obj.magic (to_value (to_value_type status_rty_t     ) x)
-  | Search _     -> Obj.magic (to_value (to_value_type search_rty_t     ) x)
-  | GetOptions _ -> Obj.magic (to_value (to_value_type get_options_rty_t) x)
-  | SetOptions _ -> Obj.magic (to_value (to_value_type set_options_rty_t) x)
-  | MkCases _    -> Obj.magic (to_value (to_value_type mkcases_rty_t    ) x)
-  | Quit _       -> Obj.magic (to_value (to_value_type quit_rty_t       ) x)
-  | About _      -> Obj.magic (to_value (to_value_type about_rty_t      ) x)
-  | Init _       -> Obj.magic (to_value (to_value_type init_rty_t       ) x)
-  | Interp _     -> Obj.magic (to_value (to_value_type interp_rty_t     ) x)
-  | StopWorker _ -> Obj.magic (to_value (to_value_type stop_worker_rty_t) x)
-  | PrintAst _   -> Obj.magic (to_value (to_value_type print_ast_rty_t  ) x)
-  | Annotate _   -> Obj.magic (to_value (to_value_type annotate_rty_t   ) x)
-
-let of_call (q : 'a call) : xml =
+let of_answer : type a. a call -> a value -> xml = function
+  | Add _        -> of_value (of_value_type add_rty_t        )
+  | Edit_at _    -> of_value (of_value_type edit_at_rty_t    )
+  | Query _      -> of_value (of_value_type query_rty_t      )
+  | Goal _       -> of_value (of_value_type goals_rty_t      )
+  | Evars _      -> of_value (of_value_type evars_rty_t      )
+  | Hints _      -> of_value (of_value_type hints_rty_t      )
+  | Status _     -> of_value (of_value_type status_rty_t     )
+  | Search _     -> of_value (of_value_type search_rty_t     )
+  | GetOptions _ -> of_value (of_value_type get_options_rty_t)
+  | SetOptions _ -> of_value (of_value_type set_options_rty_t)
+  | MkCases _    -> of_value (of_value_type mkcases_rty_t    )
+  | Quit _       -> of_value (of_value_type quit_rty_t       )
+  | About _      -> of_value (of_value_type about_rty_t      )
+  | Init _       -> of_value (of_value_type init_rty_t       )
+  | Interp _     -> of_value (of_value_type interp_rty_t     )
+  | StopWorker _ -> of_value (of_value_type stop_worker_rty_t)
+  | PrintAst _   -> of_value (of_value_type print_ast_rty_t  )
+  | Annotate _   -> of_value (of_value_type annotate_rty_t   )
+
+let to_answer : type a. a call -> xml -> a value = function
+  | Add _        -> to_value (to_value_type add_rty_t        )
+  | Edit_at _    -> to_value (to_value_type edit_at_rty_t    )
+  | Query _      -> to_value (to_value_type query_rty_t      )
+  | Goal _       -> to_value (to_value_type goals_rty_t      )
+  | Evars _      -> to_value (to_value_type evars_rty_t      )
+  | Hints _      -> to_value (to_value_type hints_rty_t      )
+  | Status _     -> to_value (to_value_type status_rty_t     )
+  | Search _     -> to_value (to_value_type search_rty_t     )
+  | GetOptions _ -> to_value (to_value_type get_options_rty_t)
+  | SetOptions _ -> to_value (to_value_type set_options_rty_t)
+  | MkCases _    -> to_value (to_value_type mkcases_rty_t    )
+  | Quit _       -> to_value (to_value_type quit_rty_t       )
+  | About _      -> to_value (to_value_type about_rty_t      )
+  | Init _       -> to_value (to_value_type init_rty_t       )
+  | Interp _     -> to_value (to_value_type interp_rty_t     )
+  | StopWorker _ -> to_value (to_value_type stop_worker_rty_t)
+  | PrintAst _   -> to_value (to_value_type print_ast_rty_t  )
+  | Annotate _   -> to_value (to_value_type annotate_rty_t   )
+
+let of_call : type a. a call -> xml = fun q ->
   let mkCall x = constructor "call" (str_of_call q) [x] in
   match q with
   | Add x        -> mkCall (of_value_type add_sty_t         x)
@@ -644,59 +660,59 @@ let of_call (q : 'a call) : xml =
   | PrintAst x   -> mkCall (of_value_type print_ast_sty_t   x)
   | Annotate x   -> mkCall (of_value_type annotate_sty_t    x)
 
-let to_call : xml -> unknown call =
+let to_call : xml -> unknown_call =
   do_match "call" (fun s a ->
     let mkCallArg vt a = to_value_type vt (singleton a) in
     match s with
-    | "Add"        -> Add        (mkCallArg add_sty_t         a)
-    | "Edit_at"    -> Edit_at    (mkCallArg edit_at_sty_t     a)
-    | "Query"      -> Query      (mkCallArg query_sty_t       a)
-    | "Goal"       -> Goal       (mkCallArg goals_sty_t       a)
-    | "Evars"      -> Evars      (mkCallArg evars_sty_t       a)
-    | "Hints"      -> Hints      (mkCallArg hints_sty_t       a)
-    | "Status"     -> Status     (mkCallArg status_sty_t      a)
-    | "Search"     -> Search     (mkCallArg search_sty_t      a)
-    | "GetOptions" -> GetOptions (mkCallArg get_options_sty_t a)
-    | "SetOptions" -> SetOptions (mkCallArg set_options_sty_t a)
-    | "MkCases"    -> MkCases    (mkCallArg mkcases_sty_t     a)
-    | "Quit"       -> Quit       (mkCallArg quit_sty_t        a)
-    | "About"      -> About      (mkCallArg about_sty_t       a)
-    | "Init"       -> Init       (mkCallArg init_sty_t        a)
-    | "Interp"     -> Interp     (mkCallArg interp_sty_t      a)
-    | "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a)
-    | "PrintAst"   -> PrintAst   (mkCallArg print_ast_sty_t   a)
-    | "Annotate"   -> Annotate   (mkCallArg annotate_sty_t    a)
+    | "Add"        -> Unknown (Add        (mkCallArg add_sty_t         a))
+    | "Edit_at"    -> Unknown (Edit_at    (mkCallArg edit_at_sty_t     a))
+    | "Query"      -> Unknown (Query      (mkCallArg query_sty_t       a))
+    | "Goal"       -> Unknown (Goal       (mkCallArg goals_sty_t       a))
+    | "Evars"      -> Unknown (Evars      (mkCallArg evars_sty_t       a))
+    | "Hints"      -> Unknown (Hints      (mkCallArg hints_sty_t       a))
+    | "Status"     -> Unknown (Status     (mkCallArg status_sty_t      a))
+    | "Search"     -> Unknown (Search     (mkCallArg search_sty_t      a))
+    | "GetOptions" -> Unknown (GetOptions (mkCallArg get_options_sty_t a))
+    | "SetOptions" -> Unknown (SetOptions (mkCallArg set_options_sty_t a))
+    | "MkCases"    -> Unknown (MkCases    (mkCallArg mkcases_sty_t     a))
+    | "Quit"       -> Unknown (Quit       (mkCallArg quit_sty_t        a))
+    | "About"      -> Unknown (About      (mkCallArg about_sty_t       a))
+    | "Init"       -> Unknown (Init       (mkCallArg init_sty_t        a))
+    | "Interp"     -> Unknown (Interp     (mkCallArg interp_sty_t      a))
+    | "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a))
+    | "PrintAst"   -> Unknown (PrintAst   (mkCallArg print_ast_sty_t   a))
+    | "Annotate"   -> Unknown (Annotate   (mkCallArg annotate_sty_t    a))
     | _ -> raise Marshal_error)
 
 (** Debug printing *)
 
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
-  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]"
+  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]"
   | Fail (id,Some(i,j),str) ->
       "FAIL "^Stateid.to_string id^
-        " ("^string_of_int i^","^string_of_int j^")["^str^"]"
+        " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]"
 let pr_value v = pr_value_gen (fun _ -> "FIXME") v
-let pr_full_value call value = match call with
-  | Add _        -> pr_value_gen (print add_rty_t        ) (Obj.magic value)
-  | Edit_at _    -> pr_value_gen (print edit_at_rty_t    ) (Obj.magic value)
-  | Query _      -> pr_value_gen (print query_rty_t      ) (Obj.magic value)
-  | Goal _       -> pr_value_gen (print goals_rty_t      ) (Obj.magic value)
-  | Evars _      -> pr_value_gen (print evars_rty_t      ) (Obj.magic value)
-  | Hints _      -> pr_value_gen (print hints_rty_t      ) (Obj.magic value)
-  | Status _     -> pr_value_gen (print status_rty_t     ) (Obj.magic value)
-  | Search _     -> pr_value_gen (print search_rty_t     ) (Obj.magic value)
-  | GetOptions _ -> pr_value_gen (print get_options_rty_t) (Obj.magic value)
-  | SetOptions _ -> pr_value_gen (print set_options_rty_t) (Obj.magic value)
-  | MkCases _    -> pr_value_gen (print mkcases_rty_t    ) (Obj.magic value)
-  | Quit _       -> pr_value_gen (print quit_rty_t       ) (Obj.magic value)
-  | About _      -> pr_value_gen (print about_rty_t      ) (Obj.magic value)
-  | Init _       -> pr_value_gen (print init_rty_t       ) (Obj.magic value)
-  | Interp _     -> pr_value_gen (print interp_rty_t     ) (Obj.magic value)
-  | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) (Obj.magic value)
-  | PrintAst _   -> pr_value_gen (print print_ast_rty_t  ) (Obj.magic value)
-  | Annotate _   -> pr_value_gen (print annotate_rty_t   ) (Obj.magic value)
-let pr_call call =
+let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with
+  | Add _        -> pr_value_gen (print add_rty_t        ) value
+  | Edit_at _    -> pr_value_gen (print edit_at_rty_t    ) value
+  | Query _      -> pr_value_gen (print query_rty_t      ) value
+  | Goal _       -> pr_value_gen (print goals_rty_t      ) value
+  | Evars _      -> pr_value_gen (print evars_rty_t      ) value
+  | Hints _      -> pr_value_gen (print hints_rty_t      ) value
+  | Status _     -> pr_value_gen (print status_rty_t     ) value
+  | Search _     -> pr_value_gen (print search_rty_t     ) value
+  | GetOptions _ -> pr_value_gen (print get_options_rty_t) value
+  | SetOptions _ -> pr_value_gen (print set_options_rty_t) value
+  | MkCases _    -> pr_value_gen (print mkcases_rty_t    ) value
+  | Quit _       -> pr_value_gen (print quit_rty_t       ) value
+  | About _      -> pr_value_gen (print about_rty_t      ) value
+  | Init _       -> pr_value_gen (print init_rty_t       ) value
+  | Interp _     -> pr_value_gen (print interp_rty_t     ) value
+  | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) value
+  | PrintAst _   -> pr_value_gen (print print_ast_rty_t  ) value
+  | Annotate _   -> pr_value_gen (print annotate_rty_t   ) value
+let pr_call : type a. a call -> string = fun call ->
   let return what x = str_of_call call ^ " " ^ print what x in
   match call with
     | Add x        -> return add_sty_t x
@@ -731,7 +747,7 @@ let document to_string_fmt =
     (to_string_fmt (of_value (fun _ -> PCData "b") (Good ())));
   Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n"
     (to_string_fmt (of_value (fun _ -> PCData "b")
-      (Fail (Stateid.initial,Some (15,34),"error message"))));
+      (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message"))));
   document_type_encoding to_string_fmt
 
 (* vim: set foldmethod=marker: *)
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 2c8ebc655a..265a50c47c 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -13,7 +13,7 @@ open Xml_datatype
 
 type 'a call
 
-type unknown
+type unknown_call = Unknown : 'a call -> unknown_call
 
 val add         : add_sty         -> add_rty call
 val edit_at     : edit_at_sty     -> edit_at_rty call
@@ -43,7 +43,7 @@ val protocol_version : string
 (** * XML data marshalling *)
 
 val of_call : 'a call -> xml
-val to_call : xml -> unknown call
+val to_call : xml -> unknown_call
 
 val of_answer : 'a call -> 'a value -> xml
 val to_answer : 'a call -> xml -> 'a value