lazy
(let mmlwidget =
TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
~packing:scrolled_window#add ~width:400 ~height:280 () in
let expr =
let term =
~packing:(vbox#pack ~expand:true ~padding:5) () in
let sequent_viewer =
TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
~packing:(scrolled_window#add) ~width:400 ~height:280 () in
object(self)
val mutable term = Cic.Rel 1 (* dummy value *)
GBin.scrolled_window ~border_width:10
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
- TermViewer.sequent_viewer ~width:400 ~height:275
- ~packing:(scrolled_window1#add) () in
+ TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
let _ = proofw_ref <- Some proofw in
let hbox3 =
GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
GBin.scrolled_window ~border_width:10
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
- TermViewer.sequent_viewer ~width:400 ~height:275
- ~packing:(scrolled_window1#add) () in
+ TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
object(self)
method proofw = (assert false : TermViewer.sequent_viewer)
method content = vbox1
(* MAIN *)
let initialize_everything () =
- let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
+ let output =
+ TermViewer.proof_viewer
+ ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object
+ ~width:350 ~height:280 ()
+ in
let notebook = new notebook in
let rendering_window' = new rendering_window output notebook in
rendering_window'#set_auto_disambiguation !auto_disambiguation;