--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Sep 01 15:15:29 2017 +0200
@@ -340,15 +340,6 @@
/* key event handling */
- def request_focus_view(alt_view: View = null)
- {
- val view = if (alt_view != null) alt_view else jEdit.getActiveView()
- if (view != null) {
- val text_area = view.getTextArea
- if (text_area != null) text_area.requestFocus
- }
- }
-
def propagate_key(view: View, evt: KeyEvent)
{
if (view != null && !evt.isConsumed)