From 799b4028834c1b073db8349bf75e384750fed591 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 25 Jun 2016 15:58:19 +0200
Subject: [merlin] Fix .merlin STM includes.

---
 .merlin | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/.merlin b/.merlin
index 91dbc336be..7ae6422335 100644
--- a/.merlin
+++ b/.merlin
@@ -1,4 +1,4 @@
-FLG -rectypes
+FLG -rectypes -thread
 
 S config
 B config
@@ -26,6 +26,8 @@ S printing
 B printing
 S parsing
 B parsing
+S stm
+B stm
 S toplevel
 B toplevel
 
@@ -35,3 +37,5 @@ S tools/coqdoc
 B tools/coqdoc
 S dev
 B dev
+
+PKG threads.posix
-- 
cgit v1.2.3


From 9bff82239c2a6412a26ae3c5faab42a9c9d2ccb1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 24 Jun 2016 18:51:32 +0200
Subject: [feedback] Remove unused tag on `Debug` level.

IMO level indicators are not the proper place to store this information.
---
 ide/coq.ml         |  4 ++--
 ide/ideutils.ml    |  2 +-
 ide/xmlprotocol.ml |  6 +++---
 lib/feedback.ml    | 10 +++++-----
 lib/feedback.mli   |  2 +-
 5 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/ide/coq.ml b/ide/coq.ml
index 61f002576b..11621078de 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -298,7 +298,7 @@ let handle_intermediate_message handle level content =
         | Feedback.Info    -> fun s -> Minilib.log ~level:`INFO    (xml_to_string s)
         | Feedback.Notice  -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
         | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s)
-        | Feedback.Debug _ -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
+        | Feedback.Debug   -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
   in
   logger level content
 
@@ -333,7 +333,7 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
     state.fragment <- String.sub s l_end (String.length s - l_end);
     state.lexerror <- None;
     match Xmlprotocol.is_message xml with
-    | Some (lvl, msg) ->
+    | Some (lvl, _loc, msg) ->
       handle_intermediate_message handle lvl msg;
       loop ()
     | None ->
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 00c3f88e56..f0698a54a3 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -301,7 +301,7 @@ type logger = Feedback.level -> Richpp.richpp -> unit
 
 let default_logger level message =
   let level = match level with
-  | Feedback.Debug _ -> `DEBUG
+  | Feedback.Debug -> `DEBUG
   | Feedback.Info -> `INFO
   | Feedback.Notice -> `NOTICE
   | Feedback.Warning -> `WARNING
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index a55d19aa1b..65c85ed153 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -769,15 +769,15 @@ let document to_string_fmt =
 open Feedback
 
 let of_message_level = function
