- 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 -> ()));
- ignore (self#connect#selection_changed (choose_selection self))
-
- method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
- let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
- ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- Cic2acic.acic_object_of_cic_object (cicCurrentProof proof)
- in
- current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_conjectures,
- ids_to_hypotheses);
- let mathml =
- 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 ./proof";
- ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
- match current_mathml with
- | None ->
- self#load_root ~root:mathml#get_documentElement ;
- current_mathml <- Some mathml
- | Some current_mathml ->
- self#freeze;
- XmlDiff.update_dom ~from:current_mathml mathml ;
- self#thaw
+ method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
+ let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
+ ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
+ Cic2acic.acic_object_of_cic_object (cicCurrentProof proof)
+ in
+ current_infos <- Some (ids_to_terms, ids_to_father_ids,
+ ids_to_conjectures, ids_to_hypotheses);
+ let mathml =
+ 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 ./proof";
+ ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
+ match current_mathml with
+ | None ->
+ self#load_root ~root:mathml#get_documentElement ;
+ current_mathml <- Some mathml
+ | Some current_mathml ->
+ self#freeze;
+ XmlDiff.update_dom ~from:current_mathml mathml ;
+ self#thaw