tuned presentation;
authorwenzelm
Fri, 08 Apr 2011 11:39:45 +0200
changeset 42283 25d9d836ed9c
parent 42282 4fa41e068ff0
child 42284 326f57825e1a
tuned presentation;
src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- 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"))