# HG changeset patch
# User wenzelm
# Date 1326402354 -3600
# Node ID 9d2273d50f4fe92c2555552e2c1acae3d012f876
# Parent  cd040c5772dea6e94f8fcfb33f8c5899ae426bae
tuned;

diff -r cd040c5772de -r 9d2273d50f4f src/Tools/jEdit/src/isabelle_rendering.scala
--- 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,