sync with Xml.pp

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index de725228e5061096b489880502f1b2ccd2e3ea14..d3e39351c04804cf06a3c0fe8cfdbd21668fd6b7 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -375,14 +375,14 @@ let
   in
    (* innertypes *)
    let innertypesuri = UriManager.innertypesuri_of_uri uri in
-    Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
+    Xml.pp ~gzip:false xmlinnertypes (Some (path ^ ".types.xml")) ;
     Http_getter.register' innertypesuri
      (Helm_registry.get "local_library.url" ^
        Str.replace_first (Str.regexp "^cic:") ""
         (UriManager.string_of_uri innertypesuri) ^ ".xml"
      ) ;
     (* constant type / variable / mutual inductive types definition *)
-    Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
+    Xml.pp ~gzip:false xml (Some (path ^ ".xml")) ;
     Http_getter.register' uri
      (Helm_registry.get "local_library.url" ^
        Str.replace_first (Str.regexp "^cic:") ""
@@ -397,7 +397,7 @@ let
             None -> assert false
           | Some bodyuri -> bodyuri
         in
-         Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
+         Xml.pp ~gzip:false bodyxml' (Some (path ^ ".body.xml")) ;
          Http_getter.register' bodyuri
           (Helm_registry.get "local_library.url" ^
             Str.replace_first (Str.regexp "^cic:") ""
@@ -490,10 +490,10 @@ let save_unfinished_proof () =
  let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
  let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
  let proof_file = Helm_registry.get "gtoplevel.proof_file" in
- Xml.pp ~quiet:true xml (Some proof_file_type) ;
+ Xml.pp ~gzip:false xml (Some proof_file_type) ;
  HelmLogger.log
   (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ;
- Xml.pp ~quiet:true bodyxml (Some proof_file) ;
+ Xml.pp ~gzip:false bodyxml (Some proof_file) ;
  HelmLogger.log
   (`Msg (`T ("Current proof body saved to " ^ proof_file)))
 ;;