From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 19 Nov 2002 16:48:08 +0000 (+0000)
Subject: Param ~ask_dtd_to_the_getter added to Cic2Xml.print_object.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4552f835b71ca9529bf5b07d0dd2b1c699ecf928;p=helm.git

Param ~ask_dtd_to_the_getter added to Cic2Xml.print_object.
---

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index d76df870e..e02f8cb15 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -28,8 +28,6 @@
 exception ImpossiblePossible;;
 exception NotImplemented;;
 
-let dtdname = "http://localhost:8081/getdtd?uri=cic.dtd";;
-
 let param_attribute_of_params params =
  String.concat " " (List.map UriManager.string_of_uri params)
 ;;
@@ -251,11 +249,16 @@ let print_term ~ids_to_inner_sorts =
    aux
 ;;
 
-let print_object uri ~ids_to_inner_sorts =
- let rec aux =
-  let module C = Cic in
-  let module X = Xml in
-  let module U = UriManager in
+let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter =
+ let module C = Cic in
+ let module X = Xml in
+ let module U = UriManager in
+ let dtdname =
+  if ask_dtd_to_the_getter then
+   Configuration.getter_url ^ "getdtd?uri=cic.dtd"
+  else
+   "http://www.cs.unibo.it/helm/dtd/cic.dtd"
+ in
     function
        C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
         let params' = param_attribute_of_params params in
@@ -302,13 +305,12 @@ let print_object uri ~ids_to_inner_sorts =
         in
         let xmlbo =
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
-            X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^dtdname ^"\">\n");
+            X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
             xml_for_current_proof_body
          >] in
         let xmlty =
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
-            X.xml_cdata
-             ("<!DOCTYPE ConstantType SYSTEM \"" ^ dtdname ^ "\">\n");
+            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
             xml_for_current_proof_type
          >]
         in
@@ -332,7 +334,7 @@ let print_object uri ~ids_to_inner_sorts =
         in
         let xmlty =
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
-            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^dtdname ^"\">\n");
+            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
              X.xml_nempty "ConstantType"
               ["name",n ; "params",params' ; "id", id]
               [< print_term ids_to_inner_sorts ty >]
@@ -361,8 +363,8 @@ let print_object uri ~ids_to_inner_sorts =
      | C.AInductiveDefinition (id,tys,params,nparams) ->
         let params' = param_attribute_of_params params in
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
-            X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
-             dtdname ^ "\">\n") ;
+            X.xml_cdata
+             ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
             X.xml_nempty "InductiveDefinition"
              ["noParams",string_of_int nparams ;
               "id",id ;
@@ -390,8 +392,6 @@ let print_object uri ~ids_to_inner_sorts =
                 )
              >]
          >], None
- in
-  aux
 ;;
 
 let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types =
diff --git a/helm/gTopLevel/cic2Xml.mli b/helm/gTopLevel/cic2Xml.mli
index 52a6f77eb..0ce8cb330 100644
--- a/helm/gTopLevel/cic2Xml.mli
+++ b/helm/gTopLevel/cic2Xml.mli
@@ -33,6 +33,7 @@ val print_term :
 val print_object :
   UriManager.uri ->
   ids_to_inner_sorts: (string, string) Hashtbl.t ->
+  ask_dtd_to_the_getter:bool ->
   Cic.annobj -> Xml.token Stream.t * Xml.token Stream.t option
 
 val print_inner_types :
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e4af786ce..999d2aaf4 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -530,7 +530,8 @@ let
 =
 (*CSC: ????????????????? *)
  let xml, bodyxml =
-  Cic2Xml.print_object uri ~ids_to_inner_sorts annobj 
+  Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
+   annobj 
  in
  let xmlinnertypes =
   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
@@ -561,7 +562,8 @@ let
  in
   let path = pathname ^ "/" ^ name in
   let xml, bodyxml =
-   Cic2Xml.print_object uri ~ids_to_inner_sorts annobj 
+   Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
+    annobj 
   in
   let xmlinnertypes =
    Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
@@ -805,7 +807,10 @@ let save () =
         Cic2acic.acic_object_of_cic_object currentproof
        in
         let xml, bodyxml =
-         match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
+         match
+          Cic2Xml.print_object uri ~ids_to_inner_sorts
+           ~ask_dtd_to_the_getter:true acurrentproof
+         with
             xml,Some bodyxml -> xml,bodyxml
           | _,None -> assert false
         in