X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=733d0aab9699e37a5fd59fb9168a96dc674a10af;hb=db88f09dfd6da59000c93e2ea1ea8565ec8e101d;hp=108b36bfb3f8738ac008a02f65bf1e7207488ef6;hpb=c1902bcdefa7ef7770e470a49fc778f8846cca62;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 108b36bfb..733d0aab9 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -331,6 +331,18 @@ class gui () =
       let clipboard =
        let atom = Gdk.Atom.clipboard in
         GData.clipboard atom in
+      ignore(self#main#editMenu#connect#activate
+        ~callback:
+          (fun () ->
+            let something_selected =
+              (source_buffer#get_iter_at_mark `INSERT)#compare
+              (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+            in
+             self#main#cutMenuItem#misc#set_sensitive something_selected;
+             self#main#copyMenuItem#misc#set_sensitive something_selected;
+             self#main#deleteMenuItem#misc#set_sensitive something_selected;
+             self#main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None)
+          ));
       ignore(self#main#cutMenuItem#connect#activate
         ~callback:(fun () -> source_view#buffer#cut_clipboard clipboard));
       ignore(self#main#copyMenuItem#connect#activate
@@ -341,23 +353,34 @@ class gui () =
           (MatitaScript.instance ())#clean_dirty_lock));
       ignore(self#main#deleteMenuItem#connect#activate
         ~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
+      ignore(self#main#selectAllMenuItem#connect#activate
+        ~callback:(fun () ->
+          source_buffer#move_mark `INSERT source_buffer#start_iter;
+          source_buffer#move_mark `SEL_BOUND source_buffer#end_iter));
       ignore(self#main#findReplMenuItem#connect#activate
         ~callback:show_find_Repl);
       ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
         (* interface lockers *)
       let lock_world _ =
         main#buttonsToolbar#misc#set_sensitive false;
+        develList#buttonsHbox#misc#set_sensitive false;
         source_view#set_editable false
       in
       let unlock_world _ =
         main#buttonsToolbar#misc#set_sensitive true;
+        develList#buttonsHbox#misc#set_sensitive true;
         source_view#set_editable true
       in
       let locker f = 
         fun () -> 
           lock_world ();
-          try f ();unlock_world () with exc -> unlock_world (); raise exc
-      in
+          try f ();unlock_world () with exc -> unlock_world (); raise exc in
+      let keep_focus f =
+        fun () ->
+         try
+          f (); source_view#misc#grab_focus ()
+         with
+          exc -> source_view#misc#grab_focus (); raise exc in
         (* developments win *)
       let model = 
         new MatitaGtkMisc.multiStringListModel 
@@ -374,39 +397,39 @@ class gui () =
         | [[name;_]] -> MatitamakeLib.development_for_name name
         | _ -> assert false 
       in
+      let refresh () = 
+        while Glib.Main.pending () do 
+          ignore(Glib.Main.iteration false); 
+        done
+      in
       connect_button develList#newButton
         (fun () -> 
           next_devel_must_contain <- None;
           newDevel#toplevel#misc#show());
       connect_button develList#deleteButton
-        (fun () -> 
+        (locker (fun () -> 
           (match get_devel_selected () with
           | None -> ()
-          | Some d -> MatitamakeLib.destroy_development d);
-          refresh_devels_win ());
-      let refresh () = 
-        while Glib.Main.pending () do 
-          ignore(Glib.Main.iteration false); 
-        done
-      in
+          | Some d -> MatitamakeLib.destroy_development_in_bg refresh d);
+          refresh_devels_win ()));
       connect_button develList#buildButton 
-        (fun () -> 
+        (locker (fun () -> 
           match get_devel_selected () with
           | None -> ()
           | Some d -> 
               let build = locker 
                 (fun () -> MatitamakeLib.build_development_in_bg refresh d)
               in
-              ignore(build ()));
+              ignore(build ())));
       connect_button develList#cleanButton 
-        (fun () -> 
+        (locker (fun () -> 
           match get_devel_selected () with
           | None -> ()
           | Some d -> 
               let clean = locker 
                 (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
               in
-              ignore(clean ()));
+              ignore(clean ())));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
@@ -524,7 +547,7 @@ class gui () =
         (tac_w_term (A.Transitivity (loc, hole)));
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
-      connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
+      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None))); (* ALB *)
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
        ~check:self#main#tacticsBarMenuItem;
@@ -613,19 +636,17 @@ class gui () =
       in
       let cursor () =
         source_buffer#place_cursor
-          (source_buffer#get_iter_at_mark (`NAME "locked"));
-        source_view#misc#grab_focus ()
-      in
+          (source_buffer#get_iter_at_mark (`NAME "locked")) in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
-      let advance = locker advance in
-      let retract = locker retract in
-      let top = locker top in
-      let bottom = locker bottom in
-      let jump = locker jump in
+      let advance = locker (keep_focus advance) in
+      let retract = locker (keep_focus retract) in
+      let top = locker (keep_focus top) in
+      let bottom = locker (keep_focus bottom) in
+      let jump = locker (keep_focus jump) in
       let connect_key sym f =
         connect_key self#main#mainWinEventBox#event
           ~modifiers:[`CONTROL] ~stop:true sym f;