]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/xml/xmlLibrary.ml
- simpler attribute system
[helm.git] / helm / software / helena / src / xml / xmlLibrary.ml
index 002688b31dae912534ae0818eb7b75dae5a8f6d7..901c783a20273edcfc18c16e20d449d245afcc3d 100644 (file)
@@ -103,13 +103,13 @@ let layer st n =
    "layer", N.to_string st n
 
 let main a =
-   let sort, degr = a.E.n_main in
+   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
+   let sort, degr = a.E.b_side in
    ["side-position", string_of_int sort;
     "side-degree", string_of_int degr;
    ]
@@ -138,8 +138,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)