From 5ac6c86ad8e18161151d53687da1e2825f0a6b46 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 13 Oct 2016 13:49:04 +0200
Subject: [pp] Try to properly tag error messages in cError.

In order to get proper coloring, we must tag the headers of error
messages in `CError`.

This should fix bug
https://coq.inria.fr/bugs/show_bug.cgi?id=5135

However, note that this could interact badly with the richpp printing
used by the IDE. At this level, we have no clue which tag we'd like to
apply, as we know (and shouldn't) nothing about the top level backend.

Thus, for now I've selected the console printer, hoping that the
`Richpp` won't crash the IDE.
---
 lib/cErrors.ml | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index c69c7e4001..5c56192fc5 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -16,6 +16,16 @@ let push = Backtrace.add_backtrace
 
 exception Anomaly of string option * std_ppcmds (* System errors *)
 
+(* XXX: To move to common tagging functions in Pp, blocked on tag
+ * system cleanup as we cannot define generic error tags now.
+ *
+ * Anyways, tagging should not happen here, but in the specific
+ * listener to the msg_* stuff.
+ *)
+let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc ()
+let err_str       = tag_err_str "Error:"
+let ann_str       = tag_err_str "Anomaly:"
+
 let _ =
   let pr = function
   | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"")
@@ -93,7 +103,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++
+    hov 0 (ann_str ++ raw_anomaly e ++ spc () ++
            strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
            str ".")
   else
@@ -115,7 +125,7 @@ let iprint_no_report (e, info) =
 
 let _ = register_handler begin function
   | UserError(s, pps) ->
-    hov 0 (str "Error: " ++ where (Some s) ++ pps)
+    hov 0 (err_str ++ where (Some s) ++ pps)
   | _ -> raise Unhandled
 end
 
-- 
cgit v1.2.3


From ff0fea7a07d85342586f65d68e9fdee0ff0c3d74 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 26 Oct 2016 17:35:47 +0200
Subject: STM: make ~valid state id non optional from APIs

It used to be Stateid.initial by default.  That is indeed a valid
state id but very likely not the very best one (that would be
the tip of the document).
---
 lib/stateid.ml  | 2 +-
 lib/stateid.mli | 5 ++---
 2 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/stateid.ml b/lib/stateid.ml
index 500581a39e..ae25735c5f 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -22,7 +22,7 @@ let to_int id = id
 let newer_than id1 id2 = id1 > id2
 
 let state_id_info : (t * t) Exninfo.t = Exninfo.make ()
-let add exn ?(valid = initial) id =
+let add exn ~valid id =
   Exninfo.add exn state_id_info (valid, id)
 let get exn = Exninfo.get exn state_id_info
 
diff --git a/lib/stateid.mli b/lib/stateid.mli
index cd8fddf0ce..1d87a343b3 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -26,9 +26,8 @@ val newer_than : t -> t -> bool
 
 (* Attaches to an exception the concerned state id, plus an optional
  * state id that is a valid state id before the error.
- * Backtracking to the valid id is safe.
- * The initial_state_id is assumed to be safe. *)
-val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info
+ * Backtracking to the valid id is safe. *)
+val add : Exninfo.info -> valid:t -> t -> Exninfo.info
 val get : Exninfo.info -> (t * t) option
 
 type ('a,'b) request = {
-- 
cgit v1.2.3