src/Pure/library.scala

 import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.util.matching.Regex
 
 
-object Library
-{
+object Library {
   /* resource management */
 
-  def using[A <: AutoCloseable, B](a: A)(f: A => B): B =
-  {
+  def using[A <: AutoCloseable, B](a: A)(f: A => B): B = {
     try { f(a) }
     finally { if (a != null) a.close() }
   }
 
 
   /* integers */
 
   private val small_int = 10000
-  private lazy val small_int_table =
-  {
+  private lazy val small_int_table = {
     val array = new Array[String](small_int)
     for (i <- 0 until small_int) array(i) = i.toString
     array
   }
 
-  def is_small_int(s: String): Boolean =
-  {
+  def is_small_int(s: String): Boolean = {
     val len = s.length
     1 <= len && len <= 4 &&
     s.forall(c => '0' <= c && c <= '9') &&
     (len == 1 || s(0) != '0')
   }

     else i.toString
 
 
   /* separated chunks */
 
-  def separate[A](s: A, list: List[A]): List[A] =
-  {
+  def separate[A](s: A, list: List[A]): List[A] = {
     val result = new mutable.ListBuffer[A]
     var first = true
     for (x <- list) {
       if (first) {
         first = false

   }
 
   def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
     new Iterator[CharSequence] {
       private val end = source.length
-      private def next_chunk(i: Int): Option[(CharSequence, Int)] =
-      {
+      private def next_chunk(i: Int): Option[(CharSequence, Int)] = {
         if (i < end) {
           var j = i
           var cont = true
           while (cont) {
             j += 1

     isabelle.setup.Library.prefix_lines(prfx, str)
 
   def indent_lines(n: Int, str: String): String =
     prefix_lines(Symbol.spaces(n), str)
 
-  def first_line(source: CharSequence): String =
-  {
+  def first_line(source: CharSequence): String = {
     val lines = separated_chunks(_ == '\n', source)
     if (lines.hasNext) lines.next().toString
     else ""
   }
 

   def decode_lines(s: String): String = s.replace('\u000b', '\n')
 
 
   /* strings */
 
-  def make_string(f: StringBuilder => Unit, capacity: Int = 16): String =
-  {
+  def make_string(f: StringBuilder => Unit, capacity: Int = 16): String = {
     val s = new StringBuilder(capacity)
     f(s)
     s.toString
   }
 

   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
 
 
   /* CharSequence */
 
-  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
-  {
+  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence {
     require(0 <= start && start <= end && end <= text.length, "bad reverse range")
 
     def this(text: CharSequence) = this(text, 0, text.length)
 
     def length: Int = end - start

 
     def subSequence(i: Int, j: Int): CharSequence =
       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
       else throw new IndexOutOfBoundsException
 
-    override def toString: String =
-    {
+    override def toString: String = {
       val buf = new StringBuilder(length)
       for (i <- 0 until length)
         buf.append(charAt(i))
       buf.toString
     }
   }
 
-  class Line_Termination(text: CharSequence) extends CharSequence
-  {
+  class Line_Termination(text: CharSequence) extends CharSequence {
     def length: Int = text.length + 1
     def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
     def subSequence(i: Int, j: Int): CharSequence =
       if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
       else text.subSequence(i, j)

   /* lists */
 
   def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
     (xs.takeWhile(pred), xs.dropWhile(pred))
 
-  def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
-  {
+  def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = {
     val rev_xs = xs.reverse
     (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse)
   }
 
   def trim[A](pred: A => Boolean, xs: List[A]): List[A] =

   def merge[A](xs: List[A], ys: List[A]): List[A] =
     if (xs.eq(ys)) xs
     else if (xs.isEmpty) ys
     else ys.foldRight(xs)(Library.insert(_)(_))
 
-  def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
-  {
+  def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = {
     val result = new mutable.ListBuffer[A]
     xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x)
     result.toList
   }
 
-  def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
-  {
+  def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = {
     val result = new mutable.ListBuffer[A]
     @tailrec def dups(rest: List[A]): Unit =
       rest match {
         case Nil =>
         case x :: xs =>

     if (list == null || list.isEmpty) None else Some(list)
 
 
   /* reflection */
 
-  def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean =
-  {
+  def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean = {
     import scala.language.existentials
-    @tailrec def subclass(c: Class[_]): Boolean =
-    {
-      c == b ||
-        {
-          val d = c.getSuperclass
-          d != null && subclass(d)
-        }
+    @tailrec def subclass(c: Class[_]): Boolean = {
+      c == b || { val d = c.getSuperclass; d != null && subclass(d) }
     }
     subclass(a)
   }
 }