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.
---
 stm/stm.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'stm')

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