diff --git a/src/Pure/Thy/html.scala b/src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala
+++ b/src/Pure/Thy/html.scala
@@ -1,441 +1,441 @@
 /*  Title:      Pure/Thy/html.scala
     Author:     Makarius
 
 HTML presentation elements.
 */
 
 package isabelle
 
 
 object HTML
 {
   /* attributes */
 
   class Attribute(val name: String, value: String)
   {
     def xml: XML.Attribute = name -> value
     def apply(elem: XML.Elem): XML.Elem = elem + xml
   }
 
   def id(s: String): Attribute = new Attribute("id", s)
   def class_(name: String): Attribute = new Attribute("class", name)
 
   def width(w: Int): Attribute = new Attribute("width", w.toString)
   def height(h: Int): Attribute = new Attribute("height", h.toString)
   def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
 
   val entity_def: Attribute = class_("entity_def")
   val entity_ref: Attribute = class_("entity_ref")
 
 
   /* structured markup operators */
 
   def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
   val break: XML.Body = List(XML.elem("br"))
   val nl: XML.Body = List(XML.Text("\n"))
 
   class Operator(val name: String)
   {
     def apply(body: XML.Body): XML.Elem = XML.elem(name, body)
     def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body))
     def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body)
   }
 
   class Heading(name: String) extends Operator(name)
   {
     def apply(txt: String): XML.Elem = super.apply(text(txt))
     def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt))
     def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt))
   }
 
   val div = new Operator("div")
   val span = new Operator("span")
   val pre = new Operator("pre")
   val par = new Operator("p")
   val sub = new Operator("sub")
   val sup = new Operator("sup")
   val emph = new Operator("em")
   val bold = new Operator("b")
   val code = new Operator("code")
   val item = new Operator("li")
   val list = new Operator("ul")
   val `enum` = new Operator("ol")
   val descr = new Operator("dl")
   val dt = new Operator("dt")
   val dd = new Operator("dd")
 
   val title = new Heading("title")
   val chapter = new Heading("h1")
   val section = new Heading("h2")
   val subsection = new Heading("h3")
   val subsubsection = new Heading("h4")
   val paragraph = new Heading("h5")
   val subparagraph = new Heading("h6")
 
   def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_)))
   def enumerate(items: List[XML.Body]): XML.Elem = `enum`(items.map(item(_)))
   def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
     descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) }))
 
   def link(href: String, body: XML.Body): XML.Elem =
     XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
 
   def link(path: Path, body: XML.Body): XML.Elem = link(path.implode, body)
 
   def image(src: String, alt: String = ""): XML.Elem =
     XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
 
   def source(body: XML.Body): XML.Elem = pre("source", body)
   def source(src: String): XML.Elem = source(text(src))
 
   def style(s: String): XML.Elem = XML.elem("style", text(s))
   def style_file(href: String): XML.Elem =
     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
   def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
 
   def script(s: String): XML.Elem = XML.elem("script", text(s))
   def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
   def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
 
 
   /* output text with control symbols */
 
   private val control: Map[Symbol.Symbol, Operator] =
     Map(
       Symbol.sub -> sub, Symbol.sub_decoded -> sub,
       Symbol.sup -> sup, Symbol.sup_decoded -> sup,
       Symbol.bold -> bold, Symbol.bold_decoded -> bold)
 
   private val control_block_begin: Map[Symbol.Symbol, Operator] =
     Map(
       Symbol.bsub -> sub, Symbol.bsub_decoded -> sub,
       Symbol.bsup -> sup, Symbol.bsup_decoded -> sup)
 
   private val control_block_end: Map[Symbol.Symbol, Operator] =
     Map(
       Symbol.esub -> sub, Symbol.esub_decoded -> sub,
       Symbol.esup -> sup, Symbol.esup_decoded -> sup)
 
   def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
 
   def is_control_block_begin(sym: Symbol.Symbol): Boolean = control_block_begin.isDefinedAt(sym)
   def is_control_block_end(sym: Symbol.Symbol): Boolean = control_block_end.isDefinedAt(sym)
   def is_control_block_pair(bg: Symbol.Symbol, en: Symbol.Symbol): Boolean =
   {
     val bg_decoded = Symbol.decode(bg)
     val en_decoded = Symbol.decode(en)
     bg_decoded == Symbol.bsub_decoded && en_decoded == Symbol.esub_decoded ||
     bg_decoded == Symbol.bsup_decoded && en_decoded == Symbol.esup_decoded
   }
 
   def check_control_blocks(body: XML.Body): Boolean =
   {
     var ok = true
     var open = List.empty[Symbol.Symbol]
     for { XML.Text(text) <- body; sym <- Symbol.iterator(text) } {
       if (is_control_block_begin(sym)) open ::= sym
       else if (is_control_block_end(sym)) {
         open match {
           case bg :: rest if is_control_block_pair(bg, sym) => open = rest
           case _ => ok = false
         }
       }
     }
     ok && open.isEmpty
   }
 
   def output(s: StringBuilder, text: String,
     control_blocks: Boolean, hidden: Boolean, permissive: Boolean): Unit =
   {
     def output_string(str: String): Unit =
       XML.output_string(s, str, permissive = permissive)
 
     def output_hidden(body: => Unit): Unit =
       if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
 
     def output_symbol(sym: Symbol.Symbol): Unit =
       if (sym != "") {
         control_block_begin.get(sym) match {
           case Some(op) if control_blocks =>
             output_hidden(output_string(sym))
             XML.output_elem(s, Markup(op.name, Nil))
           case _ =>
             control_block_end.get(sym) match {
               case Some(op) if control_blocks =>
                 XML.output_elem_end(s, op.name)
                 output_hidden(output_string(sym))
               case _ =>
                 if (hidden && Symbol.is_control_encoded(sym)) {
                   output_hidden(output_string(Symbol.control_prefix))
                   s ++= "<span class=\"control\">"
                   output_string(Symbol.control_name(sym).get)
                   s ++= "</span>"
                   output_hidden(output_string(Symbol.control_suffix))
                 }
                 else output_string(sym)
             }
         }
       }
 
     var ctrl = ""
     for (sym <- Symbol.iterator(text)) {
       if (is_control(sym)) { output_symbol(ctrl); ctrl = sym }
       else {
         control.get(ctrl) match {
           case Some(op) if Symbol.is_controllable(sym) =>
             output_hidden(output_symbol(ctrl))
             XML.output_elem(s, Markup(op.name, Nil))
             output_symbol(sym)
             XML.output_elem_end(s, op.name)
           case _ =>
             output_symbol(ctrl)
             output_symbol(sym)
         }
         ctrl = ""
       }
     }
     output_symbol(ctrl)
   }
 
   def output(text: String): String =
   {
     val control_blocks = check_control_blocks(List(XML.Text(text)))
     Library.make_string(output(_, text,
       control_blocks = control_blocks, hidden = false, permissive = true))
   }
 
 
   /* output XML as HTML */
 
   private val structural_elements =
     Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
       "ul", "ol", "dl", "li", "dt", "dd")
 
   def output(s: StringBuilder, xml: XML.Body, hidden: Boolean, structural: Boolean): Unit =
   {
     def output_body(body: XML.Body): Unit =
     {
       val control_blocks = check_control_blocks(body)
       body foreach {
         case XML.Elem(markup, Nil) =>
           XML.output_elem(s, markup, end = true)
         case XML.Elem(markup, ts) =>
           if (structural && structural_elements(markup.name)) s += '\n'
           XML.output_elem(s, markup)
           output_body(ts)
           XML.output_elem_end(s, markup.name)
           if (structural && structural_elements(markup.name)) s += '\n'
         case XML.Text(txt) =>
           output(s, txt, control_blocks = control_blocks, hidden = hidden, permissive = true)
       }
     }
     output_body(xml)
   }
 
   def output(body: XML.Body, hidden: Boolean, structural: Boolean): String =
