aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-05-26 15:04:21 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-05-26 15:04:21 +0200
commitec5ef15aae0d6f900eb4a8e6ba61c0952c993eb3 (patch)
treeeffab6623d87f23bcbb65a1fe093f8a8fd4dd429
parentc4ffe2b6725a3f8f60763228b77668aa3444f79c (diff)
Jump to error line in CoqIDE grabs focus of the textview.
-rw-r--r--ide/session.ml1
1 files changed, 1 insertions, 0 deletions
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