(* this is a shit and should be changed :-{ *)
let interactive_uri_choice
?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
(* this is a shit and should be changed :-{ *)
let interactive_uri_choice
?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
connect_menu_item main#newMenuItem self#newScript;
connect_menu_item main#closeMenuItem self#closeCurrentScript;
connect_menu_item main#showCoercionsGraphMenuItem
connect_menu_item main#newMenuItem self#newScript;
connect_menu_item main#closeMenuItem self#closeCurrentScript;
connect_menu_item main#showCoercionsGraphMenuItem
main#hpaneScriptSequent#set_position script_w;
(* math view handling *)
connect_menu_item main#newCicBrowserMenuItem (fun () ->
main#hpaneScriptSequent#set_position script_w;
(* math view handling *)
connect_menu_item main#newCicBrowserMenuItem (fun () ->
connect_menu_item main#increaseFontSizeMenuItem
MatitaMisc.increase_font_size;
connect_menu_item main#decreaseFontSizeMenuItem
connect_menu_item main#increaseFontSizeMenuItem
MatitaMisc.increase_font_size;
connect_menu_item main#decreaseFontSizeMenuItem
let scrolledWindow = GBin.scrolled_window () in
let hbox = GPack.hbox () in
let tab_label = GMisc.label ~text:"foo"
let scrolledWindow = GBin.scrolled_window () in
let hbox = GPack.hbox () in
let tab_label = GMisc.label ~text:"foo"