diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-15 19:51:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-15 20:05:29 +0200 |
| commit | 2c1882815e7877bfc574f9f71eff6ce099145df5 (patch) | |
| tree | 5bcf7e3f3b1f28669da0d0fd5cd2d0e913a76d1f /lib/richpp.ml | |
| parent | 8e3c2182d0c43530fc2cf62e63f5474773d04604 (diff) | |
Statically ensure that we omit null annotations in Richpp.
Diffstat (limited to 'lib/richpp.ml')
| -rw-r--r-- | lib/richpp.ml | 19 |
1 files changed, 5 insertions, 14 deletions
diff --git a/lib/richpp.ml b/lib/richpp.ml index b02d9903b..45173ff30 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -10,7 +10,7 @@ open Util open Xml_datatype type 'annotation located = { - annotation : 'annotation option; + annotation : 'annotation; startpos : int; endpos : int } @@ -90,7 +90,7 @@ let rich_pp annotate ppcmds = | None -> child (** Ignore the node *) | Some annotation -> let annotation = { - annotation = Some annotation; + annotation = annotation; startpos = pos; endpos = context.offset; } in @@ -134,10 +134,8 @@ let rich_pp annotate ppcmds = let annotations_positions xml = let rec node accu = function - | Element (_, { annotation = Some annotation; startpos; endpos }, cs) -> + | Element (_, { annotation = annotation; startpos; endpos }, cs) -> children ((annotation, (startpos, endpos)) :: accu) cs - | Element (_, _, cs) -> - children accu cs | _ -> accu and children accu cs = @@ -152,16 +150,9 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = [ "startpos", string_of_int startpos; "endpos", string_of_int endpos ] - @ (match annotation with - | None -> [] - | Some annotation -> attributes_of_annotation annotation - ) - in - let tag = - match annotation with - | None -> index - | Some annotation -> tag_of_annotation annotation + @ (attributes_of_annotation annotation) in + let tag = tag_of_annotation annotation in Element (tag, attributes, List.map node cs) | PCData s -> PCData s |