diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-15 19:43:22 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-15 20:05:18 +0200 |
commit | 8e3c2182d0c43530fc2cf62e63f5474773d04604 (patch) | |
tree | db217afd54b3224f7d5a9bdea83fbed3d7b40aba /lib | |
parent | 5cec38e8a2fbe39c75404f249974227afc028f27 (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.ml | 21 |
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 |