# HG changeset patch # User wenzelm # Date 1380392653 -7200 # Node ID 78bbe75c8437ff8bc474dde7993714ada998af27 # Parent c6297fa1031aac101dc943502aa77731b330c531 enforce IsabelleText font for better symbol coverage, especially on Windows; diff -r c6297fa1031a -r 78bbe75c8437 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Sep 28 16:36:17 2013 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Sep 28 20:24:13 2013 +0200 @@ -29,7 +29,8 @@ protected var _start = int_to_pos(start) protected var _end = int_to_pos(end) override def getIcon: Icon = null - override def getShortString: String = _name + override def getShortString: String = + "" + HTML.encode(_name) + "" override def getLongString: String = _name override def getName: String = _name override def setName(name: String) = _name = name