X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=0923622291bc2f1057aac701a544d4fe9b612962;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=4dc34cfa1e074fdaff1f5d047cd10c6e73127949;hpb=3705200c998538c28d8cd9d3ca557616837daf05;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 4dc34cfa1..092362229 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -51,6 +51,14 @@ class proof_viewer obj = (* initializer self#set_log_verbosity 3 *) + initializer + ignore (self#connect#click (fun (gdome_elt, _, _, _) -> + match gdome_elt with + | Some gdome_elt -> + prerr_endline (gdome_elt#get_nodeName#to_string); + ignore (self#action_toggle gdome_elt) + | None -> ())) + val mutable current_infos = None val mutable current_mathml = None @@ -65,6 +73,8 @@ class proof_viewer obj = 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";