src/Tools/jEdit/patches/jedit/completion
author wenzelm
Mon, 11 Feb 2013 14:39:04 +0100
changeset 51085 d90218288d51
parent 50724 bf5cc2a06e87
permissions -rw-r--r--
make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;

diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/CompletionPopup.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/CompletionPopup.java
--- 5.0.0/jEdit/org/gjt/sp/jedit/gui/CompletionPopup.java	2012-11-17 16:41:58.000000000 +0100
+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/CompletionPopup.java	2013-01-04 14:25:57.095172180 +0100
@@ -113,9 +113,9 @@
 		list.setCellRenderer(new CellRenderer());
 		list.addKeyListener(keyHandler);
 		list.addMouseListener(new MouseHandler());
+		list.setFocusTraversalKeysEnabled(false);
 
 		JPanel content = new JPanel(new BorderLayout());
-		content.setFocusTraversalKeysEnabled(false);
 		// stupid scrollbar policy is an attempt to work around
 		// bugs people have been seeing with IBM's JDK -- 7 Sep 2000
 		JScrollPane scroller = new JScrollPane(list,