display Java 7 only code for now (cf. b9e2ed4b1579);
authorwenzelm
Thu, 19 Apr 2012 23:15:58 +0200
changeset 47591 0ddac15782e4
parent 47590 8bdfacbc2fa2
child 47617 f5eaa7fa8d72
display Java 7 only code for now (cf. b9e2ed4b1579);
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
                       }
                     }
+                  */
                 }
           }
       }