diff options
| author | Emilio Jesus Gallego Arias | 2016-12-05 18:17:46 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:51:38 +0100 |
| commit | a8ec2dc5c330ded1ba400ef202c57e68d2533312 (patch) | |
| tree | f333e6c9367c51f7a3c208413d3fb607916a724e /ide/xmlprotocol.ml | |
| parent | 6885a398229918865378ea24f07d93d2bcdd2802 (diff) | |
[pp] Remove special tag type and handler from Pp.
For legacy reasons, pretty printing required to provide a "tag"
interpretation function `pp_tag`. However such function was not of much
use as the backends (richpp and terminal) hooked at the `Format.tag`
level.
We thus remove this unused indirection layer and annotate expressions
with their `Format` tags.
This is a step towards moving the last bit of terminal code out of the
core system.
Diffstat (limited to 'ide/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 6ed62082d7..1d50aed032 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -112,7 +112,7 @@ let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] - | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair (of_list of_string) of_pp (t,s)] + | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair of_string of_pp (t,s)] | Ppcmd_print_break (i,j) -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)] | Ppcmd_force_newline -> constructor "ppdoc" "newline" [] @@ -126,7 +126,7 @@ let rec to_pp xpp = let open Pp in | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in Ppcmd_box(bt,s) - | "tag" -> let (tg,s) = to_pair (to_list to_string) to_pp (singleton args) in + | "tag" -> let (tg,s) = to_pair to_string to_pp (singleton args) in Ppcmd_tag(tg,s) | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in Ppcmd_print_break(i, j) |