changeset 56917 | 7b65f4da136d |
parent 56907 | 0f3c375fd27c |
child 56918 | a442dc6d244d |
--- 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