X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fxml%2FxmlLibrary.ml;h=59dbc4d66917ea8ae8f5e6101b1ffc5a129117d3;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=584dc776a7b8d4a0d533c1b69a1ebce7e2f01414;hpb=68b5af5ca8f1e7f98485b92692b3dcb1ae240d19;p=helm.git

diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml
index 584dc776a..59dbc4d66 100644
--- a/helm/software/helena/src/xml/xmlLibrary.ml
+++ b/helm/software/helena/src/xml/xmlLibrary.ml
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 module KF = Filename
+module KP = Printf
 
 module U  = NUri
 module C  = Cps
@@ -18,6 +19,8 @@ module H  = Hierarchy
 module N  = Layer
 module E  = Entity
 
+IFDEF OBJECTS THEN
+
 (* internal functions *******************************************************)
 
 let base = "xml"
@@ -88,6 +91,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
 
@@ -96,14 +102,24 @@ let name a =
    let f n r = "name", if r then n else "-" ^ n in 
    E.name err f a
 
-let apix a =
-   "position", string_of_int a.E.n_apix
+let restricted r =
+   "restricted", KP.sprintf "%b" r
 
 let layer st n =
    "layer", N.to_string st n
 
-let kind a =
-   "position", string_of_int a.E.n_sort
+let main (sort, degr) =
+   ["main-position", string_of_int sort;
+    "main-degree", string_of_int degr;
+   ]
+
+let side (sort, degr) =
+   ["side-position", string_of_int sort;
+    "side-degree", string_of_int degr;
+   ]
+
+let apix a =
+   "level", string_of_int a.E.n_apix
 
 let meta a =
    let map = function
@@ -126,11 +142,11 @@ 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 a = uri u :: name ba :: apix na :: meta ra :: info ra @ side a.E.e_side 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)
+      | E.Abst (a, w) -> tag "GDec" (attrs a) ~contents:(pp_term w) 
+      | E.Abbr (a, v) -> tag "GDef" (attrs a) ~contents:(pp_term v)
       | E.Void   -> assert false
    in
    let opts = if !G.si then "si" else "" in
@@ -138,3 +154,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