let all_disambiguation_passes = ref false
-let gui_instance = ref None
-
(* this is a shit and should be changed :-{ *)
let interactive_uri_choice
?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
let script = MatitaScript.at_page page in
script#activate;
main#saveMenuItem#misc#set_sensitive script#has_name));
+ self#newScript ()
method private externalEditor () =
let script = MatitaScript.current () in
let script = MatitaScript.at_page page in
self#closeScript page script
- method newScript () =
+ method private newScript () =
let scrolledWindow = GBin.scrolled_window () in
let hbox = GPack.hbox () in
let tab_label = GMisc.label ~text:"foo"
let gui () =
let g = new gui () in
- gui_instance := Some g;
MatitaMisc.set_gui g;
g