# HG changeset patch # User wenzelm # Date 1334864870 -7200 # Node ID b9e2ed4b15794bfba0310f3fa05f890c30e0ab33 # Parent 1f8f1c2045fdf4b87d87612e01c8aa9ee55ef50f custom ListCellRenderer with text area font ensures that symbols are displayed reliably; diff -r 1f8f1c2045fd -r b9e2ed4b1579 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Apr 19 21:42:24 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Apr 19 21:47:50 2012 +0200 @@ -13,13 +13,15 @@ import scala.collection.Set import scala.collection.immutable.TreeSet +import java.awt.Component import javax.swing.tree.DefaultMutableTreeNode import javax.swing.text.Position -import javax.swing.Icon +import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList} import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} import errorlist.DefaultErrorSource -import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} +import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, + SideKickCompletionPopup, IAsset} object Isabelle_Sidekick @@ -101,8 +103,25 @@ cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word) if (ds.isEmpty) null - else new SideKickCompletion( - pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } + else + new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { + override def getRenderer() = + new ListCellRenderer[Any] { + val default_renderer = + (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]] + + override def getListCellRendererComponent( + list: JList[_ <: Any], value: Any, index: Int, + selected: Boolean, focus: Boolean): Component = + { + val renderer: Component = + default_renderer.getListCellRendererComponent( + list, value, index, selected, focus) + renderer.setFont(pane.getTextArea.getPainter.getFont) + renderer + } + } + } } } }