inherit GMathViewAux.single_selection_math_view obj
- initializer self#set_font_size 10
+(* initializer self#set_font_size 10 *)
val mutable current_infos = None
+ val mutable current_mml = None
method make_sequent_of_selected_term =
match self#get_selection with
~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
in
self#load_doc ~dom:mml ;
+ current_mml <- Some mml ;
current_infos <-
Some
(ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ;
let time3 = Sys.time () in
(* ignore (Misc.domImpl#saveDocumentToFile mml "tmp1" ()); *)
prerr_endline "(******** FINE DOM **********)";
- self#load_doc ~dom:mml;
+ (match current_mml with
+ None ->
+ let time1 = Sys.time () in
+ self#load_doc ~dom:mml ;
+ let time2 = Sys.time () in
+ prerr_endline ("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
+ prerr_endline ("XMLDIFF took " ^ string_of_float (time2 -. time1) ^ "seconds") ;
+ self#thaw ;
+ let time3 = Sys.time () in
+ prerr_endline ("The refresh of the widget took " ^ string_of_float (time3 -. time2) ^ "seconds")
+ ) ;
+(*
+ self#load_doc ~dom:mml ;
+ current_mml <- Some mml ;
+*)
prerr_endline ("Fine loading:" ^ (string_of_float (time3 -. time2)))
(*
self#load_uri "tmp";