src/Pure/PIDE/yxml.scala
changeset 75393 87ebf5a50283
parent 73712 3eba8d4b624b
--- a/src/Pure/PIDE/yxml.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/PIDE/yxml.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -11,8 +11,7 @@
 import scala.collection.mutable
 
 
-object YXML
-{
+object YXML {
   /* chunk markers */
 
   val X = '\u0005'
@@ -32,8 +31,7 @@
 
   /* string representation */
 
-  def traversal(string: String => Unit, body: XML.Body): Unit =
-  {
+  def traversal(string: String => Unit, body: XML.Body): Unit = {
     def tree(t: XML.Tree): Unit =
       t match {
         case XML.Elem(markup @ Markup(name, atts), ts) =>
@@ -51,8 +49,7 @@
     body.foreach(tree)
   }
 
-  def string_of_body(body: XML.Body): String =
-  {
+  def string_of_body(body: XML.Body): String = {
     val s = new StringBuilder
     traversal(str => s ++= str, body)
     s.toString
@@ -74,8 +71,7 @@
     Properties.Eq.unapply(source.toString) getOrElse err_attribute()
 
 
-  def parse_body(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body =
-  {
+  def parse_body(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = {
     /* stack operations */
 
     def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
@@ -134,14 +130,12 @@
   private def markup_broken(source: CharSequence) =
     XML.Elem(Markup.Broken, List(XML.Text(source.toString)))
 
-  def parse_body_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body =
-  {
+  def parse_body_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = {
     try { parse_body(source, cache = cache) }
     catch { case ERROR(_) => List(markup_broken(source)) }
   }
 
-  def parse_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree =
-  {
+  def parse_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree = {
     try { parse(source, cache = cache) }
     catch { case ERROR(_) => markup_broken(source) }
   }