From: Stefano Zacchiroli Date: Thu, 28 Jul 2005 17:00:00 +0000 (+0000) Subject: - re-factoring: dropped sequentViewer in favour of cicMathView which X-Git-Tag: V_0_7_2~8 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39736960d48b9a19f3b7ca6e4d852a9dbcd4af76;p=helm.git - re-factoring: dropped sequentViewer in favour of cicMathView which handles rendering of both sequents and objects - added preliminary support for selection in cicBrowser (there are still issues with phisical equality and multiple xrefs ...) --- diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 69bee68a5..610f22a4e 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -80,9 +80,9 @@ let script = (* math viewers *) let _ = - let sequent_viewer = MatitaMathView.sequentViewer_instance () in + let cic_math_view = MatitaMathView.cicMathView_instance () in let sequents_viewer = MatitaMathView.sequentsViewer_instance () in - sequent_viewer#set_href_callback + cic_math_view#set_href_callback (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri (UriManager.uri_of_string uri)))); let browser_observer _ = MatitaMathView.refresh_all_browsers () in @@ -130,8 +130,8 @@ let _ = prerr_endline (UriManager.string_of_uri u)) (CicEnvironment.list_obj ())); addDebugItem "print selections" (fun () -> - let sequentViewer = MatitaMathView.sequentViewer_instance () in - List.iter MatitaLog.debug (sequentViewer#string_of_selections)); + let cicMathView = MatitaMathView.cicMathView_instance () in + List.iter MatitaLog.debug (cicMathView#string_of_selections)); addDebugItem "dump getter settings" (fun _ -> prerr_endline (Http_getter_env.env_to_string ())); addDebugItem "getter: getalluris" (fun _ -> diff --git a/helm/matita/matitaGuiTypes.mli b/helm/matita/matitaGuiTypes.mli index 14bfee4f4..d9c2ece2a 100644 --- a/helm/matita/matitaGuiTypes.mli +++ b/helm/matita/matitaGuiTypes.mli @@ -102,12 +102,14 @@ object method update_font_size: unit end -class type sequentViewer = +class type cicMathView = object inherit clickableMathView (** load a sequent and render it into parent widget *) method load_sequent: Cic.metasenv -> int -> unit + + method load_object: Cic.obj -> unit end class type sequentsViewer = diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 3cb9c8c0b..ca82df075 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -74,6 +74,40 @@ let near (x1, y1) (x2, y2) = 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_parent id ids = + let rec aux id = +(* (prerr_endline (sprintf "id %s = %s" id + (try + CicPp.ppterm (Hashtbl.find ids_to_terms id) + with Not_found -> "NONE"))); *) + if List.mem id ids then Some id + else + (match + (try Hashtbl.find ids_to_father_ids id with Not_found -> None) + with + | None -> None + | Some id' -> aux id') + in + aux id + in + let return_father id ids = + match find_parent id ids with + | None -> assert false + | Some parent_id -> parent_id + in + let mk_ids terms = List.map CicUtil.id_of_annterm terms 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]) + | Cic.AConstant (_, _, _, None, ty, _, _) + | Cic.AVariable (_, _, None, ty, _, _) -> return_father id (mk_ids [ty]) + | Cic.AInductiveDefinition _ -> + assert false (* TODO *) + class clickableMathView obj = let text_width = 80 in object (self) @@ -84,10 +118,7 @@ object (self) val mutable _cic_info = None method private set_cic_info info = _cic_info <- info - method private cic_info = - match _cic_info with - | Some info -> info - | None -> assert false + method private cic_info = _cic_info initializer self#set_font_size !current_font_size; @@ -102,15 +133,18 @@ object (self) val mutable selection_changed = false method private selection_get_cb ctxt ~info ~time = +(* prerr_endline "selection_get_cb"; *) (match self#get_selections with | [] -> () | node :: _ -> ctxt#return (self#string_of_node node)) method private selection_clear_cb sel_event = +(* prerr_endline "selection_clear_cb"; *) self#remove_selections; false method private button_press_cb gdk_button = +(* prerr_endline "button_press_cb"; *) let button = GdkEvent.Button.button gdk_button in if button = left_button then begin button_press_x <- GdkEvent.Button.x gdk_button; @@ -121,6 +155,7 @@ object (self) false method private popup_contextual_menu time = +(* prerr_endline "popup_contextual_menu"; *) match self#string_of_selection with | None -> () | Some s -> @@ -208,8 +243,8 @@ object (self) method update_font_size = self#set_font_size !current_font_size - method private get_term_by_id context id = - let ids_to_terms, ids_to_hypotheses = self#cic_info in + method private get_term_by_id context cic_info id = + let ids_to_terms, ids_to_hypotheses, _, _ = cic_info in try `Term (Hashtbl.find ids_to_terms id) with Not_found -> @@ -219,6 +254,14 @@ object (self) `Hyp context' with Not_found -> assert false + 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) + method private string_of_node node = let get_id (node: Gdome.element) = let xref_attr = @@ -226,17 +269,25 @@ object (self) in xref_attr#to_string in + let id = get_id node in let script = MatitaScript.instance () in let metasenv = script#proofMetasenv in let context = script#proofContext in - let conclusion = script#proofConclusion in + let metasenv, context, conclusion = + if script#onGoingProof () then + script#proofMetasenv, script#proofContext, script#proofConclusion + else + [], [], + let t = self#find_obj_conclusion id in + MatitaLog.debug (CicPp.ppterm t); + t + in (* TODO: code for patterns let conclusion = (MatitaScript.instance ())#proofConclusion in let conclusion_pattern = ProofEngineHelpers.pattern_of ~term:conclusion cic_terms in *) - let dummy_goal = ~-1 in let string_of_cic_sequent cic_sequent = let acic_sequent, _, _, ids_to_inner_sorts, _ = Cic2acic.asequent_of_sequent metasenv cic_sequent @@ -249,20 +300,22 @@ object (self) let markup = CicNotationPres.render ids_to_uris pped_ast in BoxPp.render_to_string text_width markup in - let term = self#get_term_by_id context (get_id node) in + let cic_info = + match self#cic_info with Some info -> info | None -> assert false + in let cic_sequent = - match term with + match self#get_term_by_id context cic_info id with | `Term t -> let context' = - match - ProofEngineHelpers.locate_in_conjecture t - (dummy_goal, context, conclusion) - with + match + ProofEngineHelpers.locate_in_conjecture t + (~-1, context, conclusion) + with [context,_] -> context | _ -> assert false (* since it uses physical equality *) in - dummy_goal, context', t - | `Hyp context -> dummy_goal, context, Cic.Rel 1 + ~-1, context', t + | `Hyp context -> ~-1, context, Cic.Rel 1 in string_of_cic_sequent cic_sequent @@ -284,25 +337,47 @@ let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = ~font_size:None ~log_verbosity:None)) [] -class sequentViewer obj = +class cicMathView obj = object (self) inherit clickableMathView obj + val mutable current_mathml = None + method load_sequent metasenv metano = let sequent = CicUtil.lookup_meta metano metasenv in - let (mathml, (_, (ids_to_terms, _, ids_to_hypotheses,_ ))) = + let (mathml, (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) = ApplyTransformation.mml_of_cic_sequent metasenv sequent in - self#set_cic_info (Some (ids_to_terms, ids_to_hypotheses)); + self#set_cic_info + (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, None)); let name = "sequent_viewer.xml" in MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name); ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement - end -class sequentsViewer ~(notebook:GPack.notebook) - ~(sequentViewer:sequentViewer) () -= + 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, _, _))) + = + ApplyTransformation.mml_of_cic_object obj + in + self#set_cic_info + (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Some annobj)); + (match current_mathml with + | Some current_mathml when use_diff -> + self#freeze; + XmlDiff.update_dom ~from:current_mathml mathml; + self#thaw + | _ -> + let name = "cic_browser.xml" in + MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name); + ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); + self#load_root ~root:mathml#get_documentElement; + current_mathml <- Some mathml); +end + +class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = object (self) inherit scriptAccessor @@ -313,7 +388,7 @@ class sequentsViewer ~(notebook:GPack.notebook) val mutable goal2win = [] (* associative list: goal no -> scrolled win *) val mutable _metasenv = [] val mutable scrolledWin: GBin.scrolled_window option = None - (* scrolled window to which the sequentViewer is currently attached *) + (* scrolled window to which cicMathView is currently attached *) method private tab_label metano = (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce @@ -322,8 +397,8 @@ class sequentsViewer ~(notebook:GPack.notebook) (match scrolledWin with | Some w -> (* removing page from the notebook will destroy all contained widget, - * we do not want the sequentViewer to be destroyed as well *) - w#remove sequentViewer#coerce; + * we do not want the cicMathView to be destroyed as well *) + w#remove cicMathView#coerce; scrolledWin <- None | None -> ()); for i = 1 to pages do notebook#remove_page 0 done; @@ -352,16 +427,16 @@ class sequentsViewer ~(notebook:GPack.notebook) in let reparent () = scrolledWin <- Some w; - match sequentViewer#misc#parent with - | None -> w#add sequentViewer#coerce + match cicMathView#misc#parent with + | None -> w#add cicMathView#coerce | Some parent -> let parent = - match sequentViewer#misc#parent with + match cicMathView#misc#parent with None -> assert false | Some p -> GContainer.cast_container p in - parent#remove sequentViewer#coerce; - w#add sequentViewer#coerce + parent#remove cicMathView#coerce; + w#add cicMathView#coerce in goal2win <- (metano, reparent) :: goal2win; w#coerce @@ -385,10 +460,10 @@ class sequentsViewer ~(notebook:GPack.notebook) self#render_page ~page ~goal)) method private render_page ~page ~goal = - sequentViewer#load_sequent _metasenv goal; + cicMathView#load_sequent _metasenv goal; try List.assoc goal goal2win (); - sequentViewer#set_selection None + cicMathView#set_selection None with Not_found -> assert false method goto_sequent goal = @@ -416,11 +491,11 @@ type 'widget constructor = unit -> 'widget -let sequentViewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = +let cicMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params - (new sequentViewer (GtkMathViewProps.MathView_GMetaDOM.create p)) + (new cicMathView (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) [] @@ -479,7 +554,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) activate_combo_query arg query in let toplevel = win#toplevel in - let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in + let mathView = cicMathView ~packing:win#scrolledBrowser#add () in let fail message = MatitaGtkMisc.report_error ~title:"Cic browser" ~message ~parent:toplevel () @@ -512,7 +587,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ignore(combo#connect#changed ~callback:start_query); win#whelpBarImage#set_file (MatitaMisc.image_path "whelp.png"); win#mathOrListNotebook#set_show_tabs false; - win#browserForwardButton#misc#set_sensitive false; win#browserBackButton#misc#set_sensitive false; ignore (win#browserUri#entry#connect#activate (handle_error' (fun () -> @@ -543,7 +617,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) val mutable current_entry = `About `Blank val mutable current_infos = None - val mutable current_mathml = None val model = new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview @@ -667,28 +740,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) current_entry <- entry method private _loadObj obj = - self#_showMath; - (* this must be _before_ loading the document, since - * if the widget is not mapped (hidden by the notebook) - * the document is not rendered *) - let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) - let (mathml, (_,((ids_to_terms, ids_to_father_ids, ids_to_conjectures, - ids_to_hypotheses, ids_to_inner_sorts, ids_to_inner_types) as info))) - = - ApplyTransformation.mml_of_cic_object obj - in - current_infos <- Some info; - (match current_mathml with - | Some current_mathml when use_diff -> - mathView#freeze; - XmlDiff.update_dom ~from:current_mathml mathml; - mathView#thaw - | _ -> - let name = "cic_browser.xml" in - MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name); - ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); - mathView#load_root ~root:mathml#get_documentElement; - current_mathml <- Some mathml); + (* showMath must be done _before_ loading the document, since if the + * widget is not mapped (hidden by the notebook) the document is not + * rendered *) + self#_showMath; + mathView#load_object obj method private _loadTermCic term metasenv = let context = self#script#proofContext in @@ -746,10 +802,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) end -let sequentsViewer ~(notebook:GPack.notebook) - ~(sequentViewer:sequentViewer) () -= - new sequentsViewer ~notebook ~sequentViewer () +let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = + new sequentsViewer ~notebook ~cicMathView () let cicBrowser () = let size = BuildTimeConf.browser_history_size in @@ -774,13 +828,13 @@ let cicBrowser () = let history = new MatitaMisc.browser_history size (`About `Blank) in aux history -let default_sequentViewer () = sequentViewer ~show:true () -let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer +let default_cicMathView () = cicMathView ~show:true () +let cicMathView_instance = MatitaMisc.singleton default_cicMathView let default_sequentsViewer () = let gui = get_gui () in - let sequentViewer = sequentViewer_instance () in - sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer () + let cicMathView = cicMathView_instance () in + sequentsViewer ~notebook:gui#main#sequentsNotebook ~cicMathView () let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer let mathViewer () = @@ -803,10 +857,10 @@ let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers let update_font_sizes () = List.iter (fun b -> b#updateFontSize) !cicBrowsers; - (sequentViewer_instance ())#update_font_size + (cicMathView_instance ())#update_font_size let get_math_views () = - ((sequentViewer_instance ()) :> MatitaGuiTypes.clickableMathView) + ((cicMathView_instance ()) :> MatitaGuiTypes.clickableMathView) :: (List.map (fun b -> b#mathView) !cicBrowsers) let get_selections () = diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index f4a724160..f5acf6349 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -40,11 +40,11 @@ type 'widget constructor = val clickableMathView: MatitaGuiTypes.clickableMathView constructor -val sequentViewer: MatitaGuiTypes.sequentViewer constructor +val cicMathView: MatitaGuiTypes.cicMathView constructor val sequentsViewer: notebook:GPack.notebook -> - sequentViewer:MatitaGuiTypes.sequentViewer -> + cicMathView:MatitaGuiTypes.cicMathView -> unit -> MatitaGuiTypes.sequentsViewer @@ -71,7 +71,7 @@ val reset_selections: unit -> unit (** {2 Singleton instances} *) -val sequentViewer_instance: unit -> MatitaGuiTypes.sequentViewer +val cicMathView_instance: unit -> MatitaGuiTypes.cicMathView val sequentsViewer_instance: unit -> MatitaGuiTypes.sequentsViewer val mathViewer: unit -> MatitaTypes.mathViewer