# HG changeset patch # User wenzelm # Date 1380456467 -7200 # Node ID f6b7afa414f7a308da609fd688ecd5336a7f8c76 # Parent b9139b14c1c5a42f9a9d5f176b8034c8946b713b observe user preferences; diff -r b9139b14c1c5 -r f6b7afa414f7 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Sep 29 13:53:16 2013 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Sep 29 14:07:47 2013 +0200 @@ -30,7 +30,8 @@ protected var _end = int_to_pos(end) override def getIcon: Icon = null override def getShortString: String = - "" + HTML.encode(_name) + "" + "" + + HTML.encode(_name) + "" override def getLongString: String = _name override def getName: String = _name override def setName(name: String) = _name = name