# HG changeset patch
# User wenzelm
# Date 1281563198 -7200
# Node ID 715f39fd752d85bd3d8e8a5eb7d7ef77a74d27b8
# Parent  443fb83a21e8d8535f0c357503924f48335b6a60
Document.print_id;

diff -r 443fb83a21e8 -r 715f39fd752d src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Aug 11 23:29:17 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Aug 11 23:46:38 2010 +0200
@@ -139,7 +139,7 @@
               override def getIcon: Icon = null
               override def getShortString: String = content
               override def getLongString: String = node.info.toString
-              override def getName: String = id
+              override def getName: String = Document.print_id(id)
               override def setName(name: String) = ()
               override def setStart(start: Position) = ()
               override def getStart: Position = command_start + node.start