tab was openened, the interface got confused about which script was focused.
It did not save the previous focused script if it was at end of file and
it saved it instead when switching from the new tab. Other bugs could be related
to that.
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable _only_directory = false
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable _only_directory = false
- val mutable current_page = 0
+ val mutable current_page = -1
initializer
let s () = MatitaScript.current () in
initializer
let s () = MatitaScript.current () in
MatitaMisc.decrease_font_size;
connect_menu_item main#normalFontSizeMenuItem
MatitaMisc.reset_font_size;
MatitaMisc.decrease_font_size;
connect_menu_item main#normalFontSizeMenuItem
MatitaMisc.reset_font_size;
- ignore (main#scriptNotebook#connect#switch_page
- (fun page ->
- let old_script = MatitaScript.at_page current_page in
- save_moo0 ~do_clean:false old_script old_script#status;
- current_page <- page;
- let script = MatitaScript.at_page page in
- script#activate;
- main#saveMenuItem#misc#set_sensitive script#has_name))
+ ignore (main#scriptNotebook#connect#switch_page (fun page ->
+ self#save_page ();
+ current_page <- page;
+ let script = MatitaScript.at_page page in
+ script#activate;
+ main#saveMenuItem#misc#set_sensitive script#has_name))
method private externalEditor () =
let script = MatitaScript.current () in
method private externalEditor () =
let script = MatitaScript.current () in
let script = MatitaScript.at_page page in
self#closeScript page script
let script = MatitaScript.at_page page in
self#closeScript page script
+ method private save_page () =
+ if current_page >= 0 then
+ let old_script = MatitaScript.at_page current_page in
+ save_moo0 ~do_clean:false old_script old_script#status
+
let scrolledWindow = GBin.scrolled_window () in
let hbox = GPack.hbox () in
let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in
let scrolledWindow = GBin.scrolled_window () in
let hbox = GPack.hbox () in
let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in