Estatus finally merged into the global status using inheritance.

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

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 22ad1e4cf144c6e9ed8fe4fb037d94862b7fa540..f00ea1a0fe89be0f6859ce7d91141579f5314534 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -798,7 +798,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           self#script#setGoal (Some (goal_of_switch goal_switch));
           self#render_page ~page ~goal_switch))
 
-    method nload_sequents (status : NTacStatus.tac_status) =
+    method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
+    = fun status ->
      let _,_,metasenv,subst,_ = status#obj in
       _metasenv <- `New (metasenv,subst);
       pages <- 0;
@@ -1348,8 +1349,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
          in
           self#_loadObj obj
       | _ ->
-        match self#script#grafite_status#ng_status with
-           ProofMode tstatus -> self#_loadNObj tstatus#obj
+        match self#script#grafite_status#ng_mode with
+           `ProofMode -> self#_loadNObj self#script#grafite_status#obj
          | _ -> self#blank ()
 
       (** loads a cic uri from the environment