+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
+