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

diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml
index 4667b3aa5..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
@@ -77,7 +78,7 @@ let gref = "GRef"
 
 let cast = "Cast"
 
-let appl x = if x then "Appx" else "Appr"
+let appl = "Appl"
 
 let proj = "Proj"
 
@@ -101,17 +102,18 @@ let name a =
    let f n r = "name", if r then n else "-" ^ n in 
    E.name err f a
 
+let restricted r =
+   "restricted", KP.sprintf "%b" r
+
 let layer st n =
    "layer", N.to_string st n
 
-let main a =
-   let sort, degr = a.E.b_main in
+let main (sort, degr) =
    ["main-position", string_of_int sort;
     "main-degree", string_of_int degr;
    ]
 
-let side a =
-   let sort, degr = a.E.b_side in
+let side (sort, degr) =
    ["side-position", string_of_int sort;
     "side-degree", string_of_int degr;
    ]
@@ -141,10 +143,10 @@ let export_entity pp_term (ra, na, u, b) =
    let out = output_string och in
    xml out "1.0" "UTF-8"; doctype out obj_root system;
    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 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