From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Jul 2005 16:27:40 +0000 (+0000)
Subject: After a goto the focus is now grabbed back by the insertion window.
X-Git-Tag: V_0_7_2~138
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=570fd2488f0ba8c16105dc30dd25dd00b558f0fe;p=helm.git

After a goto the focus is now grabbed back by the insertion window.
---

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 0a0239aeb..8d8249765 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -613,7 +613,8 @@ class gui () =
       in
       let cursor () =
         source_buffer#place_cursor
-          (source_buffer#get_iter_at_mark (`NAME "locked"))
+          (source_buffer#get_iter_at_mark (`NAME "locked"));
+        source_view#misc#grab_focus ()
       in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in