-  | Debug s ->
-      Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
+  | Debug ->
+      Serialize.constructor "message_level" "debug" []
   | Info -> Serialize.constructor "message_level" "info" []
   | Notice -> Serialize.constructor "message_level" "notice" []
   | Warning -> Serialize.constructor "message_level" "warning" []
   | Error -> Serialize.constructor "message_level" "error" []
 let to_message_level =
   Serialize.do_match "message_level" (fun s args -> match s with
-  | "debug" -> Debug (Serialize.raw_string args)
+  | "debug" -> Debug
   | "info" -> Info
   | "notice" -> Notice
   | "warning" -> Warning
diff --git a/lib/feedback.ml b/lib/feedback.ml
index d6f580fd16..74a18df6f8 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -9,7 +9,7 @@
 open Xml_datatype
 
 type level =
-  | Debug of string
+  | Debug
   | Info
   | Notice
   | Warning
@@ -85,7 +85,7 @@ let make_body quoter info s = quoter (hov 0 (info ++ s))
 
 (* Generic logger *)
 let gen_logger dbg err level msg = match level with
-  | Debug _ -> msgnl (make_body dbg  dbg_str msg)
+  | Debug   -> msgnl (make_body dbg  dbg_str msg)
   | Info    -> msgnl (make_body dbg info_str msg)
   | Notice  -> msgnl msg
   | Warning -> Flags.if_warn (fun () ->
@@ -99,7 +99,7 @@ let std_logger   = gen_logger (fun x -> x) (fun x -> x)
 let color_terminal_logger level strm =
   let msg = Ppstyle.color_msg in
   match level with
-  | Debug _ -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
+  | Debug   -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
   | Info    -> msg !std_ft strm
   | Notice  -> msg !std_ft strm
   | Warning ->
@@ -121,7 +121,7 @@ let msg_info    x = !logger Info x
 let msg_notice  x = !logger Notice x
 let msg_warning x = !logger Warning x
 let msg_error   x = !logger Error x
-let msg_debug   x = !logger (Debug "_") x
+let msg_debug   x = !logger Debug x
 
 (** Feeders *)
 let feeder = ref ignore
@@ -148,7 +148,7 @@ let feedback_logger lvl msg =
 let ft_logger old_logger ft level mesg =
   let id x = x in
   match level with
-  | Debug _ -> msgnl_with ft (make_body id  dbg_str mesg)
+  | Debug   -> msgnl_with ft (make_body id  dbg_str mesg)
   | Info    -> msgnl_with ft (make_body id info_str mesg)
   | Notice  -> msgnl_with ft mesg
   | Warning -> old_logger level mesg
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 50ffd22db9..690877897e 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -10,7 +10,7 @@ open Xml_datatype
 
 (* Old plain messages (used to be in Pp) *)
 type level =
-  | Debug of string
+  | Debug
   | Info
   | Notice
   | Warning
-- 
cgit v1.2.3


From c9f9a159818c138af3b8d8a3a1023a66b88be207 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 18 Jun 2016 00:41:33 +0200
Subject: [feedback] Add optional ?loc parameter to loggers.

This is a first step to relay location info in an uniform way, as needed
by warnings and other mechanisms.

The location info remains unused for now, but coqtop printing could take
advantage of it if so wished.
---
 dev/doc/changes.txt    |  3 +++
 ide/ide_slave.ml       |  2 +-
 interp/syntax_def.ml   |  2 +-
 kernel/cbytegen.ml     |  2 +-
 lib/feedback.ml        | 26 +++++++++++++-------------
 lib/feedback.mli       | 12 ++++++------
 toplevel/metasyntax.ml |  8 ++++----
 7 files changed, 29 insertions(+), 26 deletions(-)

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 4135ddd2db..4199b71418 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -30,6 +30,9 @@ val message     : string -> unit
   proper `Feedback.msg_*` function. Clients also have no control over
   flushing, the back end takes care of it.
 
+  Also, the `msg_*` functions now take an optional `?loc` parameter
+  for relaying location to the client.
+
 * Feedback related functions and definitions have been moved to the
   `Feedback` module. `message_level` has been renamed to
   level. Functions moved from Pp to Feedback are:
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 9f10b2502a..b1f4177579 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -472,7 +472,7 @@ let print_xml =
     with e -> let e = Errors.push e in Mutex.unlock m; iraise e
 
 
-let slave_logger xml_oc level message =
+let slave_logger xml_oc ?loc level message =
   (* convert the message into XML *)
   let msg = hov 0 message in
   let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg))    in
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 891b64fa11..9a1483b105 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -93,7 +93,7 @@ let is_verbose_compat () =
 let verbose_compat kn def = function
   | Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
     let act =
-      if !verbose_compat_notations then Feedback.msg_warning else errorlabstrm ""
+      if !verbose_compat_notations then Feedback.msg_warning ?loc:None else errorlabstrm ""
     in
     let pp_def = match def with
       | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 431c914c08..a0ef5e570e 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -907,7 +907,7 @@ let compile fail_on_error ?universes:(universes=0) env c =
       Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
   with TooLargeInductive tname ->
