# HG changeset patch
# User wenzelm
# Date 1400504411 -7200
# Node ID d926fc73b55425b8152dc8b2226c67ea3d4ca69f
# Parent  ebf3c96814062f972163f7e598c5050cee04fed3
re-focus target explicity, e.g. relevant for Sledgehammer panel;

diff -r ebf3c9681406 -r d926fc73b554 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)