-    Library.make_string(output(_, body, hidden, structural))
+    Library.make_string(output(_, body, hidden, structural), capacity = XML.text_length(body) * 2)
 
   def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String =
     output(List(tree), hidden, structural)
 
 
   /* messages */
 
   // background
   val writeln_message: Attribute = class_("writeln_message")
   val warning_message: Attribute = class_("warning_message")
   val error_message: Attribute = class_("error_message")
 
   // underline
   val writeln: Attribute = class_("writeln")
   val warning: Attribute = class_("warning")
   val error: Attribute = class_("error")
 
 
   /* tooltips */
 
   def tooltip(item: XML.Body, tip: XML.Body): XML.Elem =
     span(item ::: List(div("tooltip", tip)))
 
   def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem =
     HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
 
 
   /* GUI elements */
 
   object GUI
   {
     private def optional_value(text: String): XML.Attributes =
       proper_string(text).map(a => "value" -> a).toList
 
     private def optional_name(name: String): XML.Attributes =
       proper_string(name).map(a => "name" -> a).toList
 
     private def optional_title(tooltip: String): XML.Attributes =
       proper_string(tooltip).map(a => "title" -> a).toList
 
     private def optional_submit(submit: Boolean): XML.Attributes =
       if (submit) List("onChange" -> "this.form.submit()") else Nil
 
     private def optional_checked(selected: Boolean): XML.Attributes =
       if (selected) List("checked" -> "") else Nil
 
     private def optional_action(action: String): XML.Attributes =
       proper_string(action).map(a => "action" -> a).toList
 
     private def optional_onclick(script: String): XML.Attributes =
       proper_string(script).map(a => "onclick" -> a).toList
 
     private def optional_onchange(script: String): XML.Attributes =
       proper_string(script).map(a => "onchange" -> a).toList
 
     def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false,
         script: String = ""): XML.Elem =
       XML.Elem(
         Markup("button",
           List("type" -> (if (submit) "submit" else "button"), "value" -> "true") :::
           optional_name(name) ::: optional_title(tooltip) ::: optional_onclick(script)), body)
 
     def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false,
         selected: Boolean = false, script: String = ""): XML.Elem =
       XML.elem("label",
         XML.elem(
           Markup("input",
             List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) :::
               optional_title(tooltip) ::: optional_submit(submit) :::
               optional_checked(selected) ::: optional_onchange(script))) :: body)
 
     def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "",
         submit: Boolean = false, script: String = ""): XML.Elem =
       XML.elem(Markup("input",
         List("type" -> "text") :::
           (if (columns > 0) List("size" -> columns.toString) else Nil) :::
           optional_value(text) ::: optional_name(name) ::: optional_title(tooltip) :::
           optional_submit(submit) ::: optional_onchange(script)))
 
     def parameter(text: String = "", name: String = ""): XML.Elem =
       XML.elem(
         Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name)))
 
     def form(body: XML.Body, name: String = "", action: String = "", http_post: Boolean = false)
         : XML.Elem =
       XML.Elem(
         Markup("form", optional_name(name) ::: optional_action(action) :::
           (if (http_post) List("method" -> "post") else Nil)), body)
   }
 
 
   /* GUI layout */
 
   object Wrap_Panel
   {
     object Alignment extends Enumeration
     {
       val left, right, center = Value
     }
 
     def apply(contents: List[XML.Elem], name: String = "", action: String = "",
       alignment: Alignment.Value = Alignment.right): XML.Elem =
     {
       val body = Library.separate(XML.Text(" "), contents)
       GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))),
         name = name, action = action)
     }
   }
 
 
   /* document */
 
   val header: String =
     XML.header +
     """<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
 <html xmlns="http://www.w3.org/1999/xhtml">"""
 
   val footer: String = """</html>"""
 
   val head_meta: XML.Elem =
     XML.Elem(Markup("meta",
       List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
 
   def output_document(head: XML.Body, body: XML.Body,
     css: String = "isabelle.css",
     hidden: Boolean = true,
     structural: Boolean = true): String =
   {
     cat_lines(
       List(
         header,
         output(
           XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head),
           hidden = hidden, structural = structural),
         output(XML.elem("body", body),
           hidden = hidden, structural = structural),
         footer))
   }
 
 
   /* fonts */
 
   val fonts_path: Path = Path.explode("fonts")
 
   def init_fonts(dir: Path): Unit =
   {
     val fonts_dir = Isabelle_System.make_directory(dir + HTML.fonts_path)
     for (entry <- Isabelle_Fonts.fonts(hidden = true))
       Isabelle_System.copy_file(entry.path, fonts_dir)
   }
 
   def fonts_dir(prefix: String)(ttf_name: String): String = prefix + "/" + ttf_name
 
   def fonts_url(): String => String =
     (for (entry <- Isabelle_Fonts.fonts(hidden = true))
      yield (entry.path.file_name -> Url.print_file(entry.path.file))).toMap
 
   def fonts_css(make_url: String => String = fonts_url()): String =
   {
     def font_face(entry: Isabelle_Fonts.Entry): String =
       cat_lines(
         List(
           "@font-face {",
           "  font-family: '" + entry.family + "';",
           "  src: url('" + make_url(entry.path.file_name) + "') format('truetype');") :::
         (if (entry.is_bold) List("  font-weight: bold;") else Nil) :::
         (if (entry.is_italic) List("  font-style: italic;") else Nil) :::
         List("}"))
 
     ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face))
       .mkString("", "\n\n", "\n")
   }
 
   def fonts_css_dir(prefix: String = ""): String =
   {
     val prefix1 = if (prefix.isEmpty || prefix.endsWith("/")) prefix else prefix + "/"
     fonts_css(fonts_dir(prefix1 + fonts_path.implode))
   }
 
 
   /* document directory context (fonts + css) */
 
   def relative_prefix(dir: Path, base: Option[Path]): String =
     base match {
       case None => ""
       case Some(base_dir) =>
         val path = File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile)
         if (path.is_current) "" else path.implode + "/"
     }
 
   def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
 
   def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
     base: Option[Path] = None,
     css: String = isabelle_css.file_name,
     hidden: Boolean = true,
     structural: Boolean = true): Unit =
   {
     Isabelle_System.make_directory(dir)
     val prefix = relative_prefix(dir, base)
     File.write(dir + isabelle_css.base, fonts_css_dir(prefix) + "\n\n" + File.read(isabelle_css))
     File.write(dir + Path.basic(name),
       output_document(head, body, css = css, hidden = hidden, structural = structural))
   }
 }
