From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 21 Jan 2005 09:29:48 +0000 (+0000)
Subject: attributes support (not yet in the pretty printer)
X-Git-Tag: V_0_1_0~106
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6a6d9950d0c3a7974bc0f0d8a85369b733138647;p=helm.git

attributes support (not yet in the pretty printer)
---

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index b3467ad9e..5d614db05 100644
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -265,20 +265,25 @@ let print_term ~ids_to_inner_sorts =
    aux
 ;;
 
+  (* TODO ZACK implement attributes pretty printing *)
+let xml_of_attrs attributes = [< >]
+
 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
  let module C = Cic in
  let module X = Xml in
  let module U = UriManager in
   let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
    match obj with
-       C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
+       C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
         let params' = param_attribute_of_params params in
+        let xml_attrs = xml_of_attrs obj_attrs in
         let xml_for_current_proof_body =
 (*CSC: Should the CurrentProof also have the list of variables it depends on? *)
 (*CSC: I think so. Not implemented yet.                                       *)
          X.xml_nempty "CurrentProof"
           [None,"of",UriManager.string_of_uri uri ; None,"id", id]
-          [< List.fold_left
+          [< xml_attrs;
+            List.fold_left
               (fun i (cid,n,canonical_context,t) ->
                 [< i ;
                    X.xml_nempty "Conjecture"
@@ -309,7 +314,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
                         (print_term ids_to_inner_sorts t)
                     >]
                 >])
-              [<>] conjectures ;
+              [< >] conjectures ;
              X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
         in
         let xml_for_current_proof_type =
@@ -329,8 +334,9 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
          >]
         in
          xmlty, Some xmlbo
-     | C.AConstant (id,idbody,n,bo,ty,params) ->
+     | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
         let params' = param_attribute_of_params params in
+        let xml_attrs = xml_of_attrs obj_attrs in
         let xmlbo =
          match bo with
             None -> None
@@ -351,12 +357,13 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
             X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
              X.xml_nempty "ConstantType"
               [None,"name",n ; None,"params",params' ; None,"id", id]
-              [< print_term ids_to_inner_sorts ty >]
+              [< xml_attrs; print_term ids_to_inner_sorts ty >]
          >]
         in
          xmlty, xmlbo
-     | C.AVariable (id,n,bo,ty,params) ->
+     | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
         let params' = param_attribute_of_params params in
+        let xml_attrs = xml_of_attrs obj_attrs in
         let xmlbo =
          match bo with
             None -> [< >]
@@ -368,14 +375,15 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
             X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
              X.xml_nempty "Variable"
               [None,"name",n ; None,"params",params' ; None,"id", id]
-              [< xmlbo ;
+              [< xml_attrs; xmlbo;
                  X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
               >]
          >]
         in
          aobj, None
-     | C.AInductiveDefinition (id,tys,params,nparams) ->
+     | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
         let params' = param_attribute_of_params params in
+        let xml_attrs = xml_of_attrs obj_attrs in
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
             X.xml_cdata
              ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
@@ -383,7 +391,8 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
              [None,"noParams",string_of_int nparams ;
               None,"id",id ;
               None,"params",params']
-             [< (List.fold_left
+             [< xml_attrs;
+                (List.fold_left
                   (fun i (id,typename,finite,arity,cons) ->
                     [< i ;
                        X.xml_nempty "InductiveType"