1) the home button of CicBrowser now works also for NG

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

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index ade02fb8087cb377f604810c9f805f4d6cb827f5..277dbe8f1d0361eafdbebff1a34270bd7ef27799 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -1337,14 +1337,23 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showMath;
       match self#script#grafite_status.proof_status with
       | Proof  (uri, metasenv, _subst, bo, ty, attrs) ->
-          let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
+         let name = UriManager.name_of_uri (HExtlib.unopt uri) in
+         let obj =
+          Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs)
+         in
           self#_loadObj obj
       | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
-          let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
+         let name = UriManager.name_of_uri (HExtlib.unopt uri) in
+         let obj =
+          Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs)
+         in
           self#_loadObj obj
-      | _ -> self#blank ()
+      | _ ->
+        match self#script#grafite_status.ng_status with
+           ProofMode tstatus ->
+            let nobj = tstatus.NTacStatus.istatus.NTacStatus.pstatus in
+             self#_loadNObj nobj
+         | _ -> self#blank ()
 
       (** loads a cic uri from the environment
       * @param uri UriManager.uri *)