# HG changeset patch
# User wenzelm
# Date 1302255585 -7200
# Node ID 25d9d836ed9c47ed13bf626244b27f8c2d4b37d2
# Parent  4fa41e068ff0e94c2362cb540991f25d0b35c120
tuned presentation;

diff -r 4fa41e068ff0 -r 25d9d836ed9c 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"))