Merge remote-tracking branch 'github/pr/223' into feedback-locations

Was PR#223: Allow feedback messages to carry a location.

15 files changed, 93 insertions, 72 deletions

diff --git a/.merlin b/.merlin
index 91dbc336b..7ae642233 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
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 4135ddd2d..f7c8fbb30 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:
@@ -41,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`.
@@ -69,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:
diff --git a/ide/coq.ml b/ide/coq.ml
index 61f002576..11621078d 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/coqOps.ml b/ide/coqOps.ml
index 6ffe771da..c912adcf1 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/ide_slave.ml b/ide/ide_slave.ml
index 9f10b2502..86e09922c 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -472,11 +472,11 @@ 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
-  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/ideutils.ml b/ide/ideutils.ml
index 00c3f88e5..f0698a54a 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 a55d19aa1..79509fe02 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -769,34 +769,37 @@ 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
   | "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)
-  | _ -> 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
@@ -809,7 +812,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
@@ -843,8 +845,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"
@@ -861,7 +861,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 6bca8772e..1bb998970 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/interp/syntax_def.ml b/interp/syntax_def.ml
index 891b64fa1..9a1483b10 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 431c914c0..a0ef5e570 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 d6f580fd1..bedbe226c 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
@@ -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
@@ -36,8 +35,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;
@@ -51,7 +50,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,8 +83,8 @@ 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
-  | Debug _ -> msgnl (make_body dbg  dbg_str msg)
+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
   | Warning -> Flags.if_warn (fun () ->
@@ -93,13 +92,13 @@ 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
+  | Debug   -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
   | Info    -> msg !std_ft strm
   | Notice  -> msg !std_ft strm
   | Warning ->
@@ -117,11 +116,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 +139,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))
+    (Message (lvl, loc, 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)
+  | 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 50ffd22db..d72524e65 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
@@ -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,8 +44,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;  (* The document part concerned *)
@@ -65,7 +64,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 +109,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/stm/stm.ml b/stm/stm.ml
index 87c23c30c..d460cea94 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)
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 221fb36d8..8fcca535d 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 ->
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7d8c67025..8d20bf3d1 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