This commit restores the ids_to_father_ids table.

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

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 277dbe8f1d0361eafdbebff1a34270bd7ef27799..a6aa89e8190cb62a2a0414241d113d21bbdecf5b 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -186,8 +186,11 @@ 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
@@ -511,6 +514,11 @@ 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 =
@@ -595,9 +603,10 @@ object (self)
 
   method nload_sequent metasenv subst metano =
     let sequent = List.assoc metano metasenv in
-    let mathml =
+    let mathml,ids_to_father_ids =
      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
@@ -631,10 +640,9 @@ object (self)
         current_mathml <- Some mathml);
 
   method load_nobject obj =
-    let mathml = ApplyTransformation.nmml_of_cic_object obj in
+    let mathml,ids_to_father_ids = ApplyTransformation.nmml_of_cic_object obj in
+     self#set_ncic_info (Some ids_to_father_ids);
 (*
-    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;