diff options
| -rw-r--r-- | ide/coqOps.ml | 4 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 3 | ||||
| -rw-r--r-- | lib/feedback.ml | 1 | ||||
| -rw-r--r-- | lib/feedback.mli | 3 | ||||
| -rw-r--r-- | stm/stm.ml | 12 |
5 files changed, 12 insertions, 11 deletions
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/xmlprotocol.ml b/ide/xmlprotocol.ml index f8f256157..d94cb0f3e 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 c2b512e99..bedbe226c 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 36fb3867f..d72524e65 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 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) |