From c44be86afb9b9811e59ebdd0fc5819e029b66207 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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