~ask_dtd_to_the_getter parameter added to Cic2Xml.print_innertypes

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index e02f8cb15d3e650c7733ef4566c405e6908313dc..f498effb6bc89944c3b068bec8ec69d360d802c0 100644 (file)
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -28,6 +28,13 @@
 exception ImpossiblePossible;;
 exception NotImplemented;;
 
+let dtdname ~ask_dtd_to_the_getter dtd =
+ if ask_dtd_to_the_getter then
+  Configuration.getter_url ^ "getdtd?uri=" ^ dtd
+ else
+  "http://mowgli.cs.unibo.it/dtd/" ^ dtd
+;;
+
 let param_attribute_of_params params =
  String.concat " " (List.map UriManager.string_of_uri params)
 ;;
@@ -249,17 +256,12 @@ let print_term ~ids_to_inner_sorts =
    aux
 ;;
 
-let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter =
+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 =
-  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
+  let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
+   match obj with
        C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
         let params' = param_attribute_of_params params in
         let xml_for_current_proof_body =
@@ -394,20 +396,28 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter =
          >], None
 ;;
 
-let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types =
+let
+ print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
+  ~ask_dtd_to_the_getter
+=
  let module C2A = Cic2acic in
  let module X = Xml in
-  X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
-   (Hashtbl.fold
-     (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
-       [< x ;
-          X.xml_nempty "TYPE" ["of",id]
-           [< print_term ids_to_inner_sorts synty ;
-              match expty with
-                 None -> [<>]
-               | Some expty' -> print_term ids_to_inner_sorts expty'
+  let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
+   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+      X.xml_cdata
+       ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
+      X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
+       (Hashtbl.fold
+         (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
+           [< x ;
+              X.xml_nempty "TYPE" ["of",id]
+               [< print_term ids_to_inner_sorts synty ;
+                  match expty with
+                     None -> [<>]
+                   | Some expty' -> print_term ids_to_inner_sorts expty'
+               >]
            >]
-       >]
-     ) ids_to_inner_types [<>]
-   )
+         ) ids_to_inner_types [<>]
+       )
+   >]
 ;;

diff --git a/helm/gTopLevel/cic2Xml.mli b/helm/gTopLevel/cic2Xml.mli
index 0ce8cb330c01f13eb0a58223970bfd5d52e81ef4..0891d4996cc02e98c482db74168832b494ef2b6f 100644 (file)
--- a/helm/gTopLevel/cic2Xml.mli
+++ b/helm/gTopLevel/cic2Xml.mli
@@ -40,4 +40,5 @@ val print_inner_types :
   UriManager.uri ->
   ids_to_inner_sorts: (string, string) Hashtbl.t ->
   ids_to_inner_types: (string, Cic2acic.anntypes) Hashtbl.t ->
+  ask_dtd_to_the_getter:bool ->
   Xml.token Stream.t

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 999d2aaf40a03bbaf8013950a638bba2142e71bc..8ec91964edff51159a58bb197e2d57f5bdc31aa2 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -534,8 +534,8 @@ let
    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
@@ -566,8 +566,8 @@ let
     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
@@ -788,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