diff --git a/src/Pure/General/bytes.scala b/src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala
+++ b/src/Pure/General/bytes.scala
@@ -1,235 +1,231 @@
 /*  Title:      Pure/General/bytes.scala
     Author:     Makarius
 
 Immutable byte vectors versus UTF8 strings.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
   OutputStream, InputStream, FileInputStream, FileOutputStream}
 import java.net.URL
 import java.util.Base64
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
 
 object Bytes {
   val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
 
   def apply(s: CharSequence): Bytes = {
     val str = s.toString
     if (str.isEmpty) empty
     else {
       val b = UTF8.bytes(str)
       new Bytes(b, 0, b.length)
     }
   }
 
   def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length)
 
   def apply(a: Array[Byte], offset: Int, length: Int): Bytes =
     if (length == 0) empty
     else {
       val b = new Array[Byte](length)
       System.arraycopy(a, offset, b, 0, length)
       new Bytes(b, 0, b.length)
     }
 
   val newline: Bytes = apply("\n")
 
 
   /* base64 */
 
   def decode_base64(s: String): Bytes = {
     val a = Base64.getDecoder.decode(s)
     new Bytes(a, 0, a.length)
   }
 
-  object Decode_Base64 extends Scala.Fun("decode_base64") with Scala.Fun_Single_Bytes {
+  object Decode_Base64 extends Scala.Fun_Bytes("decode_base64") {
     val here = Scala_Project.here
-    def invoke(args: List[Bytes]): List[Bytes] =
-      List(decode_base64(Library.the_single(args).text))
+    def apply(arg: Bytes): Bytes = decode_base64(arg.text)
   }
 
-  object Encode_Base64 extends Scala.Fun("encode_base64") with Scala.Fun_Single_Bytes {
+  object Encode_Base64 extends Scala.Fun_Bytes("encode_base64") {
     val here = Scala_Project.here
-    def invoke(args: List[Bytes]): List[Bytes] =
-      List(Bytes(Library.the_single(args).encode_base64))
+    def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
   }
 
 
   /* XZ compression */
 
-  object Compress extends Scala.Fun("compress") with Scala.Fun_Single_Bytes {
+  object Compress extends Scala.Fun_Bytes("compress") {
     val here = Scala_Project.here
-    def invoke(args: List[Bytes]): List[Bytes] =
-      List(Library.the_single(args).compress())
+    def apply(arg: Bytes): Bytes = arg.compress()
   }
 
-  object Uncompress extends Scala.Fun("uncompress") with Scala.Fun_Single_Bytes {
+  object Uncompress extends Scala.Fun_Bytes("uncompress") {
     val here = Scala_Project.here
-    def invoke(args: List[Bytes]): List[Bytes] =
-      List(Library.the_single(args).uncompress())
+    def apply(arg: Bytes): Bytes = arg.uncompress()
   }
 
 
   /* read */
 
   def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
     if (limit == 0) empty
     else {
       val out_size = (if (limit == Integer.MAX_VALUE) hint else limit) max 1024
       val out = new ByteArrayOutputStream(out_size)
       val buf = new Array[Byte](8192)
       var m = 0
 
       var cont = true
       while (cont) {
         m = stream.read(buf, 0, buf.length min (limit - out.size))
         if (m != -1) out.write(buf, 0, m)
         cont = (m != -1 && limit > out.size)
       }
 
       new Bytes(out.toByteArray, 0, out.size)
     }
 
   def read(file: JFile): Bytes = {
     val length = file.length
     val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
     using(new FileInputStream(file))(read_stream(_, limit = limit))
   }
 
   def read(path: Path): Bytes = read(path.file)
 
   def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
 
 
   /* write */
 
   def write(file: JFile, bytes: Bytes): Unit =
     using(new FileOutputStream(file))(bytes.write_stream(_))
 
   def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
 }
 
 final class Bytes private(
   protected val bytes: Array[Byte],
   protected val offset: Int,
   val length: Int) extends CharSequence {
   /* equality */
 
   override def equals(that: Any): Boolean = {
     that match {
       case other: Bytes =>
         if (this eq other) true
         else if (length != other.length) false
         else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
       case _ => false
     }
   }
 
   private lazy val hash: Int = {
     var h = 0
     for (i <- offset until offset + length) {
       val b = bytes(i).asInstanceOf[Int] & 0xFF
       h = 31 * h + b
     }
     h
   }
 
   override def hashCode(): Int = hash
 
 
   /* content */
 
   lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
   def is_empty: Boolean = length == 0
 
   def iterator: Iterator[Byte] =
     for (i <- (offset until (offset + length)).iterator)
       yield bytes(i)
 
   def array: Array[Byte] = {
     val a = new Array[Byte](length)
     System.arraycopy(bytes, offset, a, 0, length)
     a
   }
 
   def text: String = UTF8.decode_permissive(this)
 
   def encode_base64: String = {
     val b =
       if (offset == 0 && length == bytes.length) bytes
       else Bytes(bytes, offset, length).bytes
     Base64.getEncoder.encodeToString(b)
   }
 
   def maybe_encode_base64: (Boolean, String) = {
     val s = text
     if (this == Bytes(s)) (false, s) else (true, encode_base64)
   }
 
   override def toString: String = "Bytes(" + length + ")"
 
   def proper: Option[Bytes] = if (is_empty) None else Some(this)
   def proper_text: Option[String] = if (is_empty) None else Some(text)
 
   def +(other: Bytes): Bytes =
     if (other.is_empty) this
     else if (is_empty) other
     else {
       val new_bytes = new Array[Byte](length + other.length)
       System.arraycopy(bytes, offset, new_bytes, 0, length)
       System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
       new Bytes(new_bytes, 0, new_bytes.length)
     }
 
 
   /* CharSequence operations */
 
   def charAt(i: Int): Char =
     if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
     else throw new IndexOutOfBoundsException
 
   def subSequence(i: Int, j: Int): Bytes = {
     if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i)
     else throw new IndexOutOfBoundsException
   }
 
   def trim_line: Bytes =
     if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10)
       subSequence(0, length - 2)
     else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10))
       subSequence(0, length - 1)
     else this
 
 
   /* streams */
 
   def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length)
 
   def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length)
 
 
   /* XZ data compression */
 
   def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes =
     using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length))
 
   def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes = {
     val result = new ByteArrayOutputStream(length)
     using(new XZOutputStream(result, options, cache))(write_stream(_))
     new Bytes(result.toByteArray, 0, result.size)
   }
 
   def maybe_compress(
     options: XZ.Options = XZ.options(),
     cache: XZ.Cache = XZ.Cache()
   ) : (Boolean, Bytes) = {
     val compressed = compress(options = options, cache = cache)
     if (compressed.length < length) (true, compressed) else (false, this)
   }
 }
diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala
+++ b/src/Pure/System/scala.scala
@@ -1,335 +1,341 @@
 /*  Title:      Pure/System/scala.scala
     Author:     Makarius
 
 Support for Scala at runtime.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, StringWriter, PrintWriter}
 
 import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
 import scala.tools.nsc.interpreter.{IMain, Results}
 import scala.tools.nsc.interpreter.shell.ReplReporterImpl
 
 object Scala {
   /** registered functions **/
 
   abstract class Fun(val name: String, val thread: Boolean = false) {
     override def toString: String = name
     def single: Boolean = false
     def bytes: Boolean = false
     def position: Properties.T = here.position
     def here: Scala_Project.Here
     def invoke(args: List[Bytes]): List[Bytes]
   }
 
-  trait Fun_Single extends Fun { override def single: Boolean = true }
-  trait Fun_Bytes extends Fun { override def bytes: Boolean = true }
-  trait Fun_Single_Bytes extends Fun_Single with Fun_Bytes
+  trait Single_Fun extends Fun { override def single: Boolean = true }
+  trait Bytes_Fun extends Fun { override def bytes: Boolean = true }
 
   abstract class Fun_Strings(name: String, thread: Boolean = false)
   extends Fun(name, thread = thread) {
     override def invoke(args: List[Bytes]): List[Bytes] =
       apply(args.map(_.text)).map(Bytes.apply)
     def apply(args: List[String]): List[String]
   }
 
   abstract class Fun_String(name: String, thread: Boolean = false)
