X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=3ca6a3a5040990370f722c0e8c30755b1a1eba3d;hb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;hp=1facd4fd9c59cb7c2d65af71495df96192f43ed4;hpb=e011e7cd08af361cb5de9c953bfc58b4cd918308;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 1facd4fd9..3ca6a3a50 100644
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -261,20 +261,39 @@ let print_term ~ids_to_inner_sorts =
 
 let xml_of_attrs attributes =
   let class_of = function
-    | `Coercion -> "coercion"
-    | `Elim Cic.Prop -> "elimProp"
-    | `Elim Cic.CProp -> "elimCProp"
-    | `Elim Cic.Set -> "elimSet"
-    | `Elim (Cic.Type _) -> "elimType"
-    | `Record -> "record"
-    | `Projection -> "projection"
+    | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
+    | `Elim s ->
+        Xml.xml_nempty "class" [None,"value","elim"]
+         [< Xml.xml_empty
+             "SORT" [None,"value",
+                      (Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)) ;
+                     None,"id","elimination_sort"] >]
+    | `Record field_names ->
+        Xml.xml_nempty "class" [None,"value","record"]
+         (List.fold_right
+           (fun name res ->
+             [< Xml.xml_empty "field" [None,"name",name]; res >]
+           ) field_names [<>])
+    | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
+  in
+  let flavour_of = function
+    | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
+    | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
+    | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
+    | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
+    | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
+    | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
   in
   let xml_attr_of = function
-    | `Generated -> None, "generated", "true"
-    | `Class c -> None, "class", class_of c
+    | `Generated -> Xml.xml_empty "generated" []
+    | `Class c -> class_of c
+    | `Flavour f -> flavour_of f
+  in
+  let xml_attrs =
+   List.fold_right 
+    (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
   in
-  let xml_attrs = List.map xml_attr_of attributes in
-  Xml.xml_empty "attributes" xml_attrs
+   Xml.xml_nempty "attributes" [] xml_attrs
 
 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
  let find_sort id =