[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.

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