src/Tools/jEdit/src/isabelle_markup.scala

   }
 
 
   /* markup selectors */
 
-  val message: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
-    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
-    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
-  }
+  val message =
+    Markup_Tree.Select[Color](
+    {
+      case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
+      case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
+      case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
+    })
 
   val tooltip_message =
     Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
       {
         case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
         if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
           msgs + (serial ->
             Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
       })
 
-  val gutter_message: Markup_Tree.Select[Icon] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
-      body match {
-        case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
-        case _ => warning_icon
-      }
-    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
-  }
-
-  val background1: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
-    case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
-  }
-
-  val background2: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
-  }
-
-  val foreground: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
-    case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
-    case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
-  }
+  val gutter_message =
+    Markup_Tree.Select[Icon](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
+          body match {
+            case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
+            case _ => warning_icon
+          }
+        case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
+      })
+
+  val background1 =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
+        case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
+      })
+
+  val background2 =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
+      })
+
+  val foreground =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
+        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
+        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
+      })
 
   private val text_colors: Map[String, Color] =
     Map(
       Markup.STRING -> get_color("black"),
       Markup.ALTSTRING -> get_color("black"),

       Markup.ML_STRING -> get_color("#D2691E"),
       Markup.ML_COMMENT -> get_color("#8B0000"),
       Markup.ML_MALFORMED -> get_color("#FF6A6A"),
       Markup.ANTIQ -> get_color("blue"))
 
-  val text_color: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
-  }
+  val text_color =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
+      })
 
   private val tooltips: Map[String, String] =
     Map(
       Markup.SORT -> "sort",
       Markup.TYP -> "type",

 
   private def string_of_typing(kind: String, body: XML.Body): String =
     Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
       margin = Isabelle.Int_Property("tooltip-margin"))
 
-  val tooltip1: Markup_Tree.Select[String] =
-  {
-    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
-    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
-    case Text.Info(_, XML.Elem(Markup(name, _), _))
-    if tooltips.isDefinedAt(name) => tooltips(name)
-  }
-
-  val tooltip2: Markup_Tree.Select[String] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
-  }
+  val tooltip1 =
+    Markup_Tree.Select[String](
+      {
+        case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
+        case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
+        case Text.Info(_, XML.Elem(Markup(name, _), _))
+        if tooltips.isDefinedAt(name) => tooltips(name)
+      })
+
+  val tooltip2 =
+    Markup_Tree.Select[String](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
+      })
 
   private val subexp_include =
     Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
       Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
       Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
 
-  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
-  {
-    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
-      (range, subexp_color)
-  }
+  val subexp =
+    Markup_Tree.Select[(Text.Range, Color)](
+      {
+        case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+          (range, subexp_color)
+      })
 
 
   /* token markup -- text styles */
 
   private val command_style: Map[String, Byte] =