X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=5d614db055d92d8cd570f7f93c1b79bb6766296d;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=7594ffef1a5c4f57d00ed4631179960b2d44115b;hpb=296b163c8a2b09a6f87cbab15c2016de92fc8e70;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 7594ffef1..5d614db05 100644
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2000-2004, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -20,7 +20,7 @@
  * MA  02111-1307, USA.
  * 
  * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
+ * http://helm.cs.unibo.it/
  *)
 
 (*CSC codice cut & paste da cicPp e xmlcommand *)
@@ -30,7 +30,7 @@ exception NotImplemented;;
 
 let dtdname ~ask_dtd_to_the_getter dtd =
  if ask_dtd_to_the_getter then
-  Configuration.getter_url ^ "getdtd?uri=" ^ dtd
+  Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
  else
   "http://mowgli.cs.unibo.it/dtd/" ^ dtd
 ;;
@@ -74,7 +74,7 @@ let print_term ~ids_to_inner_sorts =
          function
             C.Prop  -> "Prop"
           | C.Set   -> "Set"
-          | C.Type  -> "Type"
+          | C.Type _ -> "Type" (* TASSI *)
 	  | C.CProp -> "CProp"
         in
          X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
@@ -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"