- (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ;
+ (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
+ (* self#load_doc ~dom:mml ;
+ current_mml <- Some mml ; *)
+ (match current_mml with
+ None ->
+ let time1 = Sys.time () in
+ self#load_doc ~dom:mml ;
+ let time2 = Sys.time () in
+ debug_print ("Loading and displaying the proof took " ^
+ string_of_float (time2 -. time1) ^ "seconds") ;
+ current_mml <- Some mml
+ | Some current_mml' ->
+ self#freeze ;
+ let time1 = Sys.time () in
+ XmlDiff.update_dom ~from:current_mml' mml ;
+ let time2 = Sys.time () in
+ debug_print ("XMLDIFF took " ^
+ string_of_float (time2 -. time1) ^ "seconds") ;
+ self#thaw ;
+ let time3 = Sys.time () in
+ debug_print ("The refresh of the widget took " ^
+ string_of_float (time3 -. time2) ^ "seconds"));