-    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning in
+    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning ?loc:None in
       (Pp.(fn
 	   (str "Cannot compile code for virtual machine as it uses inductive " ++
 	    Id.print tname ++ str str_max_constructors));
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 74a18df6f8..12b8b27ff4 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -51,7 +51,7 @@ let default_route = 0
 open Pp
 open Pp_control
 
-type logger = level -> std_ppcmds -> unit
+type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
 
 let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
 let msgnl          strm = msgnl_with !std_ft strm
@@ -84,7 +84,7 @@ let  err_str = str "Error:"   ++ spc ()
 let make_body quoter info s = quoter (hov 0 (info ++ s))
 
 (* Generic logger *)
-let gen_logger dbg err level msg = match level with
+let gen_logger dbg err ?loc level msg = match level with
   | Debug   -> msgnl (make_body dbg  dbg_str msg)
   | Info    -> msgnl (make_body dbg info_str msg)
   | Notice  -> msgnl msg
@@ -93,10 +93,10 @@ let gen_logger dbg err level msg = match level with
   | Error   -> msgnl_with !err_ft (make_body err  err_str msg)
 
 (** Standard loggers *)
-let std_logger   = gen_logger (fun x -> x) (fun x -> x)
+let std_logger  = gen_logger (fun x -> x) (fun x -> x)
 
 (* Color logger *)
-let color_terminal_logger level strm =
+let color_terminal_logger ?loc level strm =
   let msg = Ppstyle.color_msg in
   match level with
   | Debug   -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
@@ -117,11 +117,11 @@ let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
 let logger       = ref std_logger
 let set_logger l = logger := l
 
-let msg_info    x = !logger Info x
-let msg_notice  x = !logger Notice x
-let msg_warning x = !logger Warning x
-let msg_error   x = !logger Error x
-let msg_debug   x = !logger Debug x
+let msg_info    ?loc x = !logger Info x
+let msg_notice  ?loc x = !logger Notice x
+let msg_warning ?loc x = !logger Warning x
+let msg_error   ?loc x = !logger Error x
+let msg_debug   ?loc x = !logger Debug x
 
 (** Feeders *)
 let feeder = ref ignore
@@ -140,19 +140,19 @@ let feedback ?id ?route what =
      id    = Option.default !feedback_id id;
   }
 
-let feedback_logger lvl msg =
+let feedback_logger ?loc lvl msg =
   feedback ~route:!feedback_route ~id:!feedback_id
     (Message (lvl, Richpp.richpp_of_pp msg))
 
 (* Output to file *)
-let ft_logger old_logger ft level mesg =
+let ft_logger old_logger ft ?loc level mesg =
   let id x = x in
   match level with
   | Debug   -> msgnl_with ft (make_body id  dbg_str mesg)
   | Info    -> msgnl_with ft (make_body id info_str mesg)
   | Notice  -> msgnl_with ft mesg
-  | Warning -> old_logger level mesg
-  | Error   -> old_logger level mesg
+  | Warning -> old_logger ?loc level mesg
+  | Error   -> old_logger ?loc level mesg
 
 let with_output_to_file fname func input =
   let old_logger = !logger in
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 690877897e..7b293ae30b 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -65,7 +65,7 @@ type feedback = {
  * Only one among state_id and edit_id can be provided. *)
 
 (** A [logger] takes a level plus a pretty printing doc and logs it *)
-type logger = level -> Pp.std_ppcmds -> unit
+type logger = ?loc:Loc.t -> level -> Pp.std_ppcmds -> unit
 
 (** [set_logger l] makes the [msg_*] to use [l] for logging *)
 val set_logger : logger -> unit
@@ -110,22 +110,22 @@ relaxed. *)
 (* Should we advertise these functions more? Should they be the ONLY
    allowed way to output something? *)
 
-val msg_info : Pp.std_ppcmds -> unit
+val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit
 (** Message that displays information, usually in verbose mode, such as [Foobar
     is defined] *)
 
-val msg_notice : Pp.std_ppcmds -> unit
+val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit
 (** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
 
-val msg_warning : Pp.std_ppcmds -> unit
+val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit
 (** Message indicating that something went wrong, but without serious
     consequences. *)
 
-val msg_error : Pp.std_ppcmds -> unit
+val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit
 (** Message indicating that something went really wrong, though still
     recoverable; otherwise an exception would have been raised. *)
 
-val msg_debug : Pp.std_ppcmds -> unit
+val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit
 (** For debugging purposes *)
 
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7d8c670259..8d20bf3d14 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -898,7 +898,7 @@ let find_precedence lev etyps symbols =
 	| ETName | ETBigint | ETReference ->
             begin match lev with
             | None ->
-	      ([Feedback.msg_info,strbrk "Setting notation at level 0."],0)
+	      ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
             | Some 0 ->
               ([],0)
             | _ ->
@@ -916,7 +916,7 @@ let find_precedence lev etyps symbols =
 	else [],Option.get lev)
   | Terminal _ when last_is_terminal () ->
       if Option.is_empty lev then
