# HG changeset patch
# User wenzelm
# Date 1334870158 -7200
# Node ID 0ddac15782e4d1f207e3f29f64707944a3dff100
# Parent  8bdfacbc2fa2fe469f4ba6d37d0e9053d62cdbd4
display Java 7 only code for now (cf. b9e2ed4b1579);

diff -r 8bdfacbc2fa2 -r 0ddac15782e4 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Apr 19 21:53:24 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Apr 19 23:15:58 2012 +0200
@@ -105,6 +105,7 @@
               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 =
@@ -121,6 +122,7 @@
                         renderer
                       }
                     }
+                  */
                 }
           }
       }