X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=d485ac02588c66e31510ed7a6d6fed2935122bb6;hb=ac813b7e251e4bac1a8a16befa628203775771ca;hp=8c38cfc0bdaac85941241c1431317fcd4ea0cdde;hpb=5ee4e9d9fbff19b7937459c5ad4652542ac1ccb8;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 8c38cfc0b..d485ac025 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -172,7 +172,7 @@ class sequent_viewer obj =
 
 
 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
@@ -277,7 +277,27 @@ let proof_viewer_instance =
   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
+