X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=d3e39351c04804cf06a3c0fe8cfdbd21668fd6b7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f7d502066fddc2e9f356b0c77c9e181192fe4f4f;hpb=18bd1d094e9227822ea8c0fa4f9668cd8752236f;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index f7d502066..d3e39351c 100644
--- 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:") ""
@@ -451,7 +451,7 @@ let qed () =
 		  Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[]) 
                 in
 		let (acic,ids_to_inner_types,ids_to_inner_sorts) =
-		  (rendering_window ())#output#load_proof uri proof
+		  (rendering_window ())#output#load_proof proof
 		in
 		  !qed_set_sensitive false ;
 		  (* let's save the theorem and register it to the getter *) 
@@ -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)))
 ;;
@@ -564,7 +564,7 @@ let refresh_proof (output : TermViewer.proof_viewer) =
         (uri,
          Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[]))
   in
-   ignore (output#load_proof uri currentproof)
+   ignore (output#load_proof currentproof)
  with
   e ->
  match ProofEngine.get_proof () with
@@ -864,7 +864,7 @@ let
     try
       let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures,
           ids_to_hypotheses,_,_)) =
-       ApplyTransformation.mml_of_cic_object uri obj 
+       ApplyTransformation.mml_of_cic_object obj 
       in
        window#set_title (UriManager.string_of_uri uri) ;
        window#misc#hide () ; window#show () ;