diff options
| author | Pierre-Marie Pédrot | 2015-08-15 19:51:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-08-15 20:05:29 +0200 |
| commit | 2c1882815e7877bfc574f9f71eff6ce099145df5 (patch) | |
| tree | 5bcf7e3f3b1f28669da0d0fd5cd2d0e913a76d1f /lib | |
| parent | 8e3c2182d0c43530fc2cf62e63f5474773d04604 (diff) | |
Statically ensure that we omit null annotations in Richpp.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/richpp.ml | 19 | ||||
| -rw-r--r-- | lib/richpp.mli | 2 |
2 files changed, 6 insertions, 15 deletions
diff --git a/lib/richpp.ml b/lib/richpp.ml index b02d9903b4..45173ff307 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 diff --git a/lib/richpp.mli b/lib/richpp.mli index bf80c8dc8c..2c20197893 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -11,7 +11,7 @@ (** Each annotation of the semi-structured document refers to the substring it annotates. *) type 'annotation located = { - annotation : 'annotation option; + annotation : 'annotation; startpos : int; endpos : int } |