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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 066d07cc5..733d0aab9 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -374,8 +374,13 @@ class gui () =
       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 
@@ -631,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;