This commit was manufactured by cvs2svn to create branch

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e4af786ceb2e4e81a83f6f2c109f4bb881cf6ec4..8ec91964edff51159a58bb197e2d57f5bdc31aa2 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -530,11 +530,12 @@ 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
-   ~ids_to_inner_types
+  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+   ~ask_dtd_to_the_getter:true
  in
   let input =
    match bodyxml with
@@ -561,11 +562,12 @@ 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
-    ~ids_to_inner_types
+   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+    ~ask_dtd_to_the_getter:false
   in
    (* innertypes *)
    let innertypesuri = UriManager.innertypesuri_of_uri uri in
@@ -786,12 +788,6 @@ let qed () =
   | _ -> raise OpenConjecturesStillThere
 ;;
 
-(*????
-let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
-let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
-*)
-let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
-
 let save () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   match !ProofEngine.proof with
@@ -805,7 +801,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