# 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
+                      }
+                    }
+                }
           }
       }
     }