let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
mml_of_cic_sequent metasenv sequent
in
let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
mml_of_cic_sequent metasenv sequent
in
let sequent_viewer ~(mml_of_cic_sequent: mml_of_cic_sequent)
?hadjustment ?vadjustment ?font_size ?log_verbosity
=
let sequent_viewer ~(mml_of_cic_sequent: mml_of_cic_sequent)
?hadjustment ?vadjustment ?font_size ?log_verbosity
=
OgtkMathViewProps.pack_return
(fun p ->
OgtkMathViewProps.set_params
(new sequent_viewer ~mml_of_cic_sequent
OgtkMathViewProps.pack_return
(fun p ->
OgtkMathViewProps.set_params
(new sequent_viewer ~mml_of_cic_sequent
let time2 = Sys.time () in
debug_print ("Loading and displaying the proof took " ^
string_of_float (time2 -. time1) ^ "seconds") ;
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
=
let proof_viewer ~(mml_of_cic_object: mml_of_cic_object)
?hadjustment ?vadjustment ?font_size ?log_verbosity
=
OgtkMathViewProps.pack_return
(fun p ->
OgtkMathViewProps.set_params
(new proof_viewer ~mml_of_cic_object
OgtkMathViewProps.pack_return
(fun p ->
OgtkMathViewProps.set_params
(new proof_viewer ~mml_of_cic_object