- 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))