class sequents_viewer ~(notebook:GPack.notebook)
- ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal ()
+ ~(sequent_viewer:sequent_viewer) ~set_goal ()
=
let tab_label metano =
(GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
fun () -> Lazy.force instance
let sequents_viewer ~(notebook:GPack.notebook)
- ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal ()
+ ~(sequent_viewer:sequent_viewer) ~set_goal ()
=
new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
+let check_widget =
+ lazy
+ (let gui = MatitaGui.instance () in
+ sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add ())
+
+class mathViewer =
+ object
+ method checkTerm sequent metasenv =
+ let (metano, context, expr) = sequent in
+ let widget = Lazy.force check_widget in
+ let gui = MatitaGui.instance () in
+ gui#check#checkWin#show ();
+ gui#main#showCheckMenuItem#set_active true;
+ widget#load_sequent (sequent :: metasenv) metano
+
+ method unload () = (proof_viewer_instance ())#unload
+ end
+
+let mathViewer () = new mathViewer
+