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:") ""
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:") ""
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 *)
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)))
;;
(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
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 () ;