diff options
| -rw-r--r-- | dev/doc/changes.txt | 3 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 2 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 2 | ||||
| -rw-r--r-- | kernel/cbytegen.ml | 2 | ||||
| -rw-r--r-- | lib/feedback.ml | 26 | ||||
| -rw-r--r-- | lib/feedback.mli | 12 | ||||
| -rw-r--r-- | 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 |