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

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 3be3ba7f1..3ca6a3a50 100644
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -25,7 +25,6 @@
 
 (*CSC codice cut & paste da cicPp e xmlcommand *)
 
-exception ImpossiblePossible;;
 exception NotImplemented;;
 
 let dtdname ~ask_dtd_to_the_getter dtd =
@@ -260,8 +259,41 @@ let print_term ~ids_to_inner_sorts =
    aux
 ;;
 
-  (* TODO ZACK implement attributes pretty printing *)
-let xml_of_attrs attributes = [< >]
+let xml_of_attrs attributes =
+  let class_of = function
+    | `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 -> 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
+   Xml.xml_nempty "attributes" [] xml_attrs
 
 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
  let find_sort id =