From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 15 Jun 2005 16:37:16 +0000 (+0000)
Subject: DTD for attributes revised.
X-Git-Tag: INDEXING_NO_PROOFS~142
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=05feb31551afc1eafd1d350c3facc23fdda5bebe;p=helm.git

DTD for attributes revised.
New syntax:
 <attributes>
  <class type="..">
   ...
  </class>
  <generated />
 </attributes>
where the ... are the arguments of the class and the class and generated
elements are optional. For the "elim" class the only argument is the SORT.
For the "record" class the arguments are a list of <field name=".."/>
---

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 8bf8d5f3b..056240ef1 100644
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -261,20 +261,30 @@ 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 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
   in
-  let xml_attrs = List.map xml_attr_of attributes in
-  Xml.xml_empty "attributes" xml_attrs
+  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 =