From 1053a1d4e8112ae78af86024073cf03c072d1a7c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 25 Jun 2016 16:14:23 +0200
Subject: [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.
---
 ide/xmlprotocol.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'ide/xmlprotocol.ml')

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"
-- 
cgit v1.2.3