X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=f00ea1a0fe89be0f6859ce7d91141579f5314534;hb=bbb2b03fee9f7c7595870d997118d51c1ce469f2;hp=a6aa89e8190cb62a2a0414241d113d21bbdecf5b;hpb=442f3a15d7c6afc480da02602d4d4c8db4f44c10;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index a6aa89e81..f00ea1a0f 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -186,11 +186,8 @@ object (self)
   method set_href_callback f = href_callback <- f
 
   val mutable _cic_info = None
-  val mutable _ncic_info = None
   method private set_cic_info info = _cic_info <- info
   method private cic_info = _cic_info
-  method private set_ncic_info info = _ncic_info <- info
-  method private ncic_info = _ncic_info
 
   val normal_cursor = Gdk.Cursor.create `LEFT_PTR
   val href_cursor = Gdk.Cursor.create `HAND2
@@ -514,11 +511,6 @@ object (self)
         info, (~-1, [], t) (* dummy sequent for obj *)
     | None -> assert false
 
-  method private get_ncic_info id =
-    match self#ncic_info with
-    | Some info -> info
-    | None -> assert false
-
   method private sequent_of_id ~(paste_kind:paste_kind) id =
     let cic_info, unsh_sequent = self#get_cic_info id in
     let cic_sequent =
@@ -603,10 +595,9 @@ object (self)
 
   method nload_sequent metasenv subst metano =
     let sequent = List.assoc metano metasenv in
-    let mathml,ids_to_father_ids =
+    let mathml =
      ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent)
     in
-    self#set_ncic_info (Some ids_to_father_ids);
     if BuildTimeConf.debug then begin
       let name =
        "/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
@@ -640,9 +631,10 @@ object (self)
         current_mathml <- Some mathml);
 
   method load_nobject obj =
-    let mathml,ids_to_father_ids = ApplyTransformation.nmml_of_cic_object obj in
-     self#set_ncic_info (Some ids_to_father_ids);
+    let mathml = ApplyTransformation.nmml_of_cic_object obj in
 (*
+    self#set_cic_info
+      (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
     (match current_mathml with
     | Some current_mathml when use_diff ->
         self#freeze;
@@ -806,9 +798,9 @@ 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 as 'status -> unit
+    = fun status ->
+     let _,_,metasenv,subst,_ = status#obj in
       _metasenv <- `New (metasenv,subst);
       pages <- 0;
       let win goal_switch =
@@ -833,7 +825,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)
@@ -871,13 +863,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 =
@@ -1343,7 +1335,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private home () =
       self#_showMath;
-      match self#script#grafite_status.proof_status with
+      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 =
@@ -1357,10 +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 ->
-            let nobj = tstatus.NTacStatus.istatus.NTacStatus.pstatus in
-             self#_loadNObj nobj
+        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