reactivated ListCellRenderer for Java 6 (cf. b9e2ed4b1579, 0ddac15782e4, de249b5ae6e2);
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 25 15:13:03 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 25 15:13:40 2012 +0200
@@ -105,14 +105,12 @@
if (ds.isEmpty) null
else
new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) {
- /* FIXME Java 7 only
override def getRenderer() =
- new ListCellRenderer[Any] {
- val default_renderer =
- (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]]
+ new ListCellRenderer {
+ val default_renderer = new DefaultListCellRenderer
override def getListCellRendererComponent(
- list: JList[_ <: Any], value: Any, index: Int,
+ list: JList, value: Any, index: Int,
selected: Boolean, focus: Boolean): Component =
{
val renderer: Component =
@@ -122,7 +120,6 @@
renderer
}
}
- */
}
}
}