diff options
| author | Pierre-Marie Pédrot | 2016-08-29 12:22:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-29 14:05:40 +0200 |
| commit | 95212aba8ba0ad76e6ee913566040f5c6e2c291d (patch) | |
| tree | 096644b642082128eb0fa1c72be9fd64975b1a83 | |
| parent | aa0ad1713b109da690f9a56358df1f5ba56c65e6 (diff) | |
Fix tagging of notations.
We only tag the non-whitespace substrings, rather than the whole terminal token.
| -rw-r--r-- | printing/ppconstr.ml | 18 |
1 files changed, 17 insertions, 1 deletions
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 |