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
let href_ds = Gdome.domString "href"
let xref_ds = Gdome.domString "xref"
-
class clickableMathView obj =
let text_width = 80 in
object (self)
_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
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
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 =
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