From ec5ef15aae0d6f900eb4a8e6ba61c0952c993eb3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 26 May 2015 15:04:21 +0200
Subject: Jump to error line in CoqIDE grabs focus of the textview.

---
 ide/session.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'ide/session.ml')

diff --git a/ide/session.ml b/ide/session.ml
index cfcc592ef..fd8f80690 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -296,6 +296,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
         let lno = store#get ~row ~column:(find_int_col "Line" columns) in
         let where = script#buffer#get_iter (`LINE (lno-1)) in
         script#buffer#place_cursor ~where;
+        script#misc#grab_focus ();
         ignore (script#scroll_to_iter
 		  ~use_align:false ~yalign:0.75 ~within_margin:0.25 where)) in
   let tip = GMisc.label ~text:"Double click to jump to error line" () in
-- 
cgit v1.2.3