1. MatitaGuiTypes.gui interface streamlined

2. added new menu item to close a script
3. restored graying of "Save" menu item when the script is unnamed

diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade
index a49c5539d29e6e69f3f95f266697d00e0e8261ea..28a5e609f44a920e49cc9ca805d00ecb567a9688 100644 (file)
--- a/matita/matita/matita.glade
+++ b/matita/matita/matita.glade
@@ -1,6 +1,6 @@
 <?xml version="1.0"?>
 <glade-interface>
-  <!-- interface-requires gtk+ 2.6 -->
+  <!-- interface-requires gtk+ 2.16 -->
   <!-- interface-naming-policy toplevel-contextual -->
   <widget class="GtkWindow" id="BrowserWin">
     <property name="width_request">500</property>
@@ -693,6 +693,15 @@
                                 <property name="visible">True</property>
                               </widget>
                             </child>
+                            <child>
+                              <widget class="GtkImageMenuItem" id="closeMenuItem">
+                                <property name="label">gtk-close</property>
+                                <property name="visible">True</property>
+                                <property name="use_underline">True</property>
+                                <property name="use_stock">True</property>
+                                <accelerator key="q" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                              </widget>
+                            </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="quitMenuItem">
                                 <property name="label">gtk-quit</property>

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 680dec8e612850447ca1f179bb1e9a48dd6c19d3..9b32cf0b57984dcf4323bdfbcd772fd9fe79d2c3 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -792,26 +792,6 @@ class gui () =
               can we do? *)
            notify_exn (MatitaScript.current ())#source_view exn
           else raise exn);
