re-focus target explicity, e.g. relevant for Sledgehammer panel;
authorwenzelm
Mon May 19 15:00:11 2014 +0200 (2014-05-19)
changeset 56999d926fc73b554
parent 56998 ebf3c9681406
child 57000 c914618feef8
re-focus target explicity, e.g. relevant for Sledgehammer panel;
src/Tools/jEdit/src/active.scala
     1.1 --- a/src/Tools/jEdit/src/active.scala	Mon May 19 14:48:50 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/active.scala	Mon May 19 15:00:11 2014 +0200
     1.3 @@ -58,6 +58,7 @@
     1.4                        Isabelle.insert_line_padding(text_area, text)
     1.5                      else text_area.setSelectedText(text)
     1.6                  }
     1.7 +                text_area.requestFocus
     1.8  
     1.9                case Simplifier_Trace.Active(serial, answer) =>
    1.10                  Simplifier_Trace.send_reply(PIDE.session, serial, answer)