diff --git a/src/Pure/library.scala b/src/Pure/library.scala
--- a/src/Pure/library.scala
+++ b/src/Pure/library.scala
@@ -1,305 +1,305 @@
 /*  Title:      Pure/library.scala
     Author:     Makarius
 
 Basic library.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.util.matching.Regex
 
 
 object Library
 {
   /* resource management */
 
   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 =
   {
     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 =
   {
     val len = s.length
     1 <= len && len <= 4 &&
     s.forall(c => '0' <= c && c <= '9') &&
     (len == 1 || s(0) != '0')
   }
 
   def signed_string_of_long(i: Long): String =
     if (0 <= i && i < small_int) small_int_table(i.toInt)
     else i.toString
 
   def signed_string_of_int(i: Int): String =
     if (0 <= i && i < small_int) small_int_table(i)
     else i.toString
 
 
   /* separated chunks */
 
   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
         result += x
       }
       else {
         result += s
         result += x
       }
     }
     result.toList
   }
 
   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)] =
       {
         if (i < end) {
           var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
           Some((source.subSequence(i + 1, j), j))
         }
         else None
       }
       private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
 
       def hasNext: Boolean = state.isDefined
       def next(): CharSequence =
         state match {
           case Some((s, i)) => state = next_chunk(i); s
           case None => Iterator.empty.next()
         }
     }
 
   def space_explode(sep: Char, str: String): List[String] =
     separated_chunks(_ == sep, str).map(_.toString).toList
 
 
   /* lines */
 
   def terminate_lines(lines: IterableOnce[String]): String =
     lines.iterator.mkString("", "\n", "\n")
 
   def cat_lines(lines: IterableOnce[String]): String =
     lines.iterator.mkString("\n")
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
   def prefix_lines(prfx: String, str: String): String =
     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 =
   {
     val lines = separated_chunks(_ == '\n', source)
     if (lines.hasNext) lines.next().toString
     else ""
   }
 
   def trim_line(s: String): String =
     isabelle.setup.Library.trim_line(s)
 
   def trim_split_lines(s: String): List[String] =
     split_lines(trim_line(s)).map(trim_line)
 
   def encode_lines(s: String): String = s.replace('\n', '\u000b')
   def decode_lines(s: String): String = s.replace('\u000b', '\n')
 
 
   /* strings */
 
