# HG changeset patch # User wenzelm # Date 1399575785 -7200 # Node ID 7b65f4da136dded1ce661b89b68c364f64d6912a # Parent b00a861d8f1664ce0047893c45f08bca466762ec bounce focus back to main text area -- Output is for output, not query input; diff -r b00a861d8f16 -r 7b65f4da136d src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Thu May 08 19:29:01 2014 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Thu May 08 21:03:05 2014 +0200 @@ -20,6 +20,9 @@ class Output_Dockable(view: View, position: String) extends Dockable(view, position) { + override def focusOnDefaultComponent { view.getTextArea.requestFocus } + + /* component state -- owned by Swing thread */ private var zoom_factor = 100