src/Pure/PIDE/markup.scala

 */
 
 package isabelle
 
 
-object Markup
-{
+object Markup {
   /* elements */
 
-  object Elements
-  {
+  object Elements {
     def apply(elems: Set[String]): Elements = new Elements(elems)
     def apply(elems: String*): Elements = apply(Set(elems: _*))
     val empty: Elements = apply()
     val full: Elements =
-      new Elements(Set.empty)
-      {
+      new Elements(Set.empty) {
         override def apply(elem: String): Boolean = true
         override def toString: String = "Elements.full"
       }
   }
 
-  sealed class Elements private[Markup](private val rep: Set[String])
-  {
+  sealed class Elements private[Markup](private val rep: Set[String]) {
     def apply(elem: String): Boolean = rep.contains(elem)
     def + (elem: String): Elements = new Elements(rep + elem)
     def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
     def - (elem: String): Elements = new Elements(rep - elem)
     def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)

   /* basic markup */
 
   val Empty: Markup = Markup("", Nil)
   val Broken: Markup = Markup("broken", Nil)
 
-  class Markup_Elem(val name: String)
-  {
+  class Markup_Elem(val name: String) {
     def apply(props: Properties.T = Nil): Markup = Markup(name, props)
     def unapply(markup: Markup): Option[Properties.T] =
       if (markup.name == name) Some(markup.properties) else None
   }
 
-  class Markup_String(val name: String, prop: String)
-  {
+  class Markup_String(val name: String, prop: String) {
     val Prop: Properties.String = new Properties.String(prop)
 
     def apply(s: String): Markup = Markup(name, Prop(s))
     def unapply(markup: Markup): Option[String] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
     def get(markup: Markup): String = unapply(markup).getOrElse("")
   }
 
-  class Markup_Int(val name: String, prop: String)
-  {
+  class Markup_Int(val name: String, prop: String) {
     val Prop: Properties.Int = new Properties.Int(prop)
 
     def apply(i: Int): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
     def get(markup: Markup): Int = unapply(markup).getOrElse(0)
   }
 
-  class Markup_Long(val name: String, prop: String)
-  {
+  class Markup_Long(val name: String, prop: String) {
     val Prop: Properties.Long = new Properties.Long(prop)
 
     def apply(i: Long): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Long] =
       if (markup.name == name) Prop.unapply(markup.properties) else None

   /* formal entities */
 
   val BINDING = "binding"
   val ENTITY = "entity"
 
-  object Entity
-  {
+  object Entity {
     val Def = new Markup_Long(ENTITY, "def")
     val Ref = new Markup_Long(ENTITY, "ref")
 
-    object Occ
-    {
+    object Occ {
       def unapply(markup: Markup): Option[Long] =
         Def.unapply(markup) orElse Ref.unapply(markup)
     }
 
     def unapply(markup: Markup): Option[(String, String)] =

 
 
   /* expression */
 
   val EXPRESSION = "expression"
-  object Expression
-  {
+  object Expression {
     def unapply(markup: Markup): Option[String] =
       markup match {
         case Markup(EXPRESSION, props) => Some(Kind.get(props))
         case _ => None
       }

   val Symbols = new Properties.Boolean("symbols")
   val Antiquotes = new Properties.Boolean("antiquotes")
   val Delimited = new Properties.Boolean("delimited")
 
   val LANGUAGE = "language"
-  object Language
-  {
+  object Language {
     val DOCUMENT = "document"
     val ML = "ML"
     val SML = "SML"
     val PATH = "path"
     val UNKNOWN = "unknown"

             case _ => None
           }
         case _ => None
       }
 
-    object Path
-    {
+    object Path {
       def unapply(markup: Markup): Option[Boolean] =
         markup match {
           case Language(PATH, _, _, delimited) => Some(delimited)
           case _ => None
         }

 
   val Consistent = new Properties.Boolean("consistent")
   val Indent = new Properties.Int("indent")
   val Width = new Properties.Int("width")
 
-  object Block
-  {
+  object Block {
     val name = "block"
     def apply(c: Boolean, i: Int): Markup =
       Markup(name,
         (if (c) Consistent(c) else Nil) :::
         (if (i != 0) Indent(i) else Nil))

         Some((c, i))
       }
       else None
   }
 
-  object Break
-  {
+  object Break {
     val name = "break"
     def apply(w: Int, i: Int): Markup =
       Markup(name,
         (if (w != 0) Width(w) else Nil) :::
         (if (i != 0) Indent(i) else Nil))

   val PLAIN_TEXT = "plain_text"
 
   val PARAGRAPH = "paragraph"
   val TEXT_FOLD = "text_fold"
 
-  object Document_Tag extends Markup_String("document_tag", NAME)
-  {
+  object Document_Tag extends Markup_String("document_tag", NAME) {
     val IMPORTANT = "important"
     val UNIMPORTANT = "unimportant"
   }
 
 

 
   val Elapsed = new Properties.Double("elapsed")
   val CPU = new Properties.Double("cpu")
   val GC = new Properties.Double("gc")
 
-  object Timing_Properties
-  {
+  object Timing_Properties {
     def apply(timing: isabelle.Timing): Properties.T =
       Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
 
     def unapply(props: Properties.T): Option[isabelle.Timing] =
       (props, props, props) match {

       unapply(props).getOrElse(isabelle.Timing.zero)
   }
 
   val TIMING = "timing"
 
-  object Timing
-  {
+  object Timing {
     def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
 
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
         case Markup(TIMING, Timing_Properties(timing)) => Some(timing)

 
   /* process result */
 
   val Return_Code = new Properties.Int("return_code")
 
-  object Process_Result
-  {
+  object Process_Result {
     def apply(result: Process_Result): Properties.T =
       Return_Code(result.rc) :::
         (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
 
     def unapply(props: Properties.T): Option[Process_Result] =

 
   val COUNT = "count"
   val ML_PROFILING_ENTRY = "ML_profiling_entry"
   val ML_PROFILING = "ML_profiling"
 
-  object ML_Profiling
-  {
+  object ML_Profiling {
     def unapply_entry(tree: XML.Tree): Option[isabelle.ML_Profiling.Entry] =
       tree match {
         case XML.Elem(Markup(ML_PROFILING_ENTRY, List((NAME, name), (COUNT, Value.Long(count)))), _) =>
           Some(isabelle.ML_Profiling.Entry(name, count))
         case _ => None

 
   /* protocol message functions */
 
   val FUNCTION = "function"
 
-  class Function(val name: String)
-  {
+  class Function(val name: String) {
     val PROPERTY: Properties.Entry = (FUNCTION, name)
   }
 
-  class Properties_Function(name: String) extends Function(name)
-  {
+  class Properties_Function(name: String) extends Function(name) {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
         case PROPERTY :: args => Some(args)
         case _ => None
       }
   }
 
-  class Name_Function(name: String) extends Function(name)
-  {
+  class Name_Function(name: String) extends Function(name) {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (NAME, a)) => Some(a)
         case _ => None
       }
   }
 
-  object ML_Statistics extends Function("ML_statistics")
-  {
+  object ML_Statistics extends Function("ML_statistics") {
     def unapply(props: Properties.T): Option[(Long, String)] =
       props match {
         case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
           Some((pid, stats_dir))
         case _ => None

   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
   def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
-  object Session_Timing extends Properties_Function("session_timing")
-  {
+  object Session_Timing extends Properties_Function("session_timing") {
     val Threads = new Properties.Int("threads")
   }
   object Task_Statistics extends Properties_Function("task_statistics")
 
   object Loading_Theory extends Properties_Function("loading_theory")

 
   object Commands_Accepted extends Function("commands_accepted")
   object Assign_Update extends Function("assign_update")
   object Removed_Versions extends Function("removed_versions")
 
-  object Invoke_Scala extends Function("invoke_scala")
-  {
+  object Invoke_Scala extends Function("invoke_scala") {
     def unapply(props: Properties.T): Option[(String, String)] =
       props match {
         case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
         case _ => None
       }
   }
 
-  object Cancel_Scala extends Function("cancel_scala")
-  {
+  object Cancel_Scala extends Function("cancel_scala") {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (ID, id)) => Some(id)
         case _ => None
       }

 
 
   /* debugger output */
 
   val DEBUGGER_STATE = "debugger_state"
-  object Debugger_State
-  {
+  object Debugger_State {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
   val DEBUGGER_OUTPUT = "debugger_output"
-  object Debugger_Output
-  {
+  object Debugger_Output {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
         case _ => None
       }

   val SIMP_TRACE_RECURSE = "simp_trace_recurse"
   val SIMP_TRACE_HINT = "simp_trace_hint"
   val SIMP_TRACE_IGNORE = "simp_trace_ignore"
 
   val SIMP_TRACE_CANCEL = "simp_trace_cancel"
-  object Simp_Trace_Cancel
-  {
+  object Simp_Trace_Cancel {
     def unapply(props: Properties.T): Option[Long] =
       props match {
         case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
         case _ => None
       }
   }
 
 
   /* XML data representation */
 
-  def encode: XML.Encode.T[Markup] = (markup: Markup) =>
-  {
+  def encode: XML.Encode.T[Markup] = (markup: Markup) => {
     import XML.Encode._
     pair(string, properties)((markup.name, markup.properties))
   }
 
-  def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
-  {
+  def decode: XML.Decode.T[Markup] = (body: XML.Body) => {
     import XML.Decode._
     val (name, props) = pair(string, properties)(body)
     Markup(name, props)
   }
 }
 
 
-sealed case class Markup(name: String, properties: Properties.T)
-{
+sealed case class Markup(name: String, properties: Properties.T) {
   def is_empty: Boolean = name.isEmpty
 
   def position_properties: Position.T = properties.filter(Markup.position_property)
 
   def markup(s: String): String =