From 393b5943416585d0612ec62b795ceee34adb8dd7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 9 Feb 2005 15:07:22 +0000 Subject: [PATCH] - fixed "error loading dom error" avoiding sequent_viewer be delivered the destroy signal when resetting the notebook - added singleton instances of sequent_viewer and sequents_viewer --- helm/matita/matitaMathView.ml | 41 +++++++++++++++++++++++++--------- helm/matita/matitaMathView.mli | 6 ++++- 2 files changed, 35 insertions(+), 12 deletions(-) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index cde097e9a..7aa54f2c7 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -139,29 +139,30 @@ class sequent_viewer obj = selections method load_sequent metasenv metano = -(* - let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, - ids_to_hypotheses) = - Cic2acic.asequent_of_sequent metasenv conjecture - in -*) let sequent = CicUtil.lookup_meta metano metasenv in let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) = ApplyTransformation.mml_of_cic_sequent metasenv sequent in current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); +(* debug_print "load_sequent: dumping MathML to ./prova"; ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); +*) self#load_root ~root:mathml#get_documentElement end class sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:sequent_viewer) ~set_goal () + ~(sequent_viewer:sequent_viewer) () = let tab_label metano = (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce in + let set_goal goal = + let currentProof = MatitaProof.instance () in + assert (currentProof#onGoing ()); + currentProof#proof#set_goal goal + in object (self) val mutable pages = 0 val mutable switch_page_callback = None @@ -169,8 +170,17 @@ class sequents_viewer ~(notebook:GPack.notebook) val mutable goal2page = [] (* the other way round *) 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 sequent_viewer is currently attached *) method reset = + (match scrolledWin with + | Some w -> + (* removing page from the notebook will destroy all contained widget, + * we do not want the sequent_viewer to be destroyed as well *) + w#remove sequent_viewer#coerce; + scrolledWin <- None + | None -> ()); for i = 1 to pages do notebook#remove_page 0 done; pages <- 0; page2goal <- []; @@ -193,6 +203,7 @@ class sequents_viewer ~(notebook:GPack.notebook) ~shadow_type:`IN ~show:true () in let reparent () = + scrolledWin <- Some w; match sequent_viewer#misc#parent with | None -> w#add sequent_viewer#coerce | Some _ -> sequent_viewer#misc#reparent w#coerce @@ -232,7 +243,7 @@ class sequents_viewer ~(notebook:GPack.notebook) with Not_found -> assert false in notebook#goto_page page; - self#render_page page goal; + self#render_page page goal end @@ -453,9 +464,9 @@ class cicBrowser ~(history:string MatitaMisc.history) () = end let sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:sequent_viewer) ~set_goal () + ~(sequent_viewer:sequent_viewer) () = - new sequents_viewer ~notebook ~sequent_viewer ~set_goal () + new sequents_viewer ~notebook ~sequent_viewer () let cicBrowser () = let size = BuildTimeConf.browser_history_size in @@ -488,5 +499,13 @@ class mathViewer = end let mathViewer () = new mathViewer -let instance = MatitaMisc.singleton mathViewer + +let default_sequent_viewer () = sequent_viewer ~show:true () +let sequent_viewer_instance = MatitaMisc.singleton default_sequent_viewer + +let default_sequents_viewer () = + let gui = MatitaGui.instance () in + let sequent_viewer = sequent_viewer_instance () in + sequents_viewer ~notebook:gui#main#sequentsNotebook ~sequent_viewer () +let sequents_viewer_instance = MatitaMisc.singleton default_sequents_viewer diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 2c27704d2..0a1e425e3 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -79,7 +79,6 @@ val sequent_viewer: sequent_viewer constructor val sequents_viewer: notebook:GPack.notebook -> sequent_viewer:sequent_viewer -> - set_goal:(int -> unit) -> unit -> sequents_viewer @@ -89,3 +88,8 @@ val refresh_all_browsers: unit -> unit val mathViewer: unit -> MatitaTypes.mathViewer +(** {2 singleton instances} *) + +val sequent_viewer_instance: unit -> sequent_viewer +val sequents_viewer_instance: unit -> sequents_viewer + -- 2.39.2