diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 4 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 3 |
2 files changed, 3 insertions, 4 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 6ffe771da3..c912adcf15 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 f8f256157d..d94cb0f3ef 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" |