-  extends Fun_Strings(name, thread = thread) with Fun_Single {
+  extends Fun_Strings(name, thread = thread) with Single_Fun {
     override def apply(args: List[String]): List[String] =
       List(apply(Library.the_single(args)))
     def apply(arg: String): String
   }
 
+  abstract class Fun_Bytes(name: String, thread: Boolean = false)
+    extends Fun(name, thread = thread) with Single_Fun with Bytes_Fun {
+    override def invoke(args: List[Bytes]): List[Bytes] =
+      List(apply(Library.the_single(args)))
+    def apply(arg: Bytes): Bytes
+  }
+
   val encode_fun: XML.Encode.T[Fun] = { fun =>
     import XML.Encode._
     pair(string, pair(pair(bool, bool), properties))(
       fun.name, ((fun.single, fun.bytes), fun.position))
   }
 
   class Functions(val functions: Fun*) extends Isabelle_System.Service
 
   lazy val functions: List[Fun] =
     Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions)
 
 
 
   /** demo functions **/
 
   object Echo extends Fun_String("echo") {
     val here = Scala_Project.here
     def apply(arg: String): String = arg
   }
 
   object Sleep extends Fun_String("sleep") {
     val here = Scala_Project.here
     def apply(seconds: String): String = {
       val t =
         seconds match {
           case Value.Double(s) => Time.seconds(s)
           case _ => error("Malformed argument: " + quote(seconds))
         }
       val t0 = Time.now()
       t.sleep()
       val t1 = Time.now()
       (t1 - t0).toString
     }
   }
 
 
 
   /** compiler **/
 
   def class_path(): List[String] =
     for {
       prop <- List("isabelle.scala.classpath", "java.class.path")
       elems = System.getProperty(prop, "") if elems.nonEmpty
       elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty
     } yield elem
 
   object Compiler {
     def default_print_writer: PrintWriter =
       new NewLinePrintWriter(new ConsoleWriter, true)
 
     def context(
       print_writer: PrintWriter = default_print_writer,
       error: String => Unit = Exn.error,
       jar_dirs: List[JFile] = Nil,
       class_loader: Option[ClassLoader] = None
     ): Context = {
       def find_jars(dir: JFile): List[String] =
         File.find_files(dir, file => file.getName.endsWith(".jar")).
           map(File.absolute_name)
 
       val settings = new GenericRunnerSettings(error)
       settings.classpath.value =
         (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
 
       new Context(settings, print_writer, class_loader)
     }
 
     class Context private [Compiler](
       val settings: GenericRunnerSettings,
       val print_writer: PrintWriter,
       val class_loader: Option[ClassLoader]
     ) {
       override def toString: String = settings.toString
 
       val interp: IMain =
         new IMain(settings, new ReplReporterImpl(settings, print_writer)) {
           override def parentClassLoader: ClassLoader =
             class_loader getOrElse super.parentClassLoader
         }
     }
 
     def toplevel(interpret: Boolean, source: String): List[String] = {
       val out = new StringWriter
       val interp = Compiler.context(print_writer = new PrintWriter(out)).interp
       val marker = '\u000b'
       val ok =
         interp.withLabel(marker.toString) {
           if (interpret) interp.interpret(source) == Results.Success
           else (new interp.ReadEvalPrint).compile(source)
         }
       out.close()
 
       val Error = """(?s)^\S* error: (.*)$""".r
       val errors =
         space_explode(marker, Library.strip_ansi_color(out.toString)).
           collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
 
       if (!ok && errors.isEmpty) List("Error") else errors
     }
   }
 
   object Toplevel extends Fun_String("scala_toplevel") {
     val here = Scala_Project.here
     def apply(arg: String): String = {
       val (interpret, source) =
         YXML.parse_body(arg) match {
           case Nil => (false, "")
           case List(XML.Text(source)) => (false, source)
           case body => import XML.Decode._; pair(bool, string)(body)
         }
       val errors =
         try { Compiler.toplevel(interpret, source) }
         catch { case ERROR(msg) => List(msg) }
       locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
     }
   }
 
 
 
   /** interpreter thread **/
 
   object Interpreter {
     /* requests */
 
     sealed abstract class Request
     case class Execute(command: Compiler.Context => Unit) extends Request
     case object Shutdown extends Request
 
 
     /* known interpreters */
 
     private val known = Synchronized(Set.empty[Interpreter])
 
     def add(interpreter: Interpreter): Unit = known.change(_ + interpreter)
     def del(interpreter: Interpreter): Unit = known.change(_ - interpreter)
 
     def get[A](which: PartialFunction[Interpreter, A]): Option[A] =
       known.value.collectFirst(which)
   }
 
   class Interpreter(context: Compiler.Context) {
     interpreter =>
 
     private val running = Synchronized[Option[Thread]](None)
     def running_thread(thread: Thread): Boolean = running.value.contains(thread)
     def interrupt_thread(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt })
 
     private lazy val thread: Consumer_Thread[Interpreter.Request] =
       Consumer_Thread.fork("Scala.Interpreter") {
         case Interpreter.Execute(command) =>
           try {
             running.change(_ => Some(Thread.currentThread()))
             command(context)
           }
           finally {
             running.change(_ => None)
             Exn.Interrupt.dispose()
           }
           true
         case Interpreter.Shutdown =>
           Interpreter.del(interpreter)
           false
       }
 
     def shutdown(): Unit = {
       thread.send(Interpreter.Shutdown)
       interrupt_thread()
       thread.shutdown()
     }
 
     def execute(command: Compiler.Context => Unit): Unit =
       thread.send(Interpreter.Execute(command))
 
     Interpreter.add(interpreter)
     thread
   }
 
 
 
   /** invoke Scala functions from ML **/
 
   /* invoke function */
 
   object Tag extends Enumeration {
     val NULL, OK, ERROR, FAIL, INTERRUPT = Value
   }
 
   def function_thread(name: String): Boolean =
     functions.find(fun => fun.name == name) match {
       case Some(fun) => fun.thread
       case None => false
     }
 
   def function_body(name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) =
     functions.find(fun => fun.name == name) match {
       case Some(fun) =>
         Exn.capture { fun.invoke(args) } match {
           case Exn.Res(null) => (Tag.NULL, Nil)
           case Exn.Res(res) => (Tag.OK, res)
           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil)
           case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e))))
         }
       case None => (Tag.FAIL, List(Bytes("Unknown Isabelle/Scala function: " + quote(name))))
     }
 
 
   /* protocol handler */
 
   class Handler extends Session.Protocol_Handler {
     private var session: Session = null
     private var futures = Map.empty[String, Future[Unit]]
 
     override def init(session: Session): Unit =
       synchronized { this.session = session }
 
     override def exit(): Unit = synchronized {
       for ((id, future) <- futures) cancel(id, future)
       futures = Map.empty
     }
 
     private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit =
       synchronized {
         if (futures.isDefinedAt(id)) {
           session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res)
           futures -= id
         }
       }
 
     private def cancel(id: String, future: Future[Unit]): Unit = {
       future.cancel()
       result(id, Scala.Tag.INTERRUPT, Nil)
     }
 
     private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
       msg.properties match {
         case Markup.Invoke_Scala(name, id) =>
           def body(): Unit = {
             val (tag, res) = Scala.function_body(name, msg.chunks)
             result(id, tag, res)
           }
           val future =
             if (Scala.function_thread(name)) {
               Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body())
             }
             else Future.fork(body())
           futures += (id -> future)
           true
         case _ => false
       }
     }
 
     private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
       msg.properties match {
         case Markup.Cancel_Scala(id) =>
           futures.get(id) match {
             case Some(future) => cancel(id, future)
             case None =>
           }
           true
         case _ => false
       }
     }
 
     override val functions: Session.Protocol_Functions =
       List(
         Markup.Invoke_Scala.name -> invoke_scala,
         Markup.Cancel_Scala.name -> cancel_scala)
   }
 }
 
 class Scala_Functions extends Scala.Functions(
   Scala.Echo,
   Scala.Sleep,
   Scala.Toplevel,
   Bytes.Decode_Base64,
   Bytes.Encode_Base64,
   Bytes.Compress,
   Bytes.Uncompress,
   Doc.Doc_Names,
   Bibtex.Check_Database,
   Isabelle_System.Make_Directory,
   Isabelle_System.Copy_Dir,
   Isabelle_System.Copy_File,
   Isabelle_System.Copy_File_Base,
   Isabelle_System.Rm_Tree,
   Isabelle_System.Download,
   Isabelle_System.Isabelle_Id,
   Isabelle_Tool.Isabelle_Tools,
   isabelle.atp.SystemOnTPTP.List_Systems,
   isabelle.atp.SystemOnTPTP.Run_System)