-      let disableSave () =
-        (s())#assignFileName None;
-        main#saveMenuItem#misc#set_sensitive false
-      in
-      let 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 -> ()
-      in
-      let saveScript script =
-        if script#has_name then 
-          (script#saveToFile (); 
-           console#message ("'"^script#filename^"' saved.\n"))
-        else saveAsScript script
-      in
       let loadScript () =
         try 
           match self#chooseFile () with
@@ -839,17 +819,8 @@ class gui () =
         MatitaScript.iter_scripts
          (fun script ->
            if not !cancel then
-            if script#source_view#buffer#modified then
-              match
-               ask_unsaved main#toplevel (Filename.basename script#filename)
-              with
-              | `YES -> 
-                   saveScript script;
-                   save_moo script#grafite_status
-              | `NO -> ()
-              | `CANCEL -> cancel := true
-            else 
-              save_moo script#grafite_status);
+            if not (self#closeScript0 script) then
+             cancel := true);
         if not !cancel then
          GMain.Main.quit ());
       connect_button main#scriptAdvanceButton advance;
@@ -865,10 +836,11 @@ class gui () =
       connect_menu_item main#scriptJumpMenuItem jump;
       connect_menu_item main#openMenuItem   loadScript;
       connect_menu_item main#saveMenuItem 
-       (fun () -> saveScript (MatitaScript.current ()));
+       (fun () -> self#saveScript (MatitaScript.current ()));
       connect_menu_item main#saveAsMenuItem
-       (fun () -> saveAsScript (MatitaScript.current ()));
-      connect_menu_item main#newMenuItem    self#newScript;
+       (fun () -> self#saveAsScript (MatitaScript.current ()));
+      connect_menu_item main#newMenuItem self#newScript;
+      connect_menu_item main#closeMenuItem self#closeScript;
       connect_menu_item main#showCoercionsGraphMenuItem 
         (fun _ -> 
           let c = MatitaMathView.cicBrowser () in
@@ -915,7 +887,10 @@ class gui () =
       connect_menu_item main#normalFontSizeMenuItem
         MatitaMisc.reset_font_size;
       ignore (main#scriptNotebook#connect#switch_page
-       (fun page -> (MatitaScript.at_page page)#activate));
+       (fun 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
@@ -974,6 +949,46 @@ class gui () =
       | Exit -> ()
       | Invalid_argument _ -> script#goto `Bottom ()
 
+    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#grafite_status;
+             true
+        | `NO -> true
+        | `CANCEL -> false
+      else 
+       (save_moo script#grafite_status; true)
+
+    method private closeScript () = 
+     let page = main#scriptNotebook#current_page in
+     let script = MatitaScript.at_page page in 
+     if self#closeScript0 script then
+      begin
+       MatitaScript.destroy page;
+       ignore (main#scriptNotebook#remove_page page)
+      end
+
     method newScript () = 
        let scrolledWindow = GBin.scrolled_window () in
        let tab_label = GMisc.label ~text:"foo" () in
@@ -1037,9 +1052,9 @@ class gui () =
     method private _enableSaveTo file =
       self#main#saveMenuItem#misc#set_sensitive true
         
-    method console = console
-    method fileSel = fileSel
-    method findRepl = findRepl
+    method private console = console
+    method private fileSel = fileSel
+    method private findRepl = findRepl
     method main = main
 
     method newBrowserWin () =
@@ -1059,7 +1074,7 @@ class gui () =
       dialog#check_widgets ();
       dialog
 
-    method newConfirmationDialog () =
+    method private newConfirmationDialog () =
       let dialog = new confirmationDialog () in
       dialog#check_widgets ();
       dialog
@@ -1073,13 +1088,13 @@ class gui () =
       List.iter (fun evbox -> add_key_binding key callback evbox)
         keyBindingBoxes
 
-    method setQuitCallback callback =
+    method private setQuitCallback callback =
       connect_menu_item main#quitMenuItem callback;
       ignore (main#toplevel#event#connect#delete 
         (fun _ -> callback ();true));
       self#addKeyBinding GdkKeysyms._q callback
 
-    method chooseFile ?(ok_not_exists = false) () =
+    method private chooseFile ?(ok_not_exists = false) () =
       _ok_not_exists <- ok_not_exists;
       _only_directory <- false;
       fileSel#fileSelectionWin#show ();
@@ -1094,25 +1109,6 @@ class gui () =
       (* we should check that this is a directory *)
       chosen_file
   
-    method askText ?(title = "") ?(msg = "") () =
-      let dialog = new textDialog () in
-      dialog#textDialog#set_title title;
-      dialog#textDialogLabel#set_label msg;
-      let text = ref None in
-      let return v =
-        text := v;
-        dialog#textDialog#destroy ();
-        GMain.Main.quit ()
-      in
-      ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
-      connect_button dialog#textDialogCancelButton (fun _ -> return None);
-      connect_button dialog#textDialogOkButton (fun _ ->
-        let text = dialog#textDialogTextView#buffer#get_text () in
-        return (Some text));
-      dialog#textDialog#show ();
-      GtkThread.main ();
-      !text
-
   end
 
 let gui () = 

diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli
index fa62970cef6c0835a74561ff0fcf23e59d02955e..2c685c0ad4cfd9c51268a5bfade524383ab60368 100644 (file)
--- a/matita/matita/matitaGuiTypes.mli
+++ b/matita/matita/matitaGuiTypes.mli
@@ -42,15 +42,8 @@ end
 
 class type gui =
 object
-  method setQuitCallback    : (unit -> unit) -> unit
-
     (** {2 Access to singleton instances of lower-level GTK widgets} *)
-
-  method fileSel :      MatitaGeneratedGui.fileSelectionWin
   method main :         MatitaGeneratedGui.mainWin
-  method findRepl :     MatitaGeneratedGui.findReplWin
-
-  method console:       console
 
     (** {2 Dialogs instantiation}
      * methods below create a new window on each invocation. You should
@@ -58,19 +51,10 @@ object
 
   method newBrowserWin:         unit -> browserWin
   method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
-  method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
   method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
 
     (** {2 Utility methods} *)
 
-    (** ask the used to choose a file with the file chooser
-    * @param ok_not_exists if set to true returns also non existent files
-    * (useful for save). Defaults to false *)
-  method chooseFile: ?ok_not_exists:bool -> unit -> string option
-
-    (** prompt the user for a (multiline) text entry *)
-  method askText: ?title:string -> ?msg:string -> unit -> string option
-
   method newScript: unit -> unit
   method loadScript: string -> unit
 end

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 6528eab9a9cbcb4d7446087dd7a02cd7aa538a75..0f7789a89d6fd2655e51a61a582100b0ac06be7c 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -1036,6 +1036,11 @@ let at_page page =
 let current () =
  at_page ((MatitaMisc.get_gui ())#main#scriptNotebook#current_page)
 
+let destroy page =
+ let s = at_page page in
+  _script := List.filter ((<>) s) !_script
+;;
+
 let iter_scripts f = List.iter f !_script;;
 
 let _ =

diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli
index add51ccf02eb6e88060fd848b5b79b1d42ef9794..81ade1c88c34ec0e8a87bfef61920ad0d3b128bb 100644 (file)
--- a/matita/matita/matitaScript.mli
+++ b/matita/matita/matitaScript.mli
@@ -109,6 +109,7 @@ val script:
   unit -> 
     script
 
+val destroy: int -> unit
 val current: unit -> script
 val at_page: int -> script
 val iter_scripts: (script -> unit) -> unit