Code simplification.

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 5f0c77df5f9bfe70d322b4d0012a29bb7ef897fc..07233700a29f15ae43da3e8f223f3652a18c39b4 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -45,6 +45,12 @@ object (self)
 end
 
 let cicBrowsers = ref []
+let gui_instance = ref None
+let set_gui gui = gui_instance := Some gui
+let get_gui () =
+  match !gui_instance with
+  | None -> assert false
+  | Some gui -> gui
 
 let default_font_size () =
   Helm_registry.get_opt_default Helm_registry.int
@@ -64,7 +70,6 @@ let near (x1, y1) (x2, y2) =
 let href_ds = Gdome.domString "href"
 let xref_ds = Gdome.domString "xref"
 
-
 class clickableMathView obj =
   let text_width = 80 in
   object (self)
@@ -311,7 +316,6 @@ class sequentsViewer ~(notebook:GPack.notebook)
       _metasenv <- metasenv;
       pages <- sequents_no;
       self#script#setGoal goal;
-      let parentref = ref None in
       let win metano =
         let w =
           GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
@@ -320,13 +324,15 @@ class sequentsViewer ~(notebook:GPack.notebook)
         let reparent () =
           scrolledWin <- Some w;
           match sequentViewer#misc#parent with
-          | None -> w#add sequentViewer#coerce; parentref := Some w
+          | None -> w#add sequentViewer#coerce
           | Some parent ->
              let parent =
-              match !parentref with None -> assert false | Some p -> p in
-             parent#remove sequentViewer#coerce;
-             w#add sequentViewer#coerce;
-             parentref := Some w;
+              match sequentViewer#misc#parent with
+                 None -> assert false
+               | Some p -> GContainer.cast_container p
+             in
+              parent#remove sequentViewer#coerce;
+              w#add sequentViewer#coerce
         in
         goal2win <- (metano, reparent) :: goal2win;
         w#coerce
@@ -427,8 +433,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
-  let gui = MatitaGui.instance () in
-  let win = gui#newBrowserWin () in
+  let gui = get_gui () in
+  let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
   let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
   let combo,_ = GEdit.combo_box_text ~strings:queries () in
   let activate_combo_query input q =
@@ -748,7 +754,7 @@ let default_sequentViewer () = sequentViewer ~show:true ()
 let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer
 
 let default_sequentsViewer () =
-  let gui = MatitaGui.instance () in
+  let gui = get_gui () in
   let sequentViewer = sequentViewer_instance () in
   sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer ()
 let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer