From bd458575ba7f767e3b939fad5d628a9cb24e6bb2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Mar 2017 18:23:41 +0100
Subject: [pp] Add anomaly header to anomaly error messages.

This patch restores the proper printing of anomalies in coqtop / coqc
/ coqide. Currently, they are printed with an `Error` header, whereas
they should be printed with an `Anomaly" header.

This reopens an unfinished debate started in #390 , about how to
properly do "message" headers. Prior to #390, headers were handled
inconsistently, sometimes, `Error` or `Anomaly` were added in
`CErrors`, which lives below of the tagging system, thus some times we
got no coloring (c.f. https://coq.inria.fr/bugs/show_bug.cgi?id=4789),
but some other times the headers were added by the message handlers in
Feedback.

PR #390 takes the position of identifying the messages with the
`Feedback.level` tag, and letting the backends to the tagging. This
makes sense as the backends may want to interpret the "headers" in any
way they'd like. For instance, instead of printing: `Error: foo` they
may want to insert an image.

Note that this implies that CoqIDE doesn't currently insert an error
header on the first error case. This could be easily solved, but for
anomalies we could do in any of the ways explained below.

There are thus two natural ways to handle anomalies here: One is to
tag them as errors, but add a text header, this is done now, with the
small optimization in the case the handled has access to the exception
itself. The second way is to add a new `Feedback.level` category and
tag the anomalies appropriately. We would need also to modify Fail in
this case, or to completely remove it from the protocol.

I guess feedback from the rest of developers is needed before
committing to a strategy, for now this patch should be good.
---
 lib/cErrors.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 99b763602d..1c1ff7e2fd 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -92,9 +92,8 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (raw_anomaly e ++ spc () ++
-           strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
-           str ".")
+    hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e) ++ spc ()) ++
+    hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")
   else
     hov 0 (raw_anomaly e)
 
-- 
cgit v1.2.3


From 63cfc77ddf3586262d905dc351b58669d185a55e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 31 Mar 2017 20:38:52 +0200
Subject: [toplevel] Remove exception error printer in favor of feedback
 printer.

We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing
all the errors from the feedback handler, even in the case of coqtop.

All error display is handled by a single, uniform path.

There may be some minor discrepancies with 8.6 as we are uniform now
whereas 8.6 tended to print errors in several ways, but our behavior
is a subset of the 8.6 behavior.

We had to make a choice for `-emacs` error output, which used to vary
too. We have chosen to display error messages as:

```
(location info) option \n
(program caret) option \n
MARKER[254]Error: msgMARKER[255]
```

This commit also fixes:

- https://coq.inria.fr/bugs/show_bug.cgi?id=5418
- https://coq.inria.fr/bugs/show_bug.cgi?id=5429
---
 lib/pp.ml  | 19 -------------------
 lib/pp.mli |  1 -
 2 files changed, 20 deletions(-)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index 9f33756dfe..66feae761a 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -116,25 +116,6 @@ let strbrk s =
     else if p = n then [] else [str (String.sub s p (n-p))]
   in Ppcmd_glue (aux 0 0)
 
-let pr_loc_pos loc =
-  if Loc.is_ghost loc then (str"<unknown>")
-  else
-    let loc = Loc.unloc loc in
-    int (fst loc) ++ str"-" ++ int (snd loc)
-
-let pr_loc loc =
-  if Loc.is_ghost loc then str"<unknown>" ++ fnl ()
-  else
-    let fname = loc.Loc.fname in
-    if CString.equal fname "" then
-      Loc.(str"Toplevel input, characters " ++ int loc.bp ++
-	   str"-" ++ int loc.ep ++ str":" ++ fnl ())
-    else
-      Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
-	   str", line " ++ int loc.line_nb ++ str", characters " ++
-	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
-	   str":" ++ fnl())
-
 let ismt = function | Ppcmd_empty -> true | _ -> false
 
 (* boxing commands *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 802ffe8e7a..7a191b01a8 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -171,7 +171,6 @@ val surround : std_ppcmds -> std_ppcmds
 (** Surround with parenthesis. *)
 
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
-val pr_loc : Loc.t -> std_ppcmds
 
 (** {6 Main renderers, to formatter and to string } *)
 
-- 
cgit v1.2.3