diff options
| author | Maxime Dénès | 2016-06-27 15:16:56 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-27 18:35:08 +0200 |
| commit | d4725f692a5f202ca4c5d6341b586b0e377f6973 (patch) | |
| tree | 9cd74c65a51ca06547e9117b4d4901ec18a9519b /stm | |
| parent | 403c12ac3e8a9c3719aacbfa113600abc74846b7 (diff) | |
| parent | a10e3e0252560992128f490dfcb3d76c4bbf317b (diff) | |
Merge remote-tracking branch 'github/pr/223' into feedback-locations
Was PR#223: Allow feedback messages to carry a location.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 12 |
1 files changed, 8 insertions, 4 deletions
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) |