From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 9 Feb 2005 15:07:22 +0000 (+0000)
Subject: - fixed "error loading dom error" avoiding sequent_viewer be delivered
X-Git-Tag: before_svn_merge~16
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=393b5943416585d0612ec62b795ceee34adb8dd7;p=helm.git

- 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
---

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
+