src/Pure/PIDE/xml.scala

 */
 
 package isabelle
 
 
-object XML
-{
+object XML {
   /** XML trees **/
 
   /* datatype representation */
 
   type Attribute = Properties.Entry
   type Attributes = Properties.T
 
   sealed abstract class Tree { override def toString: String = string_of_tree(this) }
   type Body = List[Tree]
-  case class Elem(markup: Markup, body: Body) extends Tree
-  {
+  case class Elem(markup: Markup, body: Body) extends Tree {
     private lazy val hash: Int = (markup, body).hashCode()
     override def hashCode(): Int = hash
 
     def name: String = markup.name
 

       if (more_attributes.isEmpty) this
       else Elem(markup.update_properties(more_attributes), body)
 
     def + (att: Attribute): Elem = Elem(markup + att, body)
   }
-  case class Text(content: String) extends Tree
-  {
+  case class Text(content: String) extends Tree {
     private lazy val hash: Int = content.hashCode()
     override def hashCode(): Int = hash
   }
 
   def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)

     string(bg) ::: body ::: string(en)
 
 
   /* name space */
 
-  object Namespace
-  {
+  object Namespace {
     def apply(prefix: String, target: String): Namespace =
       new Namespace(prefix, target)
   }
 
-  final class Namespace private(prefix: String, target: String)
-  {
+  final class Namespace private(prefix: String, target: String) {
     def apply(name: String): String = prefix + ":" + name
     val attribute: XML.Attribute = ("xmlns:" + prefix, target)
 
     override def toString: String = attribute.toString
   }

 
   val XML_ELEM = "xml_elem"
   val XML_NAME = "xml_name"
   val XML_BODY = "xml_body"
 
-  object Wrapped_Elem
-  {
+  object Wrapped_Elem {
     def apply(markup: Markup, body1: Body, body2: Body): XML.Elem =
       XML.Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties),
         XML.Elem(Markup(XML_BODY, Nil), body1) :: body2)
 
     def unapply(tree: Tree): Option[(Markup, Body, Body)] =

           Some(Markup(name, props), body1, body2)
         case _ => None
       }
   }
 
-  object Root_Elem
-  {
+  object Root_Elem {
     def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body)
     def unapply(tree: Tree): Option[Body] =
       tree match {
         case XML.Elem(Markup(XML_ELEM, Nil), body) => Some(body)
         case _ => None

   }
 
 
   /* traverse text */
 
-  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
-  {
+  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = {
     def traverse(x: A, t: Tree): A =
       t match {
         case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse)
         case XML.Elem(_, ts) => ts.foldLeft(x)(traverse)
         case XML.Text(s) => op(x, s)

   def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) }
 
 
   /* text content */
 
-  def content(body: Body): String =
-  {
+  def content(body: Body): String = {
     val text = new StringBuilder(text_length(body))
     traverse_text(body)(()) { case (_, s) => text.append(s) }
     text.toString
   }
 

 
   /** string representation **/
 
   val header: String = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n"
 
-  def output_char(s: StringBuilder, c: Char, permissive: Boolean = false): Unit =
-  {
+  def output_char(s: StringBuilder, c: Char, permissive: Boolean = false): Unit = {
     c match {
       case '<' => s ++= "&lt;"
       case '>' => s ++= "&gt;"
       case '&' => s ++= "&amp;"
       case '"' if !permissive => s ++= "&quot;"
       case '\'' if !permissive => s ++= "&apos;"
       case _ => s += c
     }
   }
 
-  def output_string(s: StringBuilder, str: String, permissive: Boolean = false): Unit =
-  {
+  def output_string(s: StringBuilder, str: String, permissive: Boolean = false): Unit = {
     if (str == null) s ++= str
     else str.iterator.foreach(output_char(s, _, permissive = permissive))
   }
 
-  def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false): Unit =
-  {
+  def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false): Unit = {
     s += '<'
     s ++= markup.name
     for ((a, b) <- markup.properties) {
       s += ' '
       s ++= a

     }
     if (end) s += '/'
     s += '>'
   }
 
-  def output_elem_end(s: StringBuilder, name: String): Unit =
-  {
+  def output_elem_end(s: StringBuilder, name: String): Unit = {
     s += '<'
     s += '/'
     s ++= name
     s += '>'
   }
 
-  def string_of_body(body: Body): String =
-  {
+  def string_of_body(body: Body): String = {
     val s = new StringBuilder
 
     def tree(t: Tree): Unit =
       t match {
         case XML.Elem(markup, Nil) =>

   def text(s: String): String = string_of_tree(XML.Text(s))
 
 
   /** cache **/
 
-  object Cache
-  {
+  object Cache {
     def make(
         xz: XZ.Cache = XZ.Cache.make(),
         max_string: Int = isabelle.Cache.default_max_string,
         initial_size: Int = isabelle.Cache.default_initial_size): Cache =
       new Cache(xz, max_string, initial_size)
 
     val none: Cache = make(XZ.Cache.none, max_string = 0)
   }
 
   class Cache(val xz: XZ.Cache, max_string: Int, initial_size: Int)
-    extends isabelle.Cache(max_string, initial_size)
-  {
-    protected def cache_props(x: Properties.T): Properties.T =
-    {
+  extends isabelle.Cache(max_string, initial_size) {
+    protected def cache_props(x: Properties.T): Properties.T = {
       if (x.isEmpty) x
       else
         lookup(x) match {
           case Some(y) => y
           case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2))))
         }
     }
 
-    protected def cache_markup(x: Markup): Markup =
-    {
+    protected def cache_markup(x: Markup): Markup = {
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
             case Markup(name, props) =>
               store(Markup(cache_string(name), cache_props(props)))
           }
       }
     }
 
-    protected def cache_tree(x: XML.Tree): XML.Tree =
-    {
+    protected def cache_tree(x: XML.Tree): XML.Tree = {
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
             case XML.Elem(markup, body) =>

             case XML.Text(text) => store(XML.Text(cache_string(text)))
           }
       }
     }
 
-    protected def cache_body(x: XML.Body): XML.Body =
-    {
+    protected def cache_body(x: XML.Body): XML.Body = {
       if (x.isEmpty) x
       else
         lookup(x) match {
           case Some(y) => y
           case None => x.map(cache_tree)

 
   abstract class Error(s: String) extends Exception(s)
   class XML_Atom(s: String) extends Error(s)
   class XML_Body(body: XML.Body) extends Error("")
 
-  object Encode
-  {
+  object Encode {
     type T[A] = A => XML.Body
     type V[A] = PartialFunction[A, (List[String], XML.Body)]
     type P[A] = PartialFunction[A, List[String]]
 
 

       (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
 
     def list[A](f: T[A]): T[List[A]] =
       (xs => xs.map((x: A) => node(f(x))))
 
-    def option[A](f: T[A]): T[Option[A]] =
-    {
+    def option[A](f: T[A]): T[Option[A]] = {
       case None => Nil
       case Some(x) => List(node(f(x)))
     }
 
-    def variant[A](fs: List[V[A]]): T[A] =
-    {
+    def variant[A](fs: List[V[A]]): T[A] = {
       case x =>
         val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
         List(tagged(tag, f(x)))
     }
   }
 
-  object Decode
-  {
+  object Decode {
     type T[A] = XML.Body => A
     type V[A] = (List[String], XML.Body) => A
     type P[A] = PartialFunction[List[String], A]
 
 

       }
 
 
     /* representation of standard types */
 
-    val tree: T[XML.Tree] =
-    {
+    val tree: T[XML.Tree] = {
       case List(t) => t
       case ts => throw new XML_Body(ts)
     }
 
-    val properties: T[Properties.T] =
-    {
+    val properties: T[Properties.T] = {
       case List(XML.Elem(Markup(":", props), Nil)) => props
       case ts => throw new XML_Body(ts)
     }
 
-    val string: T[String] =
-    {
+    val string: T[String] = {
       case Nil => ""
       case List(XML.Text(s)) => s
       case ts => throw new XML_Body(ts)
     }
 

 
     val bool: T[Boolean] = (x => bool_atom(string(x)))
 
     val unit: T[Unit] = (x => unit_atom(string(x)))
 
-    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
-    {
+    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = {
       case List(t1, t2) => (f(node(t1)), g(node(t2)))
       case ts => throw new XML_Body(ts)
     }
 
-    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
-    {
+    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = {
       case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
       case ts => throw new XML_Body(ts)
     }
 
     def list[A](f: T[A]): T[List[A]] =
       (ts => ts.map(t => f(node(t))))
 
-    def option[A](f: T[A]): T[Option[A]] =
-    {
+    def option[A](f: T[A]): T[Option[A]] = {
       case Nil => None
       case List(t) => Some(f(node(t)))
       case ts => throw new XML_Body(ts)
     }
 
-    def variant[A](fs: List[V[A]]): T[A] =
-    {
+    def variant[A](fs: List[V[A]]): T[A] = {
       case List(t) =>
         val (tag, (xs, ts)) = tagged(t)
         val f =
           try { fs(tag) }
           catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }