From 52f51fb385d6a1c90bd7d055185fee50ef2670be Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Nov 2014 20:52:54 +0100
Subject: Adding notation terminals to coqtop highlight.

---
 printing/ppconstr.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index e9fddd815c..64519446a4 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -734,12 +734,17 @@ struct
     Ppstyle.make ~style ["constr"; "keyword"]
 
   let evar =
-    let style = Terminal.make ~bold:true ~fg_color:`BLUE () in
+    let style = Terminal.make ~fg_color:`LIGHT_BLUE () in
     Ppstyle.make ~style ["constr"; "evar"]
 
   let univ =
     let style = Terminal.make ~bold:true ~fg_color:`YELLOW () in
     Ppstyle.make ~style ["constr"; "type"]
+
+  let notation =
+    let style = Terminal.make ~fg_color:`WHITE () in
+    Ppstyle.make ~style ["constr"; "notation"]
+
 end
 
 let do_not_tag _ x = x
@@ -751,7 +756,9 @@ include Make (struct
     let tag_keyword     = tag Tag.keyword
     let tag_evar        = tag Tag.evar
     let tag_type        = tag Tag.univ
-    let tag_unparsing   = do_not_tag
+    let tag_unparsing   = function
+    | UnpTerminal s -> tag Tag.notation
+    | _ -> do_not_tag ()
     let tag_constr_expr = do_not_tag
 end)
 
-- 
cgit v1.2.3