diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-26 15:04:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-26 15:04:21 +0200 |
| commit | ec5ef15aae0d6f900eb4a8e6ba61c0952c993eb3 (patch) | |
| tree | effab6623d87f23bcbb65a1fe093f8a8fd4dd429 | |
| parent | c4ffe2b6725a3f8f60763228b77668aa3444f79c (diff) | |
Jump to error line in CoqIDE grabs focus of the textview.
| -rw-r--r-- | ide/session.ml | 1 |
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 |