aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-08-15 19:43:22 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-08-15 20:05:18 +0200
commit8e3c2182d0c43530fc2cf62e63f5474773d04604 (patch)
treedb217afd54b3224f7d5a9bdea83fbed3d7b40aba /lib
parent5cec38e8a2fbe39c75404f249974227afc028f27 (diff)
Fixing richpp behaviour w.r.t. its specification.
Contrarily to what was described in the API, nodes without annotations were not ignored by the printer but left there instead.
Diffstat (limited to 'lib')
-rw-r--r--lib/richpp.ml21
1 files changed, 13 insertions, 8 deletions
diff --git a/lib/richpp.ml b/lib/richpp.ml
index c4a9c39d5..b02d9903b 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -85,18 +85,23 @@ let rich_pp annotate ppcmds =
try Int.Map.find (int_of_string node) context.annotations
with _ -> None
in
- let annotation = {
- annotation = annotation;
- startpos = pos;
- endpos = context.offset;
- } in
- let xml = Element (node, annotation, List.rev child) in
+ let child = List.rev child in
+ let xml = match annotation with
+ | None -> child (** Ignore the node *)
+ | Some annotation ->
+ let annotation = {
+ annotation = Some annotation;
+ startpos = pos;
+ endpos = context.offset;
+ } in
+ [Element (node, annotation, child)]
+ in
match ctx with
| Leaf ->
(** Final node: we keep the result in a dummy context *)
- context.stack <- Node ("", [xml], 0, Leaf)
+ context.stack <- Node ("", List.rev xml, 0, Leaf)
| Node (node, child, pos, ctx) ->
- context.stack <- Node (node, xml :: child, pos, ctx)
+ context.stack <- Node (node, List.rev_append xml child, pos, ctx)
in
let open Format in