added "tags" target to generate vim tags with otags

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index addf9763cc2350125be11b57792f8d41d1a5f506..c9e0b217faf4e0638841b06f940a16273b38931e 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -370,13 +370,16 @@ class cicBrowser_impl ~(history:string MatitaMisc.history) () =
       mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement
 
     method private home () =
-      if self#script#onGoingProof () then
-        let ((uri, metasenv, bo, ty), _) = self#script#proofStatus in
-        let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
-        let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
-        self#loadObj obj
-      else
-        self#blank ()
+      match self#script#status.proof_status with
+      | Proof  (uri, metasenv, bo, ty) ->
+          let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
+          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          self#loadObj obj
+      | Incomplete_proof ((uri, metasenv, bo, ty), _) -> 
+          let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
+          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          self#loadObj obj
+      | _ -> self#blank ()
 
       (** loads a cic uri from the environment
       * @param uri UriManager.uri *)
@@ -511,3 +514,8 @@ let default_sequentsViewer () =
   sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer ()
 let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
 
+
+let mathViewer () = 
+  object 
+    method show_term t = (cicBrowser ()) # loadTerm t
+  end