+ method private saveAsScript script =
+ match self#chooseFile ~ok_not_exists:true () with
+ | Some f ->
+ HExtlib.touch f;
+ script#assignFileName (Some f);
+ script#saveToFile ();
+ console#message ("'"^f^"' saved.\n");
+ self#_enableSaveTo f
+ | None -> ()
+
+ method private saveScript script =
+ if script#has_name then
+ (script#saveToFile ();
+ console#message ("'"^script#filename^"' saved.\n"))
+ else self#saveAsScript script
+
+ (* returns false if closure is aborted by the user *)
+ method private closeScript0 script =
+ if script#source_view#buffer#modified then
+ match
+ ask_unsaved main#toplevel (Filename.basename script#filename)
+ with
+ | `YES ->
+ self#saveScript script;
+ save_moo script#status;
+ true
+ | `NO -> true
+ | `CANCEL -> false
+ else
+ (save_moo script#status; true)
+
+ method private closeScript page script =
+ if self#closeScript0 script then
+ begin
+ MatitaScript.destroy page;
+ ignore (main#scriptNotebook#remove_page page)
+ end
+
+ method private closeCurrentScript () =
+ let page = main#scriptNotebook#current_page in
+ 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
+