From 95212aba8ba0ad76e6ee913566040f5c6e2c291d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Aug 2016 12:22:24 +0200
Subject: Fix tagging of notations.

We only tag the non-whitespace substrings, rather than the whole terminal token.
---
 printing/ppconstr.ml | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 935e2d076e..a00e4bab30 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -793,6 +793,22 @@ end
 
 let do_not_tag _ x = x
 
+let split_token tag s =
+  let len = String.length s in
+  let rec parse_string off i =
+    if Int.equal i len then
+      if Int.equal off i then mt () else tag (str (String.sub s off (i - off)))
+    else if s.[i] == ' ' then
+      if Int.equal off i then parse_space 1 (succ i)
+      else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i)
+    else parse_string off (succ i)
+  and parse_space spc i =
+    if Int.equal i len then str (String.make spc ' ')
+    else if s.[i] == ' ' then parse_space (succ spc) (succ i)
+    else str (String.make spc ' ') ++ parse_string i (succ i)
+  in
+  parse_string 0 0
+
 (** Instantiating Make with tagging functions that only add style
     information. *)
 include Make (struct
@@ -801,7 +817,7 @@ include Make (struct
     let tag_evar        = tag Tag.evar
     let tag_type        = tag Tag.univ
     let tag_unparsing   = function
-    | UnpTerminal s -> tag Tag.notation
+    | UnpTerminal s -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s
     | _ -> do_not_tag ()
     let tag_constr_expr = do_not_tag
     let tag_path = tag Tag.path
-- 
cgit v1.2.3