summaryrefslogtreecommitdiff
path: root/lib/richpp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/richpp.ml')
-rw-r--r--lib/richpp.ml30
1 files changed, 30 insertions, 0 deletions
diff --git a/lib/richpp.ml b/lib/richpp.ml
index 453df43d..a98273ed 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -163,4 +163,34 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
in
node xml
+type richpp = xml
+
+let repr xml = xml
+let richpp_of_xml xml = xml
+let richpp_of_string s = PCData s
+
+let richpp_of_pp pp =
+ let annotate t = match Pp.Tag.prj t Ppstyle.tag with
+ | None -> None
+ | Some key -> Some (Ppstyle.repr key)
+ in
+ let rec drop = function
+ | PCData s -> [PCData s]
+ | Element (_, annotation, cs) ->
+ let cs = List.concat (List.map drop cs) in
+ match annotation.annotation with
+ | None -> cs
+ | Some s -> [Element (String.concat "." s, [], cs)]
+ in
+ let xml = rich_pp annotate pp in
+ Element ("_", [], drop xml)
+
+let raw_print xml =
+ let buf = Buffer.create 1024 in
+ let rec print = function
+ | PCData s -> Buffer.add_string buf s
+ | Element (_, _, cs) -> List.iter print cs
+ in
+ let () = print xml in
+ Buffer.contents buf