]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/xml/xmlLibrary.ml
- bugfix is refreshed state of AutCrg: now we return a fresh state
[helm.git] / helm / software / helena / src / xml / xmlLibrary.ml
index 4caa7c1c2f50008b12db6f7ad7ed6d3185cb7503..d51af0bfb742b66e32af98e90ab47baad0cc5edc 100644 (file)
@@ -9,14 +9,14 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module F = Filename
+module KF = Filename
 
-module U = NUri
-module C = Cps
-module G = Options
-module H = Hierarchy
-module N = Level
-module E = Entity
+module U  = NUri
+module C  = Cps
+module G  = Options
+module H  = Hierarchy
+module N  = Layer
+module E  = Entity
 
 (* internal functions *******************************************************)
 
@@ -24,17 +24,17 @@ let base = "xml"
 
 let ext = ".xml"
 
-let obj_root = "ENTITY"
+let obj_root = "CONSTANT"
 
 let home = "http://lambdadelta.info/"
 
-let system = F.concat (F.concat home base) "ld.dtd"
+let system = KF.concat (KF.concat home base) "ld.dtd"
 
 let xmlns = "xmlns", home
 
 let path_of_uri xdir uri =
-   let base = F.concat xdir base in 
-   F.concat base (Str.string_after (U.string_of_uri uri) 3)
+   let base = KF.concat xdir base in 
+   KF.concat base (Str.string_after (U.string_of_uri uri) 3)
 
 (* interface functions ******************************************************)
 
@@ -99,8 +99,8 @@ let name a =
 let apix a =
    "position", string_of_int a.E.n_apix
 
-let level st n =
-   "level", N.to_string st n
+let layer st n =
+   "layer", N.to_string st n
 
 let kind a =
    "position", string_of_int a.E.n_sort
@@ -122,7 +122,7 @@ let info a =
 
 let export_entity pp_term (ra, na, u, b) = 
    let path = path_of_uri !G.xdir u in
-   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
+   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (KF.dirname path)) in
    let och = open_out (path ^ ext) in
    let out = output_string och in
    xml out "1.0" "UTF-8"; doctype out obj_root system;
@@ -133,8 +133,7 @@ let export_entity pp_term (ra, na, u, b) =
       | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
       | E.Void   -> assert false
    in
-   let opts = if !G.si then "si" else "" in
    let shp = H.string_of_graph () in
-   let attrs = [xmlns; "hierarchy", shp; "options", opts] in
+   let attrs = [xmlns; "hierarchy", shp] in
    tag obj_root attrs ~contents out 0;
    close_out och