--- a/src/Tools/jEdit/src/isabelle_rendering.scala Thu Jan 12 21:50:00 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Thu Jan 12 22:05:54 2012 +0100
@@ -88,42 +88,34 @@
})
def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
- snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
- Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
- {
- case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
- if markup == Isabelle_Markup.WRITELN ||
- markup == Isabelle_Markup.WARNING ||
- markup == Isabelle_Markup.ERROR =>
- msgs + (serial ->
- Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
- }) match {
- case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
- Some(cat_lines(msgs.iterator.map(_._2)))
- case _ => None
- }
+ {
+ val msgs =
+ snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
+ Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+ {
+ case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
+ if markup == Isabelle_Markup.WRITELN ||
+ markup == Isabelle_Markup.WARNING ||
+ markup == Isabelle_Markup.ERROR =>
+ msgs + (serial ->
+ Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
+ }).toList.flatMap(_.info)
+ if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
+ }
def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
- {
- val icons =
- (snapshot.select_markup(range,
- Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
- {
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
- body match {
- case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
- case _ => warning_icon
- }
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
- }).map { case Text.Info(_, icon) => icon }).toList.sortWith(_ >= _)
- icons match {
- case icon :: _ => Some(icon)
- case Nil => None
- }
- }
+ snapshot.select_markup(range,
+ Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+ {
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
+ body match {
+ case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
+ case _ => warning_icon
+ }
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
+ }).map(_.info).toList.sortWith(_ >= _).headOption
def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
- {
for {
Text.Info(r, result) <-
snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
@@ -147,7 +139,6 @@
case (_, opt_color) => opt_color
})
} yield Text.Info(r, color)
- }
def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
snapshot.select_markup(range,