let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
mml_of_cic_sequent metasenv sequent
in
- self#load_doc ~dom:sequent_mml ;
+ self#load_root ~root:sequent_mml#get_documentElement ;
(*
Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
*)
let sequent_viewer ~(mml_of_cic_sequent: mml_of_cic_sequent)
?hadjustment ?vadjustment ?font_size ?log_verbosity
=
- GtkBase.Container.make_params ~cont:(
+ GtkBase.Widget.size_params ~cont:(
OgtkMathViewProps.pack_return
(fun p ->
OgtkMathViewProps.set_params
(new sequent_viewer ~mml_of_cic_sequent
- (GtkMathViewProps.MathView.create p))
+ (GtkMathViewProps.MathView_GMetaDOM.create p))
~font_size ~log_verbosity)) []
;;
(match current_mml with
None ->
let time1 = Sys.time () in
- self#load_doc ~dom:mml ;
+ self#load_root ~root:mml#get_documentElement ;
let time2 = Sys.time () in
debug_print ("Loading and displaying the proof took " ^
string_of_float (time2 -. time1) ^ "seconds") ;
let proof_viewer ~(mml_of_cic_object: mml_of_cic_object)
?hadjustment ?vadjustment ?font_size ?log_verbosity
=
- GtkBase.Container.make_params ~cont:(
+ GtkBase.Widget.size_params ~cont:(
OgtkMathViewProps.pack_return
(fun p ->
OgtkMathViewProps.set_params
(new proof_viewer ~mml_of_cic_object
- (GtkMathViewProps.MathView.create p))
+ (GtkMathViewProps.MathView_GMetaDOM.create p))
~font_size ~log_verbosity)) []
;;