+ 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 newScript () =
+ let scrolledWindow = GBin.scrolled_window () in
+ let hbox = GPack.hbox () in
+ let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in
+ let _ =
+ GMisc.label ~text:"" ~packing:(hbox#pack ~expand:true ~fill:true) () in
+ let closebutton =
+ GButton.button ~relief:`NONE ~packing:hbox#pack () in
+ let image = GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in
+ closebutton#set_image image#coerce;
+ let script = MatitaScript.script ~parent:scrolledWindow ~tab_label () in
+ ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce
+ scrolledWindow#coerce);
+ ignore (closebutton#connect#clicked (fun () ->
+ self#closeScript
+ (main#scriptNotebook#page_num scrolledWindow#coerce) script));
+ main#scriptNotebook#goto_page 0;
+ sequents_viewer#reset;
+ sequents_viewer#load_logo;
+ let browser_observer _ = MatitaMathView.refresh_all_browsers () in
+ let sequents_observer status =
+ sequents_viewer#reset;
+ match status#ng_mode with
+ `ProofMode ->
+ sequents_viewer#nload_sequents status;
+ (try
+ let goal =
+ Continuationals.Stack.find_goal status#stack
+ in
+ sequents_viewer#goto_sequent status goal
+ with Failure _ -> ());
+ | `CommandMode -> sequents_viewer#load_logo
+ in
+ script#addObserver sequents_observer;
+ script#addObserver browser_observer
+