Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50724
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
     1
 
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
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
     2
 
--- 5.0.0/jEdit/org/gjt/sp/jedit/gui/CompletionPopup.java	2012-11-17 16:41:58.000000000 +0100
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
     3
 
+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/CompletionPopup.java	2013-01-04 14:25:57.095172180 +0100
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
     4
 
@@ -113,9 +113,9 @@
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
     5
 
 		list.setCellRenderer(new CellRenderer());
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
     6
 
 		list.addKeyListener(keyHandler);
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
     7
 
 		list.addMouseListener(new MouseHandler());
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
     8
 
+		list.setFocusTraversalKeysEnabled(false);
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
     9
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
    10
 
 		JPanel content = new JPanel(new BorderLayout());
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
    11
 
-		content.setFocusTraversalKeysEnabled(false);
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
    12
 
 		// stupid scrollbar policy is an attempt to work around
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
    13
 
 		// bugs people have been seeing with IBM's JDK -- 7 Sep 2000
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
    14
 
 		JScrollPane scroller = new JScrollPane(list,
bf5cc2a06e87 support TAB in completion: need to configure the component with the key handler;
wenzelm
parents:
diff changeset 
    15
 














isabelle