diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-25 16:14:23 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-25 17:17:45 +0200 |
| commit | 1053a1d4e8112ae78af86024073cf03c072d1a7c (patch) | |
| tree | 968d9890732461ae2264ede479d22d64148078b8 /ide | |
| parent | 893ea5219eb74aedf93bd53f23b5e050fb9acbf6 (diff) | |
[feedback] Remove `ErrorMsg` in favor of `Message Error`.
The ErrorMsg datatype was introduced to allow locations in messages,
however, it was redundant with error and used only in one place.
We remove it in favor of a more uniform treatment of messages with
location. This patch also removes the use of `Loc.ghost` in one place.
Lightly tested.
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 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" |