added dump/restore environment to the debug menu

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 05f5246e5518bbfbe50de186a51f7376faea3d7c..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 *)