-  def make_string(f: StringBuilder => Unit): String =
+  def make_string(f: StringBuilder => Unit, capacity: Int = 16): String =
   {
-    val s = new StringBuilder
+    val s = new StringBuilder(capacity)
     f(s)
     s.toString
   }
 
   def try_unprefix(prfx: String, s: String): Option[String] =
     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
 
   def try_unsuffix(sffx: String, s: String): Option[String] =
     if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
 
   def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s
   def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s
 
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
   def strip_ansi_color(s: String): String =
     s.replaceAll("\u001b\\[\\d+m", "")
 
 
   /* quote */
 
   def single_quote(s: String): String = "'" + s + "'"
 
   def quote(s: String): String = "\"" + s + "\""
 
   def try_unquote(s: String): Option[String] =
     if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
     else None
 
   def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
 
   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
 
 
   /* 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 charAt(i: Int): Char = text.charAt(end - i - 1)
 
     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 =
     {
       val buf = new StringBuilder(length)
       for (i <- 0 until length)
         buf.append(charAt(i))
       buf.toString
     }
   }
 
   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)
     override def toString: String = text.toString + "\n"
   }
 
 
   /* regular expressions */
 
   def make_regex(s: String): Option[Regex] =
     try { Some(new Regex(s)) } catch { case ERROR(_) => None }
 
   def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
 
   def escape_regex(s: String): String =
     if (s.exists(is_regex_meta)) {
       (for (c <- s.iterator)
        yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
     }
     else s
 
 
   /* 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]) =
   {
     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] =
     take_suffix(pred, take_prefix(pred, xs)._2)._1
 
   def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
 
   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] =
   {
     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] =
   {
     val result = new mutable.ListBuffer[A]
     @tailrec def dups(rest: List[A]): Unit =
       rest match {
         case Nil =>
         case x :: xs =>
           if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x
           dups(xs)
       }
     dups(lst)
     result.toList
   }
 
   def replicate[A](n: Int, a: A): List[A] =
     if (n < 0) throw new IllegalArgumentException
     else if (n == 0) Nil
     else {
       val res = new mutable.ListBuffer[A]
       (1 to n).foreach(_ => res += a)
       res.toList
     }
 
   def the_single[A](xs: List[A]): A =
     xs match {
       case List(x) => x
       case _ => error("Single argument expected")
     }
 
 
   /* proper values */
 
   def proper_string(s: String): Option[String] =
     if (s == null || s == "") None else Some(s)
 
   def proper_list[A](list: List[A]): Option[List[A]] =
     if (list == null || list.isEmpty) None else Some(list)
 
 
   /* reflection */
 
   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)
         }
     }
     subclass(a)
   }
 }