-	([Feedback.msg_info,strbrk "Setting notation at level 0."], 0)
+	([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
       else [],Option.get lev
   | _ ->
       if Option.is_empty lev then error "Cannot determine the level.";
@@ -988,12 +988,12 @@ let compute_pure_syntax_data df mods =
   let (msgs,(onlyparse,onlyprint,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
   let msgs =
     if onlyparse then
-      (Feedback.msg_warning,
+      (Feedback.msg_warning ?loc:None,
       strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
     else msgs in
   let msgs =
     if onlyprint then
-      (Feedback.msg_warning,
+      (Feedback.msg_warning ?loc:None,
       strbrk "The only printing modifier has no effect in Reserved Notation.")::msgs
     else msgs in
   msgs, sy_data, extra
-- 
cgit v1.2.3


From 893ea5219eb74aedf93bd53f23b5e050fb9acbf6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 25 Jun 2016 16:05:25 +0200
Subject: [feedback] Allow messages to carry a location.

The new warnings mechanism may which to forward a location to
IDEs. This also makes sense for other message types.

Next step is to remove redundant MsgError feedback type.
---
 ide/ide_slave.ml    |  4 ++--
 ide/xmlprotocol.ml  | 16 +++++++++-------
 ide/xmlprotocol.mli |  4 ++--
 lib/feedback.ml     |  6 +++---
 lib/feedback.mli    |  2 +-
 tools/fake_ide.ml   |  2 +-
 6 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index b1f4177579..86e09922c5 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -475,8 +475,8 @@ let print_xml =
 let slave_logger xml_oc ?loc level message =
   (* convert the message into XML *)
   let msg = hov 0 message in
-  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg))    in
-  let xml = Xmlprotocol.of_message level (Richpp.richpp_of_pp message) in
+  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg))         in
+  let xml = Xmlprotocol.of_message level loc (Richpp.richpp_of_pp message) in
   print_xml xml_oc xml
 
 let slave_feeder xml_oc msg =
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 65c85ed153..f8f256157d 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -784,18 +784,20 @@ let to_message_level =
   | "error" -> Error
   | x -> raise Serialize.(Marshal_error("error level",PCData x)))
 
-let of_message lvl msg =
+let of_message lvl loc msg =
   let lvl     = of_message_level lvl in
+  let xloc    = of_option of_loc loc in
   let content = of_richpp msg        in
-  Xml_datatype.Element ("message", [], [lvl; content])
+  Xml_datatype.Element ("message", [], [lvl; xloc; content])
+
 let to_message xml = match xml with
-  | Xml_datatype.Element ("message", [], [lvl; content]) ->
-      Message(to_message_level lvl, to_richpp content)
+  | Xml_datatype.Element ("message", [], [lvl; xloc; content]) ->
+      Message(to_message_level lvl, to_option to_loc xloc, to_richpp content)
   | x -> raise (Marshal_error("message",x))
 
 let is_message = function
-  | Xml_datatype.Element ("message", [], [lvl; content]) ->
-    Some (to_message_level lvl, to_richpp content)
+  | Xml_datatype.Element ("message", [], [lvl; xloc; content]) ->
+    Some (to_message_level lvl, to_option to_loc xloc, to_richpp content)
   | _ -> None
 
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
@@ -861,7 +863,7 @@ let of_feedback_content = function
       constructor "feedback_content" "fileloaded" [
         of_string dirpath;
         of_string filename ]
-  | Message (l,m) -> constructor "feedback_content" "message" [ of_message l m ]
+  | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ]
 
 let of_edit_or_state_id = function
   | Edit id -> ["object","edit"], of_edit_id id
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 6bca8772ed..1bb9989704 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -66,7 +66,7 @@ val of_feedback : Feedback.feedback -> xml
 val to_feedback : xml -> Feedback.feedback
 val is_feedback : xml -> bool
 
-val is_message : xml -> (Feedback.level * Richpp.richpp) option
-val of_message : Feedback.level -> Richpp.richpp -> xml
+val is_message : xml -> (Feedback.level * Loc.t option * Richpp.richpp) option
+val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml
 (* val to_message : xml -> Feedback.message *)
 
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 12b8b27ff4..c2b512e991 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -36,8 +36,8 @@ type feedback_content =
   | FileLoaded of string * string
   (* Extra metadata *)
   | Custom of Loc.t * string * xml
-  (* Old generic messages *)
-  | Message of level * Richpp.richpp
+  (* Generic messages *)
+  | Message of level * Loc.t option * Richpp.richpp
 
 type feedback = {
   id : edit_or_state_id;
@@ -142,7 +142,7 @@ let feedback ?id ?route what =
 
 let feedback_logger ?loc lvl msg =
   feedback ~route:!feedback_route ~id:!feedback_id
-    (Message (lvl, Richpp.richpp_of_pp msg))
+    (Message (lvl, loc, Richpp.richpp_of_pp msg))
 
 (* Output to file *)
 let ft_logger old_logger ft ?loc level mesg =
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 7b293ae30b..36fb3867fb 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -46,7 +46,7 @@ type feedback_content =
   (* Extra metadata *)
   | Custom of Loc.t * string * xml
   (* Old generic messages *)
-  | Message of level * Richpp.richpp
+  | Message of level * Loc.t option * Richpp.richpp
 
 type feedback = {
   id       : edit_or_state_id;  (* The document part concerned *)
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 221fb36d8d..8fcca535d1 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -38,7 +38,7 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   let rec loop () =
     let xml = Xml_parser.parse coqtop.xml_parser in
     match Xmlprotocol.is_message xml with
-    | Some (level, content) ->
+    | Some (level, _loc, content) ->
       logger level content;
       loop ()
     | None ->
-- 
cgit v1.2.3


From 1053a1d4e8112ae78af86024073cf03c072d1a7c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 25 Jun 2016 16:14:23 +0200
Subject: [feedback] Remove `ErrorMsg` in favor of `Message Error`.

The ErrorMsg datatype was introduced to allow locations in messages,
however, it was redundant with error and used only in one place.

We remove it in favor of a more uniform treatment of messages with
location. This patch also removes the use of `Loc.ghost` in one place.

Lightly tested.
---
 ide/coqOps.ml      |  4 +++-
 ide/xmlprotocol.ml |  3 ---
 lib/feedback.ml    |  1 -
 lib/feedback.mli   |  3 +--
 stm/stm.ml         | 12 ++++++++----
 5 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 6ffe771da3..c912adcf15 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -460,7 +460,9 @@ object(self)
           log "GlobRef" id;
           self#attach_tooltip sentence loc
             (Printf.sprintf "%s %s %s" filepath ident ty)
-      | ErrorMsg(loc, msg), Some (id,sentence) ->
+      | Message(Error, loc, msg), Some (id,sentence) ->
+          let loc = Option.default Loc.ghost loc in
+          let msg = Richpp.raw_print msg         in
           log "ErrorMsg" id;
           remove_flag sentence `PROCESSING;
           add_flag sentence (`ERROR (loc, msg));
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index f8f256157d..d94cb0f3ef 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -811,7 +811,6 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
          to_string modpath, to_string ident, to_string ty)
   | "globdef", [loc; ident; secpath; ty] ->
        GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
-  | "errormsg", [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
   | "inprogress", [n] -> InProgress (to_int n)
   | "workerstatus", [ns] ->
        let n, s = to_pair to_string to_string ns in
@@ -845,8 +844,6 @@ let of_feedback_content = function
         of_string ident;
         of_string secpath;
         of_string ty ]
-  | ErrorMsg(loc, s) ->
-      constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
   | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
   | WorkerStatus(n,s) ->
       constructor "feedback_content" "workerstatus"
diff --git a/lib/feedback.ml b/lib/feedback.ml
index c2b512e991..bedbe226c2 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -24,7 +24,6 @@ type feedback_content =
   | Processed
   | Incomplete
   | Complete
-  | ErrorMsg of Loc.t * string
   | ProcessingIn of string
   | InProgress of int
   | WorkerStatus of string * string
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 36fb3867fb..d72524e65f 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -31,7 +31,6 @@ type feedback_content =
   | Processed
   | Incomplete
   | Complete
-  | ErrorMsg of Loc.t * string
   (* STM optional data *)
   | ProcessingIn of string
   | InProgress of int
@@ -45,7 +44,7 @@ type feedback_content =
   | FileLoaded of string * string
   (* Extra metadata *)
   | Custom of Loc.t * string * xml
-  (* Old generic messages *)
+  (* Generic messages *)
   | Message of level * Loc.t option * Richpp.richpp
 
 type feedback = {
diff --git a/stm/stm.ml b/stm/stm.ml
index 87c23c30ce..d460cea943 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -11,6 +11,10 @@ let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
 let prerr_endline s = if false then begin pr_err (s ()) end else ()
 let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
 
+(* Opening ppvernac below aliases Richpp, see PR#185 *)
+let pp_to_richpp  = Richpp.richpp_of_pp
+let str_to_richpp = Richpp.richpp_of_string
+
 open Vernacexpr
 open Errors
 open Pp
@@ -40,11 +44,11 @@ let forward_feedback, forward_feedback_hook = Hook.make
 
 let parse_error, parse_error_hook = Hook.make
  ~default:(fun id loc msg ->
-        feedback ~id (ErrorMsg (loc, Pp.string_of_ppcmds msg))) ()
+        feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) ()
 
 let execution_error, execution_error_hook = Hook.make
  ~default:(fun state_id loc msg ->
-    feedback ~id:(State state_id) (ErrorMsg (loc, Pp.string_of_ppcmds msg))) ()
+    feedback ~id:(State state_id) (Message(Error, Some loc, pp_to_richpp msg))) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
@@ -1842,8 +1846,8 @@ end = struct (* {{{ *)
       feedback ~id:(State r_for) Processed
     with e when Errors.noncritical e ->
       let e = Errors.push e in
-      let msg = string_of_ppcmds (iprint e) in
-      feedback ~id:(State r_for) (ErrorMsg (Loc.ghost, msg))
+      let msg = pp_to_richpp (iprint e) in
+      feedback ~id:(State r_for) (Message (Error, None, msg))
     
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
   let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
-- 
cgit v1.2.3


From 670519d2568c1a84331bd35a32b56887bb7191d9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 25 Jun 2016 16:36:20 +0200
Subject: [doc] Update changes for feedback.

I've included some other changes that didn't happen in this PR.
---
 dev/doc/changes.txt | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 4199b71418..f7c8fbb304 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -44,16 +44,24 @@ val emacs_logger    : logger
 val feedback_logger : logger
 ````
 
+* Changes in the Feedback format/Protocol.
+
+- The `Message` feedback type now carries an optional location, the main
+  payload is encoded using the richpp document format.
+
+- The `ErrorMsg` feedback type is thus unified now with `Message` at
+  level `Error`.
+
 * We now provide several loggers, `log_via_feedback` is removed in
   favor of `set_logger feedback_logger`. Output functions are:
 
 ```` ocaml
 val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-val msg_info    : Pp.std_ppcmds -> unit
-val msg_notice  : Pp.std_ppcmds -> unit
-val msg_warning : Pp.std_ppcmds -> unit
-val msg_error   : Pp.std_ppcmds -> unit
-val msg_debug   : Pp.std_ppcmds -> unit
+val msg_error   : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_notice  : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_info    : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_debug   : ?loc:Loc.t -> Pp.std_ppcmds -> unit
 ````
 
   with the `msg_*` functions being just an alias for `logger $Level`.
@@ -72,6 +80,8 @@ val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
 val get_id_for_feedback : unit -> edit_or_state_id * route_id
 ````
 
+** Kernel API changes **
+
 - The interface of the Context module was changed.
   Related types and functions were put in separate submodules.
   The mapping from old identifiers to new identifiers is the following:
-- 
cgit v1.2.3


From a10e3e0252560992128f490dfcb3d76c4bbf317b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 25 Jun 2016 17:39:04 +0200
Subject: [xmlproto] Remove duplicated deserialization.

---
 ide/xmlprotocol.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index d94cb0f3ef..79509fe021 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -795,10 +795,11 @@ let to_message xml = match xml with
       Message(to_message_level lvl, to_option to_loc xloc, to_richpp content)
   | x -> raise (Marshal_error("message",x))
 
-let is_message = function
-  | Xml_datatype.Element ("message", [], [lvl; xloc; content]) ->
-    Some (to_message_level lvl, to_option to_loc xloc, to_richpp content)
-  | _ -> None
+let is_message xml =
+  try begin match to_message xml with
+    | Message(l,c,m) -> Some (l,c,m)
+    | _              -> None
+  end with | Marshal_error _ -> None
 
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "addedaxiom", _ -> AddedAxiom
-- 
cgit v1.2.3