]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/xml/xmlLibrary.ml
- new attributes system
[helm.git] / helm / software / helena / src / xml / xmlLibrary.ml
index e182ab9a39d20d45fac636194f42267b7eee3c44..1e2bd4de4d5e015ff100fcc6f09e3c5794a89059 100644 (file)
@@ -96,24 +96,15 @@ let uri u =
    "uri", U.string_of_uri u
 
 let name a =
-   let map f i n r s =
-      let n = if r then n else "-" ^ n in 
-      let spc = if i then "" else " " in
-      f (s ^ n ^ spc)
-   in
-   let f s = "name", s in
-   E.names f map a ""
+   let err () = "name", "" in
+   let f n r = "name", if r then n else "-" ^ n in 
+   E.name err f a
 
 let apix a =
    let err () = "age", "" in
    let f i = "age", string_of_int i in
    E.apix err f a
 
-let mark a =
-   let err () = "mark", "" in
-   let f i = "mark", string_of_int i in
-   E.mark err f a
-
 let level n =
    "level", N.to_string n
 
@@ -124,9 +115,7 @@ let meta a =
       | E.Progress -> "Progress"
       | E.Private  -> "Private"
    in
-   let err () = "meta", "" in
-   let f ms = "meta", String.concat " " (List.rev_map map ms) in
-   E.meta err f a
+   "meta", String.concat " " (List.rev_map map a.E.r_meta)
 
 let arity l =
    "arity", string_of_int (List.length l)
@@ -137,18 +126,18 @@ let info a =
    let f lg tx = ["lang", lg; "info", tx] in
    E.info err f a
 
-let export_entity pp_term (a, u, b) = 
+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 och = open_out (path ^ ext) in
    let out = output_string och in
    xml out "1.0" "UTF-8"; doctype out obj_root system;
-   let a = E.Name (U.name_of_uri u, true) :: a in
-   let attrs = uri u :: name a :: apix a :: meta a :: info a in 
+   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 contents = match b with
-      | E.Abst (n, w) -> tag "GDec" (level n :: attrs) ~contents:(pp_term w) 
-      | E.Abbr v      -> tag "GDef" attrs ~contents:(pp_term v)
-      | E.Void        -> assert false
+      | E.Abst w -> tag "GDec" attrs ~contents:(pp_term w) 
+      | 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
@@ -171,7 +160,7 @@ let precs = function
 let nexts = function
    | [] -> "next", ""
    | l  -> "next", String.concat " " (List.rev_map next_map l)
-
+(*
 let export_csys s = 
    let path = path_of_uri !G.xdir s.Q.buri in
    let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in
@@ -187,3 +176,4 @@ let export_csys s =
    in
    tag ccs_root attrs ~contents out 0;
    close_out och
+*)