Objects are now used to represent also the tactic status.

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

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 277dbe8f1d0361eafdbebff1a34270bd7ef27799..e93ac4f3cf1bddb4adb41c57c79e81e41a65b498 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -798,9 +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 
-      { NTacStatus.istatus = { NTacStatus.pstatus = (_,_,metasenv,subst,_) }; gstatus = stack } 
-    =
+    method nload_sequents (status : NTacStatus.tac_status) =
+     let _,_,metasenv,subst,_ = status#obj in
       _metasenv <- `New (metasenv,subst);
       pages <- 0;
       let win goal_switch =
@@ -825,7 +824,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         w#coerce
       in
       assert (
-        let stack_goals = Stack.open_goals stack in
+        let stack_goals = Stack.open_goals status#stack in
         let proof_goals = List.map fst metasenv in
         if
           HExtlib.list_uniq (List.sort Pervasives.compare stack_goals)
@@ -863,13 +862,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
             match depth, pos with
             | 0, 0 -> `Current (render_switch sw)
             | 0, _ -> `Shift (pos, `Current (render_switch sw))
-            | 1, pos when Stack.head_tag stack = `BranchTag ->
+            | 1, pos when Stack.head_tag status#stack = `BranchTag ->
                 `Shift (pos, render_switch sw)
             | _ -> render_switch sw
           in
           add_tab markup sw)
         ~cont:add_switch ~todo:add_switch
-        stack;
+        status#stack;
       switch_page_callback <-
         Some (notebook#connect#switch_page ~callback:(fun page ->
           let goal_switch =
@@ -1350,9 +1349,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           self#_loadObj obj
       | _ ->
         match self#script#grafite_status.ng_status with
-           ProofMode tstatus ->
-            let nobj = tstatus.NTacStatus.istatus.NTacStatus.pstatus in
-             self#_loadNObj nobj
+           ProofMode tstatus -> self#_loadNObj tstatus#obj
          | _ -> self#blank ()
 
       (** loads a cic uri from the environment