--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Thu Apr 07 23:25:09 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Fri Apr 08 11:39:45 2011 +0200
@@ -112,7 +112,7 @@
val tooltip: Markup_Tree.Select[String] =
{
- case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + name
+ case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
margin = Isabelle.Int_Property("tooltip-margin"))