--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Thu Nov 04 10:33:37 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Thu Nov 04 10:58:03 2010 +0100
@@ -84,10 +84,11 @@
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
}
- val popup: Markup_Tree.Select[XML.Tree] =
+ val popup: Markup_Tree.Select[String] =
{
case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
- if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => msg
+ if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
+ Pretty.string_of(List(msg), margin = 40)
}
val gutter_message: Markup_Tree.Select[Icon] =