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