X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fxml%2FxmlLibrary.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fxml%2FxmlLibrary.ml;h=2796bae24ec23884875543bf79eaa2d14a3209e1;hb=fa5cd121c672589afc0ac8ddd5d184897a38c7c6;hp=7355c98a76d8d4516c99fb411c6bad3c66e6f8d8;hpb=5280ec9794de75e63ffc01bddf1756ebcca02be0;p=helm.git

diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.ml b/helm/software/lambda-delta/src/xml/xmlLibrary.ml
index 7355c98a7..2796bae24 100644
--- a/helm/software/lambda-delta/src/xml/xmlLibrary.ml
+++ b/helm/software/lambda-delta/src/xml/xmlLibrary.ml
@@ -30,7 +30,11 @@ let ccs_name = "ccs.ldc"
 
 let ccs_root = "CCS"
 
-let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
+let home = "http://lambda-delta.info"
+
+let system = home ^ "/" ^ base ^ "/ld.dtd"
+
+let xmlns = "xmlns", home
 
 let path_of_uri xdir uri =
    let base = F.concat xdir base in 
@@ -120,12 +124,23 @@ let mark a =
 let level n =
    "level", N.to_string n
 
-(* TODO: the string s must be quoted *)
 let meta a =
+   let map = function
+      | E.Main     -> "Main"
+      | E.InProp   -> "InProp"
+      | E.Progress -> "Progress"
+      | E.Private  -> "Private"
+   in
    let err () = "meta", "" in
-   let f s = "meta", s in
+   let f ms = "meta", String.concat " " (List.rev_map map ms) in
    E.meta err f a
 
+(* TODO: the string tx must be quoted *)
+let info a =
+   let err () = ["lang", ""; "info", ""] in
+   let f lg tx = ["lang", lg; "info", tx] in
+   E.info err f a
+
 let export_entity pp_term (a, u, b) = 
    let path = path_of_uri !G.xdir u in
    let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
@@ -133,7 +148,7 @@ let export_entity pp_term (a, u, b) =
    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; mark a; meta a] in 
+   let attrs = uri u :: name a :: mark a :: meta a :: info a in 
    let contents = match b with
       | E.Abst (n, w) -> tag "ABST" (level n :: attrs) ~contents:(pp_term w) 
       | E.Abbr v      -> tag "ABBR" attrs ~contents:(pp_term v)
@@ -141,7 +156,7 @@ let export_entity pp_term (a, u, b) =
    in
    let opts = if !G.si then "si" else "" in
    let shp = H.string_of_graph () in
-   let attrs = ["hierarchy", shp; "options", opts] in
+   let attrs = [xmlns; "hierarchy", shp; "options", opts] in
    tag obj_root attrs ~contents out 0;
    close_out och
 
@@ -168,7 +183,7 @@ let export_csys s =
    let och = open_out name in
    let out = output_string och in
    xml out "1.0" "UTF-8"; doctype out ccs_root system;
-   let attrs = [uri s.Q.uri] in
+   let attrs = [xmlns; uri s.Q.uri] in
    let contents out tab =
       tag "ToPositive" [arity s.Q.tp; marks s.Q.tp] out tab;
       tag "ToOne" [arity s.Q.t1; marks s.Q.t1] out tab;