we begin the commit of the validation procedure

[helm.git] / helm / software / helena / src / xml / xmlLibrary.ml

diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml
index 91225c336135384c73c48b60e492dfb0bb76714a..a7f5ae29a6e15bc94812514c7982e0b53af02ed8 100644 (file)
--- a/helm/software/helena/src/xml/xmlLibrary.ml
+++ b/helm/software/helena/src/xml/xmlLibrary.ml
@@ -116,6 +116,11 @@ let name a =
    let f s = "name", s in
    E.names f map a ""
 
+let apix a =
+   let err () = "age", "" in
+   let f i = "age", string_of_int i in
+   E.apix err f a
+
 let mark a =
    let err () = "mark", "" in
    let f i = "mark", string_of_int i in
@@ -148,10 +153,10 @@ let export_entity pp_term (a, u, b) =
    let out = output_string och in
    xml out "1.0" "UTF-8"; doctype out obj_root system;
    let a = E.Name (U.name_of_uri u, true) :: a in
-   let attrs = uri u :: name a :: mark a :: meta a :: info a in 
+   let attrs = uri u :: name a :: apix a :: meta a :: info a in 
    let contents = match b with
-      | E.Abst (n, w) -> tag "ABST" (level n :: attrs) ~contents:(pp_term w) 
-      | E.Abbr v      -> tag "ABBR" attrs ~contents:(pp_term v)
+      | E.Abst (n, w) -> tag "GDec" (level n :: attrs) ~contents:(pp_term w) 
+      | E.Abbr v      -> tag "GDef" attrs ~contents:(pp_term v)
       | E.Void        -> assert false
    in
    let opts = if !G.si then "si" else "" in