]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaMathView.ml
refactored gui handling code so that MatitaMathView is linked before MatitaGui
[helm.git] / helm / matita / matitaMathView.ml
index 5f0c77df5f9bfe70d322b4d0012a29bb7ef897fc..3b9d0282319cafa3d955aba9dffe90f9f3351b7c 100644 (file)
@@ -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)
@@ -427,8 +432,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 +753,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