X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fxml%2FxmlLibrary.ml;h=4667b3aa57db8fd9009d17b1416a2fab6c7866c4;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=dcc18c94b125a49c92928190820b68c278cc2b23;hpb=2cf2e883f91164ce614bdc86b5c5e2419b98f68d;p=helm.git

diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml
index dcc18c94b..4667b3aa5 100644
--- a/helm/software/helena/src/xml/xmlLibrary.ml
+++ b/helm/software/helena/src/xml/xmlLibrary.ml
@@ -18,6 +18,8 @@ module H  = Hierarchy
 module N  = Layer
 module E  = Entity
 
+IFDEF OBJECTS THEN
+
 (* internal functions *******************************************************)
 
 let base = "xml"
@@ -88,6 +90,9 @@ let void = "Void"
 let position i =
    "position", string_of_int i
 
+let depth i =
+   "depth", string_of_int i
+
 let uri u =
    "uri", U.string_of_uri u
 
@@ -100,14 +105,14 @@ let layer st n =
    "layer", N.to_string st n
 
 let main a =
-   let sort, degr = a.E.n_main in
-   ["main-sort", string_of_int sort;
+   let sort, degr = a.E.b_main in
+   ["main-position", string_of_int sort;
     "main-degree", string_of_int degr;
    ]
 
 let side a =
-   let sort, degr = a.E.n_side in
-   ["side-sort", string_of_int sort;
+   let sort, degr = a.E.b_side in
+   ["side-position", string_of_int sort;
     "side-degree", string_of_int degr;
    ]
 
@@ -135,8 +140,8 @@ let export_entity pp_term (ra, na, u, b) =
    let och = open_out (path ^ ext) in
    let out = output_string och in
    xml out "1.0" "UTF-8"; doctype out obj_root system;
-   let na = {na with E.n_name = Some (U.name_of_uri u, true)} in
-   let attrs = uri u :: name na :: apix na :: meta ra :: info ra in 
+   let ba = E.bind_attrs ~name:(U.name_of_uri u, true) () in
+   let attrs = uri u :: name ba :: apix na :: meta ra :: info ra in 
    let contents = match b with
       | E.Abst w -> tag "GDec" attrs ~contents:(pp_term w) 
       | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
@@ -147,3 +152,5 @@ let export_entity pp_term (ra, na, u, b) =
    let attrs = [xmlns; "hierarchy", shp; "options", opts] in
    tag obj_root attrs ~contents out 0;
    close_out och
+
+END