From 570fd2488f0ba8c16105dc30dd25dd00b558f0fe Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 20 Jul 2005 16:27:40 +0000 Subject: [PATCH] After a goto the focus is now grabbed back by the insertion window. --- helm/matita/matitaGui.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2