(* initializer self#set_log_verbosity 3 *)
+ initializer
+ ignore (self#connect#click (fun (gdome_elt, _, _, _) ->
+ match gdome_elt with
+ | Some gdome_elt -> ignore (self#action_toggle gdome_elt)
+ | None -> ()))
+
val mutable current_infos = None
val mutable current_mathml = None
ApplyTransformation.mml_of_cic_object ~explode_all:true
(unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types
in
+ debug_print "load_proof: dumping MathML to /tmp/proof";
+ ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/proof" ~doc:mathml ());
match current_mathml with
| None ->
debug_print "no previous MathML";