From c44be86afb9b9811e59ebdd0fc5819e029b66207 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 29 Jul 2005 09:00:32 +0000
Subject: [PATCH] Partial bug fix: every inner type is now added to the
 selection roots. However, the inner types are not closed terms! They live in
 the context of their terms. Right now there is a bug in locating subterms of
 a proof. Thus I do not even try to fix inner types selection properly.

---
 helm/matita/matitaMathView.ml | 32 ++++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 481b8fd6c..f57364d5f 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -75,7 +75,7 @@ let href_ds = Gdome.domString "href"
 let xref_ds = Gdome.domString "xref"
 
 (* ids_to_terms should not be passed here, is just for debugging *)
-let find_root_id annobj id ids_to_father_ids ids_to_terms =
+let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types =
   let find_parent id ids =
     let rec aux id =
 (*       (prerr_endline (sprintf "id %s = %s" id
@@ -98,13 +98,20 @@ let find_root_id annobj id ids_to_father_ids ids_to_terms =
     | Some parent_id -> parent_id
   in
   let mk_ids terms = List.map CicUtil.id_of_annterm terms in
+  let inner_types =
+   Hashtbl.fold
+    (fun _ types acc ->
+      match types.Cic2acic.annexpected with
+         None -> types.Cic2acic.annsynthesized :: acc
+       | Some ty -> ty :: types.Cic2acic.annsynthesized :: acc
+    ) ids_to_inner_types [] in
   match annobj with
   | Cic.AConstant (_, _, _, Some bo, ty, _, _)
   | Cic.AVariable (_, _, Some bo, ty, _, _)
   | Cic.ACurrentProof (_, _, _, _, bo, ty, _, _) ->
-      return_father id (mk_ids [ty; bo])
+      return_father id (mk_ids (ty :: bo :: inner_types))
   | Cic.AConstant (_, _, _, None, ty, _, _)
-  | Cic.AVariable (_, _, None, ty, _, _) -> return_father id (mk_ids [ty])
+  | Cic.AVariable (_, _, None, ty, _, _) -> return_father id (mk_ids (ty::inner_types))
   | Cic.AInductiveDefinition _ ->
       assert false  (* TODO *)
 
@@ -244,7 +251,7 @@ object (self)
   method update_font_size = self#set_font_size !current_font_size
 
   method private get_term_by_id context cic_info id =
-    let ids_to_terms, ids_to_hypotheses, _, _ = cic_info in
+    let ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in
     try
       `Term (Hashtbl.find ids_to_terms id)
     with Not_found ->
@@ -257,10 +264,12 @@ object (self)
   method private find_obj_conclusion id =
     match self#cic_info with
     | None
-    | Some (_, _, _, None) -> assert false
-    | Some (ids_to_terms, _, ids_to_father_ids, Some annobj) ->
-        let id = find_root_id annobj id ids_to_father_ids ids_to_terms in
-        (try Hashtbl.find ids_to_terms id with Not_found -> assert false)
+    | Some (_, _, _, _, None) -> assert false
+    | Some (ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) ->
+        let id =
+         find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types
+        in
+         (try Hashtbl.find ids_to_terms id with Not_found -> assert false)
 
   method private string_of_node node =
     let get_id (node: Gdome.element) =
@@ -349,7 +358,7 @@ object (self)
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
     self#set_cic_info
-      (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, None));
+      (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None));
     let name = "sequent_viewer.xml" in
     MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name);
     ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
@@ -358,12 +367,12 @@ object (self)
   method load_object obj =
     let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
     let (mathml,
-      (annobj, (ids_to_terms, ids_to_father_ids, _, ids_to_hypotheses, _, _)))
+      (annobj, (ids_to_terms, ids_to_father_ids, _, ids_to_hypotheses, _, ids_to_inner_types)))
     =
       ApplyTransformation.mml_of_cic_object obj
     in
     self#set_cic_info
-      (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Some annobj));
+      (Some (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;
@@ -621,7 +630,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       toplevel#show ()
 
     val mutable current_entry = `About `Blank 
-    val mutable current_infos = None
 
     val model =
       new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
-- 
2.39.2