diff --git a/src/Pure/General/linear_set.scala b/src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala
+++ b/src/Pure/General/linear_set.scala
@@ -1,159 +1,159 @@
 /*  Title:      Pure/General/linear_set.scala
     Author:     Makarius
     Author:     Fabian Immler, TU Munich
 
 Sets with canonical linear order, or immutable linked-lists.
 */
 
 package isabelle
 
 
 import scala.collection.SetLike
 import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
 import scala.collection.mutable.{Builder, SetBuilder}
 import scala.language.higherKinds
 
 
 object Linear_Set extends SetFactory[Linear_Set]
 {
   private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
   override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]]
 
   implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
   def newBuilder[A]: Builder[A, Linear_Set[A]] = new SetBuilder[A, Linear_Set[A]](empty[A])
 
   class Duplicate[A](x: A) extends Exception
   class Undefined[A](x: A) extends Exception
   class Next_Undefined[A](x: Option[A]) extends Exception
 }
 
 
 final class Linear_Set[A] private(
     start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
   extends scala.collection.immutable.Set[A]
   with GenericSetTemplate[A, Linear_Set]
   with SetLike[A, Linear_Set[A]]
 {
   override def companion: GenericCompanion[Linear_Set] = Linear_Set
 
 
   /* relative addressing */
 
   def next(elem: A): Option[A] =
     if (contains(elem)) nexts.get(elem)
     else throw new Linear_Set.Undefined(elem)
 
   def prev(elem: A): Option[A] =
     if (contains(elem)) prevs.get(elem)
     else throw new Linear_Set.Undefined(elem)
 
   def get_after(hook: Option[A]): Option[A] =
     hook match {
       case None => start
       case Some(elem) => next(elem)
     }
 
   def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
     if (contains(elem)) throw new Linear_Set.Duplicate(elem)
     else
       hook match {
         case None =>
           start match {
             case None => new Linear_Set[A](Some(elem), Some(elem), Map(), Map())
             case Some(elem1) =>
               new Linear_Set[A](Some(elem), end,
                 nexts + (elem -> elem1), prevs + (elem1 -> elem))
           }
         case Some(elem1) =>
           if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
           else
             nexts.get(elem1) match {
               case None =>
                 new Linear_Set[A](start, Some(elem),
                   nexts + (elem1 -> elem), prevs + (elem -> elem1))
               case Some(elem2) =>
                 new Linear_Set[A](start, end,
                   nexts + (elem1 -> elem) + (elem -> elem2),
                   prevs + (elem2 -> elem) + (elem -> elem1))
             }
       }
 
   def append_after(hook: Option[A], elems: Traversable[A]): Linear_Set[A] =  // FIXME reverse fold
     ((hook, this) /: elems) {
       case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
     }._2
 
   def delete_after(hook: Option[A]): Linear_Set[A] =
     hook match {
       case None =>
         start match {
           case None => throw new Linear_Set.Next_Undefined[A](None)
           case Some(elem1) =>
             nexts.get(elem1) match {
               case None => empty
               case Some(elem2) =>
                 new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2)
             }
         }
       case Some(elem1) =>
         if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
         else
           nexts.get(elem1) match {
             case None => throw new Linear_Set.Next_Undefined(Some(elem1))
             case Some(elem2) =>
               nexts.get(elem2) match {
                 case None =>
                   new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2)
                 case Some(elem3) =>
                   new Linear_Set[A](start, end,
                     nexts - elem2 + (elem1 -> elem3),
                     prevs - elem2 + (elem3 -> elem1))
               }
           }
     }
 
 
   /* Set methods */
 
   override def stringPrefix = "Linear_Set"
 
-  override def isEmpty: Boolean = !start.isDefined
+  override def isEmpty: Boolean = start.isEmpty
   override def size: Int = if (isEmpty) 0 else nexts.size + 1
 
   def contains(elem: A): Boolean =
     nonEmpty && (end.get == elem || nexts.isDefinedAt(elem))
 
   private def make_iterator(from: Option[A]): Iterator[A] = new Iterator[A] {
     private var next_elem = from
     def hasNext(): Boolean = next_elem.isDefined
     def next(): A =
       next_elem match {
         case Some(elem) =>
           next_elem = nexts.get(elem)
           elem
         case None => Iterator.empty.next()
       }
   }
 
   override def iterator: Iterator[A] = make_iterator(start)
 
   def iterator(elem: A): Iterator[A] =
     if (contains(elem)) make_iterator(Some(elem))
     else throw new Linear_Set.Undefined(elem)
 
   def iterator(from: A, to: A): Iterator[A] =
     if (contains(to))
       nexts.get(to) match {
         case None => iterator(from)
         case Some(stop) => iterator(from).takeWhile(_ != stop)
       }
     else throw new Linear_Set.Undefined(to)
 
   def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
 
   override def last: A = reverse.head
 
   def + (elem: A): Linear_Set[A] = insert_after(end, elem)
 
   def - (elem: A): Linear_Set[A] = delete_after(prev(elem))
 }
diff --git a/src/Pure/General/mercurial.scala b/src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala
+++ b/src/Pure/General/mercurial.scala
@@ -1,335 +1,335 @@
 /*  Title:      Pure/General/mercurial.scala
     Author:     Makarius
 
 Support for Mercurial repositories, with local or remote repository clone
 and working directory (via ssh connection).
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 import scala.annotation.tailrec
 import scala.collection.mutable
 
 
 object Mercurial
 {
   type Graph = isabelle.Graph[String, Unit]
 
 
   /* command-line syntax */
 
   def optional(s: String, prefix: String = ""): String =
     if (s == "") "" else " " + prefix + " " + Bash.string(s)
 
   def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
   def opt_rev(s: String): String = optional(s, "--rev")
   def opt_template(s: String): String = optional(s, "--template")
 
 
   /* repository access */
 
   def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =
     ssh.is_dir(root + Path.explode(".hg")) &&
     new Repository(root, ssh).command("root").ok
 
   def repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
   {
     val hg = new Repository(root, ssh)
     hg.command("root").check
     hg
   }
 
   def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
   {
     def find(root: Path): Option[Repository] =
       if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
       else if (root.is_root) None
       else find(root + Path.parent)
 
     find(ssh.expand_path(start))
   }
 
   private def make_repository(root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local)
     : Repository =
   {
     val hg = new Repository(root, ssh)
     ssh.mkdirs(hg.root.dir)
     hg.command(cmd, args, repository = false).check
     hg
   }
 
   def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
     make_repository(root, "init", ssh.bash_path(root), ssh = ssh)
 
   def clone_repository(source: String, root: Path,
       rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
     make_repository(root, "clone",
       options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
 
   def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
   {
     if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
     else clone_repository(source, root, options = "--noupdate", ssh = ssh)
   }
 
   class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local)
   {
     hg =>
 
     val root: Path = ssh.expand_path(root_path)
     def root_url: String = ssh.hg_url + root.implode
 
     override def toString: String = ssh.prefix + root.implode
 
     def command(name: String, args: String = "", options: String = "",
       repository: Boolean = true): Process_Result =
     {
       val cmdline =
         "export HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
           (if (repository) " --repository " + ssh.bash_path(root) else "") +
           " --noninteractive " + name + " " + options + " " + args
       ssh.execute(cmdline)
     }
 
     def add(files: List[Path]): Unit =
       hg.command("add", files.map(ssh.bash_path(_)).mkString(" "))
 
     def archive(target: String, rev: String = "", options: String = ""): Unit =
       hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
 
     def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
       hg.command("heads", opt_template(template), options).check.out_lines
 
     def identify(rev: String = "tip", options: String = ""): String =
       hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
 
     def id(rev: String = "tip"): String = identify(rev, options = "-i")
 
     def paths(args: String = "", options: String = ""): List[String] =
       hg.command("paths", args = args, options = options).check.out_lines
 
     def manifest(rev: String = "", options: String = ""): List[String] =
       hg.command("manifest", opt_rev(rev), options).check.out_lines
 
     def log(rev: String = "", template: String = "", options: String = ""): String =
       hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
 
     def parent(): String = log(rev = "p1()", template = "{node|short}")
 
     def push(remote: String = "", rev: String = "", force: Boolean = false, options: String = "")
     {
       hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
         check_rc(rc => rc == 0 | rc == 1)
     }
 
     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
       hg.command("pull", opt_rev(rev) + optional(remote), options).check
 
     def update(
       rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
     {
       hg.command("update",
         opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
     }
 
     def known_files(): List[String] =
       hg.command("status", options = "--modified --added --clean --no-status").check.out_lines
 
     def graph(): Graph =
     {
       val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
       val log_result =
         log(template = """node: {node|short} {p1node|short} {p2node|short}\n""")
       (Graph.string[Unit] /: split_lines(log_result)) {
         case (graph, Node(x, y, z)) =>
           val deps = List(y, z).filterNot(s => s.forall(_ == '0'))
           val graph1 = (graph /: (x :: deps))(_.default_node(_, ()))
           (graph1 /: deps)({ case (g, dep) => g.add_edge(dep, x) })
         case (graph, _) => graph
       }
     }
   }
 
 
   /* check files */
 
   def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) =
   {
     val outside = new mutable.ListBuffer[Path]
     val unknown = new mutable.ListBuffer[Path]
 
     @tailrec def check(paths: List[Path])
     {
       paths match {
         case path :: rest =>
           find_repository(path, ssh) match {
             case None => outside += path; check(rest)
             case Some(hg) =>
               val known =
                 hg.known_files().iterator.map(name =>
                   (hg.root + Path.explode(name)).canonical_file).toSet
               if (!known(path.canonical_file)) unknown += path
               check(rest.filterNot(p => known(p.canonical_file)))
           }
         case Nil =>
       }
     }
 
     check(files)
     (outside.toList, unknown.toList)
   }
 
 
   /* setup remote vs. local repository */
 
   private def edit_hgrc(local_hg: Repository, path_name: String, source: String)
   {
     val hgrc = local_hg.root + Path.explode(".hg/hgrc")
     def header(line: String): Boolean = line.startsWith("[paths]")
     val Entry = """^(\S+)\s*=\s*(.*)$""".r
     val new_entry = path_name + " = " + source
 
     def commit(lines: List[String]): Boolean =
     {
       File.write(hgrc, cat_lines(lines))
       true
     }
     val edited =
       hgrc.is_file && {
         val lines = split_lines(File.read(hgrc))
-        lines.filter(header).length == 1 && {
+        lines.count(header) == 1 && {
           if (local_hg.paths(options = "-q").contains(path_name)) {
             val old_source = local_hg.paths(args = path_name).head
             val old_entry = path_name + ".old = " + old_source
             val lines1 =
               lines.map {
                 case Entry(a, b) if a == path_name && b == old_source =>
                   new_entry + "\n" + old_entry
                 case line => line
               }
             lines != lines1 && commit(lines1)
           }
           else {
             val prefix = lines.takeWhile(line => !header(line))
             val n = prefix.length
             commit(prefix ::: List(lines(n), new_entry) ::: lines.drop(n + 1))
           }
         }
       }
     if (!edited) File.append(hgrc, "\n[paths]\n" + new_entry + "\n")
   }
 
   val default_path_name = "default"
 
   def hg_setup(
     remote: String,
     local_path: Path,
     remote_name: String = "",
     path_name: String = default_path_name,
     remote_exists: Boolean = false,
     progress: Progress = No_Progress)
   {
     /* local repository */
 
     Isabelle_System.mkdirs(local_path)
 
     val repos_name =
       proper_string(remote_name) getOrElse local_path.absolute.base.implode
 
     val local_hg =
       if (is_repository(local_path)) repository(local_path)
       else init_repository(local_path)
 
     progress.echo("Local repository " + local_hg.root.absolute)
 
 
     /* remote repository */
 
     val remote_url =
       remote match {
         case _ if remote.startsWith("ssh://") =>
           val ssh_url = remote + "/" + repos_name
 
           if (!remote_exists) {
             try { local_hg.command("init", ssh_url, repository = false).check }
             catch { case ERROR(msg) => progress.echo_warning(msg) }
           }
 
           ssh_url
 
         case SSH.Target(user, host) =>
           val phabricator = Phabricator.API(user, host)
 
           var repos =
             phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
               if (remote_exists) {
                 error("Remote repository " +
                   quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
               }
               else phabricator.create_repository(repos_name, short_name = repos_name)
             }
 
           while (repos.importing) {
             progress.echo("Awaiting remote repository ...")
             Thread.sleep(500)
             repos = phabricator.the_repository(repos.phid)
           }
 
           repos.ssh_url
 
         case _ => error("Malformed remote specification " + quote(remote))
       }
 
     progress.echo("Remote repository " + quote(remote_url))
 
 
     /* synchronize local and remote state */
 
     progress.echo("Synchronizing ...")
 
     edit_hgrc(local_hg, path_name, remote_url)
 
     local_hg.pull(options = "-u")
 
     local_hg.push(remote = remote_url)
   }
 
   val isabelle_tool =
     Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository", args =>
     {
       var remote_name = ""
       var path_name = default_path_name
       var remote_exists = false
 
       val getopts = Getopts("""
 Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
 
   Options are:
     -n NAME      remote repository name (default: base name of LOCAL_DIR)
     -p PATH      Mercurial path name (default: """ + quote(default_path_name) + """)
     -r           assume that remote repository already exists
 
   Setup a remote vs. local Mercurial repository: REMOTE either refers to a
   Phabricator server "user@host" or SSH file server "ssh://user@host/path".
 """,
         "n:" -> (arg => remote_name = arg),
         "p:" -> (arg => path_name = arg),
         "r" -> (_ => remote_exists = true))
 
       val more_args = getopts(args)
 
       val (remote, local_path) =
         more_args match {
           case List(arg1, arg2) => (arg1, Path.explode(arg2))
           case _ => getopts.usage()
         }
 
       val progress = new Console_Progress
 
       hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name,
         remote_exists = remote_exists, progress = progress)
     })
 }
diff --git a/src/Pure/General/path.scala b/src/Pure/General/path.scala
--- a/src/Pure/General/path.scala
+++ b/src/Pure/General/path.scala
@@ -1,260 +1,260 @@
 /*  Title:      Pure/General/path.scala
     Author:     Makarius
 
 Algebra of file-system paths: basic POSIX notation, extended by named
 roots (e.g. //foo) and variables (e.g. $BAR).
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 import scala.util.matching.Regex
 
 
 object Path
 {
   /* path elements */
 
   sealed abstract class Elem
   private case class Root(name: String) extends Elem
   private case class Basic(name: String) extends Elem
   private case class Variable(name: String) extends Elem
   private case object Parent extends Elem
 
   private def err_elem(msg: String, s: String): Nothing =
     error(msg + " path element " + quote(s))
 
   private val illegal_elem = Set("", "~", "~~", ".", "..")
   private val illegal_char = "/\\$:\"'<>|?*"
 
   private def check_elem(s: String): String =
     if (illegal_elem.contains(s)) err_elem("Illegal", s)
     else {
       for (c <- s) {
         if (c.toInt < 32)
           err_elem("Illegal control character " + c.toInt + " in", s)
         if (illegal_char.contains(c))
           err_elem("Illegal character " + quote(c.toString) + " in", s)
       }
       s
     }
 
   private def root_elem(s: String): Elem = Root(check_elem(s))
   private def basic_elem(s: String): Elem = Basic(check_elem(s))
   private def variable_elem(s: String): Elem = Variable(check_elem(s))
 
   private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] =
     (y, xs) match {
       case (Root(_), _) => List(y)
       case (Parent, Root(_) :: _) => xs
       case (Parent, Basic(_) :: rest) => rest
       case _ => y :: xs
     }
 
   private def norm_elems(elems: List[Elem]): List[Elem] =
     (elems :\ (Nil: List[Elem]))(apply_elem)
 
   private def implode_elem(elem: Elem, short: Boolean): String =
     elem match {
       case Root("") => ""
       case Root(s) => "//" + s
       case Basic(s) => s
       case Variable("USER_HOME") if short => "~"
       case Variable("ISABELLE_HOME") if short => "~~"
       case Variable(s) => "$" + s
       case Parent => ".."
     }
 
 
   /* path constructors */
 
   val current: Path = new Path(Nil)
   val root: Path = new Path(List(Root("")))
   def named_root(s: String): Path = new Path(List(root_elem(s)))
   def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem(_)))
   def basic(s: String): Path = new Path(List(basic_elem(s)))
   def variable(s: String): Path = new Path(List(variable_elem(s)))
   val parent: Path = new Path(List(Parent))
 
 
   /* explode */
 
   def explode(str: String): Path =
   {
     def explode_elem(s: String): Elem =
       try {
         if (s == "..") Parent
         else if (s == "~") Variable("USER_HOME")
         else if (s == "~~") Variable("ISABELLE_HOME")
         else if (s.startsWith("$")) variable_elem(s.substring(1))
         else basic_elem(s)
       }
       catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) }
   
     val ss = space_explode('/', str)
     val r = ss.takeWhile(_.isEmpty).length
     val es = ss.dropWhile(_.isEmpty)
     val (roots, raw_elems) =
       if (r == 0) (Nil, es)
       else if (r == 1) (List(Root("")), es)
       else if (es.isEmpty) (List(Root("")), Nil)
       else (List(root_elem(es.head)), es.tail)
     val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
 
     new Path(norm_elems(elems reverse_::: roots))
   }
 
   def is_wellformed(str: String): Boolean =
     try { explode(str); true } catch { case ERROR(_) => false }
 
   def is_valid(str: String): Boolean =
     try { explode(str).expand; true } catch { case ERROR(_) => false }
 
   def split(str: String): List[Path] =
     space_explode(':', str).filterNot(_.isEmpty).map(explode)
 
 
   /* encode */
 
   val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
 
 
   /* reserved names */
 
   private val reserved_windows: Set[String] =
     Set("CON", "PRN", "AUX", "NUL",
       "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9",
       "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9")
 
   def is_reserved(name: String): Boolean =
     Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a)))
 
 
   /* case-insensitive names */
 
   def check_case_insensitive(paths: List[Path])
   {
     val table =
       (Multi_Map.empty[String, String] /: paths)({ case (tab, path) =>
         val name = path.expand.implode
         tab.insert(Word.lowercase(name), name)
       })
     val collisions =
       (for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten
     if (collisions.nonEmpty) {
       error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n  "))
     }
   }
 }
 
 
 final class Path private(private val elems: List[Path.Elem]) // reversed elements
 {
   def is_current: Boolean = elems.isEmpty
   def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
   def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }
   def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
 
   def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))
 
 
   /* implode */
 
   private def gen_implode(short: Boolean): String =
     elems match {
       case Nil => "."
       case List(Path.Root("")) => "/"
       case _ => elems.map(Path.implode_elem(_, short)).reverse.mkString("/")
     }
   def implode: String = gen_implode(false)
   def implode_short: String = gen_implode(true)
 
   override def toString: String = quote(implode)
 
 
   /* base element */
 
   private def split_path: (Path, String) =
     elems match {
       case Path.Basic(s) :: xs => (new Path(xs), s)
       case _ => error("Cannot split path into dir/base: " + toString)
     }
 
   def dir: Path = split_path._1
   def base: Path = new Path(List(Path.Basic(split_path._2)))
 
   def ext(e: String): Path =
     if (e == "") this
     else {
       val (prfx, s) = split_path
       prfx + Path.basic(s + "." + e)
     }
 
   def backup: Path =
   {
     val (prfx, s) = split_path
     prfx + Path.basic(s + "~")
   }
 
   def backup2: Path =
   {
     val (prfx, s) = split_path
     prfx + Path.basic(s + "~~")
   }
 
   private val Ext = new Regex("(.*)\\.([^.]*)")
 
   def split_ext: (Path, String) =
   {
     val (prefix, base) = split_path
     base match {
       case Ext(b, e) => (prefix + Path.basic(b), e)
       case _ => (prefix + Path.basic(base), "")
     }
   }
 
   def drop_ext: Path = split_ext._1
   def get_ext: String = split_ext._2
 
 
   /* expand */
 
   def expand_env(env: Map[String, String]): Path =
   {
     def eval(elem: Path.Elem): List[Path.Elem] =
       elem match {
         case Path.Variable(s) =>
           val path = Path.explode(Isabelle_System.getenv_strict(s, env))
           if (path.elems.exists(_.isInstanceOf[Path.Variable]))
             error("Illegal path variable nesting: " + s + "=" + path.toString)
           else path.elems
         case x => List(x)
       }
 
-    new Path(Path.norm_elems(elems.map(eval).flatten))
+    new Path(Path.norm_elems(elems.flatMap(eval)))
   }
 
   def expand: Path = expand_env(Isabelle_System.settings())
 
   def file_name: String = expand.base.implode
 
 
   /* source position */
 
   def position: Position.T = Position.File(implode)
 
 
   /* platform files */
 
   def file: JFile = File.platform_file(this)
   def is_file: Boolean = file.isFile
   def is_dir: Boolean = file.isDirectory
 
   def absolute_file: JFile = File.absolute(file)
   def canonical_file: JFile = File.canonical(file)
 
   def absolute: Path = File.path(absolute_file)
   def canonical: Path = File.path(canonical_file)
 }
diff --git a/src/Pure/General/scan.scala b/src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala
+++ b/src/Pure/General/scan.scala
@@ -1,512 +1,512 @@
 /*  Title:      Pure/General/scan.scala
     Author:     Makarius
 
 Efficient scanning of keywords and tokens.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.collection.{IndexedSeq, Traversable, TraversableOnce}
 import scala.collection.immutable.PagedSeq
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition,
   Reader, CharSequenceReader}
 import scala.util.parsing.combinator.RegexParsers
 
 import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream}
 import java.net.URL
 
 
 object Scan
 {
   /** context of partial line-oriented scans **/
 
   abstract class Line_Context
   case object Finished extends Line_Context
   case class Quoted(quote: String) extends Line_Context
   case object Verbatim extends Line_Context
   case class Cartouche(depth: Int) extends Line_Context
   case class Comment_Prefix(symbol: Symbol.Symbol) extends Line_Context
   case class Cartouche_Comment(depth: Int) extends Line_Context
   case class Comment(depth: Int) extends Line_Context
 
 
 
   /** parser combinators **/
 
   object Parsers extends Parsers
 
   trait Parsers extends RegexParsers
   {
     override val whiteSpace = "".r
 
 
     /* optional termination */
 
     def opt_term[T](p: => Parser[T]): Parser[Option[T]] =
       p ^^ (x => Some(x)) | """\z""".r ^^ (_ => None)
 
 
     /* repeated symbols */
 
     def repeated(pred: Symbol.Symbol => Boolean, min_count: Int, max_count: Int): Parser[String] =
       new Parser[String]
       {
         def apply(in: Input) =
         {
           val start = in.offset
           val end = in.source.length
           val matcher = new Symbol.Matcher(in.source)
 
           var i = start
           var count = 0
           var finished = false
           while (!finished && i < end && count < max_count) {
             val n = matcher(i, end)
             val sym = in.source.subSequence(i, i + n).toString
             if (pred(sym)) { i += n; count += 1 }
             else finished = true
           }
           if (count < min_count) Failure("bad input", in)
           else Success(in.source.subSequence(start, i).toString, in.drop(i - start))
         }
       }.named("repeated")
 
     def one(pred: Symbol.Symbol => Boolean): Parser[String] =
       repeated(pred, 1, 1)
 
     def maybe(pred: Symbol.Symbol => Boolean): Parser[String] =
       repeated(pred, 0, 1)
 
     def many(pred: Symbol.Symbol => Boolean): Parser[String] =
       repeated(pred, 0, Integer.MAX_VALUE)
 
     def many1(pred: Symbol.Symbol => Boolean): Parser[String] =
       repeated(pred, 1, Integer.MAX_VALUE)
 
 
     /* character */
 
     def character(pred: Char => Boolean): Symbol.Symbol => Boolean =
       (s: Symbol. Symbol) => s.length == 1 && pred(s.charAt(0))
 
 
     /* quoted strings */
 
     private def quoted_body(quote: Symbol.Symbol): Parser[String] =
     {
       rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" |
         ("""\\\d\d\d""".r ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString)
     }
 
     def quoted(quote: Symbol.Symbol): Parser[String] =
     {
       quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z }
     }.named("quoted")
 
     def quoted_content(quote: Symbol.Symbol, source: String): String =
     {
       require(parseAll(quoted(quote), source).successful)
       val body = source.substring(1, source.length - 1)
       if (body.exists(_ == '\\')) {
         val content =
           rep(many1(sym => sym != quote && sym != "\\") |
               "\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString }))
         parseAll(content ^^ (_.mkString), body).get
       }
       else body
     }
 
     def quoted_line(quote: Symbol.Symbol, ctxt: Line_Context): Parser[(String, Line_Context)] =
     {
       ctxt match {
         case Finished =>
           quote ~ quoted_body(quote) ~ opt_term(quote) ^^
             { case x ~ y ~ Some(z) => (x + y + z, Finished)
               case x ~ y ~ None => (x + y, Quoted(quote)) }
         case Quoted(q) if q == quote =>
           quoted_body(quote) ~ opt_term(quote) ^^
             { case x ~ Some(y) => (x + y, Finished)
               case x ~ None => (x, ctxt) }
         case _ => failure("")
       }
     }.named("quoted_line")
 
     def recover_quoted(quote: Symbol.Symbol): Parser[String] =
       quote ~ quoted_body(quote) ^^ { case x ~ y => x + y }
 
 
     /* verbatim text */
 
     private def verbatim_body: Parser[String] =
       rep(many1(sym => sym != "*") | """\*(?!\})""".r) ^^ (_.mkString)
 
     def verbatim: Parser[String] =
     {
       "{*" ~ verbatim_body ~ "*}" ^^ { case x ~ y ~ z => x + y + z }
     }.named("verbatim")
 
     def verbatim_content(source: String): String =
     {
       require(parseAll(verbatim, source).successful)
       source.substring(2, source.length - 2)
     }
 
     def verbatim_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
     {
       ctxt match {
         case Finished =>
           "{*" ~ verbatim_body ~ opt_term("*}") ^^
             { case x ~ y ~ Some(z) => (x + y + z, Finished)
               case x ~ y ~ None => (x + y, Verbatim) }
         case Verbatim =>
           verbatim_body ~ opt_term("*}") ^^
             { case x ~ Some(y) => (x + y, Finished)
               case x ~ None => (x, Verbatim) }
         case _ => failure("")
       }
     }.named("verbatim_line")
 
     val recover_verbatim: Parser[String] =
       "{*" ~ verbatim_body ^^ { case x ~ y => x + y }
 
 
     /* nested text cartouches */
 
     def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
     {
       require(depth >= 0)
 
       def apply(in: Input) =
       {
         val start = in.offset
         val end = in.source.length
         val matcher = new Symbol.Matcher(in.source)
 
         var i = start
         var d = depth
         var finished = false
         while (!finished && i < end) {
           val n = matcher(i, end)
           val sym = in.source.subSequence(i, i + n).toString
           if (Symbol.is_open(sym)) { i += n; d += 1 }
           else if (Symbol.is_close(sym) && d > 0) { i += n; d -= 1; if (d == 0) finished = true }
           else if (d > 0) i += n
           else finished = true
         }
         if (i == start) Failure("bad input", in)
         else Success((in.source.subSequence(start, i).toString, d), in.drop(i - start))
       }
     }.named("cartouche_depth")
 
     def cartouche: Parser[String] =
       cartouche_depth(0) ^? { case (x, d) if d == 0 => x }
 
     def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
     {
       def cartouche_context(d: Int): Line_Context =
         if (d == 0) Finished else Cartouche(d)
 
       ctxt match {
         case Finished =>
           cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) }
         case Cartouche(depth) =>
           cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) }
         case _ => failure("")
       }
     }
 
     val recover_cartouche: Parser[String] =
       cartouche_depth(0) ^^ (_._1)
 
     def cartouche_content(source: String): String =
     {
       def err(): Nothing = error("Malformed text cartouche: " + quote(source))
       val source1 =
         Library.try_unprefix(Symbol.open_decoded, source) orElse
           Library.try_unprefix(Symbol.open, source) getOrElse err()
       Library.try_unsuffix(Symbol.close_decoded, source1) orElse
         Library.try_unsuffix(Symbol.close, source1) getOrElse err()
     }
 
 
     /* nested comments */
 
     private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
     {
       require(depth >= 0)
 
       val comment_text =
         rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r)
 
       def apply(in: Input) =
       {
         var rest = in
         def try_parse[A](p: Parser[A]): Boolean =
         {
           parse(p ^^^ (()), rest) match {
             case Success(_, next) => { rest = next; true }
             case _ => false
           }
         }
         var d = depth
         var finished = false
         while (!finished) {
           if (try_parse("(*")) d += 1
           else if (d > 0 && try_parse("*)")) { d -= 1; if (d == 0) finished = true }
           else if (d == 0 || !try_parse(comment_text)) finished = true
         }
         if (in.offset < rest.offset)
           Success((in.source.subSequence(in.offset, rest.offset).toString, d), rest)
         else Failure("comment expected", in)
       }
     }.named("comment_depth")
 
     def comment: Parser[String] =
       comment_depth(0) ^? { case (x, d) if d == 0 => x }
 
     def comment_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
     {
       val depth =
         ctxt match {
           case Finished => 0
           case Comment(d) => d
           case _ => -1
         }
       if (depth >= 0)
         comment_depth(depth) ^^
           { case (x, 0) => (x, Finished)
             case (x, d) => (x, Comment(d)) }
       else failure("")
     }
 
     val recover_comment: Parser[String] =
       comment_depth(0) ^^ (_._1)
 
     def comment_content(source: String): String =
     {
       require(parseAll(comment, source).successful)
       source.substring(2, source.length - 2)
     }
 
 
     /* keyword */
 
     def literal(lexicon: Lexicon): Parser[String] = new Parser[String]
     {
       def apply(in: Input) =
       {
         val result = lexicon.scan(in)
         if (result.isEmpty) Failure("keyword expected", in)
         else Success(result, in.drop(result.length))
       }
     }.named("keyword")
   }
 
 
 
   /** Lexicon -- position tree **/
 
   object Lexicon
   {
     /* representation */
 
     private sealed case class Tree(branches: Map[Char, (String, Tree)])
     private val empty_tree = Tree(Map())
 
     val empty: Lexicon = new Lexicon(empty_tree)
     def apply(elems: String*): Lexicon = empty ++ elems
   }
 
   final class Lexicon private(rep: Lexicon.Tree)
   {
     /* auxiliary operations */
 
     private def dest(tree: Lexicon.Tree, result: List[String]): List[String] =
       (result /: tree.branches.toList) ((res, entry) =>
         entry match { case (_, (s, tr)) =>
           if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) })
 
     private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
     {
       val len = str.length
       @tailrec def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
       {
         if (i < len) {
           tree.branches.get(str.charAt(i)) match {
             case Some((s, tr)) => look(tr, s.nonEmpty, i + 1)
             case None => None
           }
         }
         else Some(tip, tree)
       }
       look(rep, false, 0)
     }
 
     def completions(str: CharSequence): List[String] =
       lookup(str) match {
         case Some((true, tree)) => dest(tree, List(str.toString))
         case Some((false, tree)) => dest(tree, Nil)
         case None => Nil
       }
 
 
     /* pseudo Set methods */
 
     def raw_iterator: Iterator[String] = dest(rep, Nil).iterator
     def iterator: Iterator[String] = dest(rep, Nil).sorted.iterator
 
     override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
 
     def is_empty: Boolean = rep.branches.isEmpty
 
     def contains(elem: String): Boolean =
       lookup(elem) match {
         case Some((tip, _)) => tip
         case _ => false
       }
 
 
     /* build lexicon */
 
     def + (elem: String): Lexicon =
       if (contains(elem)) this
       else {
         val len = elem.length
         def extend(tree: Lexicon.Tree, i: Int): Lexicon.Tree =
           if (i < len) {
             val c = elem.charAt(i)
             val end = (i + 1 == len)
             tree.branches.get(c) match {
               case Some((s, tr)) =>
                 Lexicon.Tree(tree.branches +
                   (c -> (if (end) elem else s, extend(tr, i + 1))))
               case None =>
                 Lexicon.Tree(tree.branches +
                   (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
             }
           }
           else tree
         new Lexicon(extend(rep, 0))
       }
 
     def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
 
     def ++ (other: Lexicon): Lexicon =
       if (this eq other) this
       else if (is_empty) other
       else this ++ other.raw_iterator
 
     def -- (remove: Traversable[String]): Lexicon =
       if (remove.exists(contains(_)))
         Lexicon.empty ++ iterator.filterNot(a => remove.exists(b => a == b))
       else this
 
 
     /* scan */
 
     def scan(in: Reader[Char]): String =
     {
       val source = in.source
       val offset = in.offset
       val len = source.length - offset
 
-      def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String =
+      @tailrec def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String =
       {
         if (i < len) {
           tree.branches.get(source.charAt(offset + i)) match {
             case Some((s, tr)) => scan_tree(tr, if (s.isEmpty) result else s, i + 1)
             case None => result
           }
         }
         else result
       }
       scan_tree(rep, "", 0)
     }
   }
 
 
 
   /** read stream without decoding: efficient length operation **/
 
   private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int)
     extends CharSequence
   {
     def charAt(i: Int): Char =
       if (0 <= i && i < length) seq(start + i)
       else throw new IndexOutOfBoundsException
 
     def length: Int = end - start  // avoid expensive seq.length
 
     def subSequence(i: Int, j: Int): CharSequence =
       if (0 <= i && i <= j && j <= length) new Restricted_Seq(seq, start + i, start + j)
       else throw new IndexOutOfBoundsException
 
     override def toString: String =
     {
       val buf = new StringBuilder(length)
       for (offset <- start until end) buf.append(seq(offset))
       buf.toString
     }
   }
 
   abstract class Byte_Reader extends Reader[Char] with AutoCloseable
 
   private def make_byte_reader(stream: InputStream, stream_length: Int): Byte_Reader =
   {
     val buffered_stream = new BufferedInputStream(stream)
     val seq = new PagedSeq(
       (buf: Array[Char], offset: Int, length: Int) =>
         {
           var i = 0
           var c = 0
           var eof = false
           while (!eof && i < length) {
             c = buffered_stream.read
             if (c == -1) eof = true
             else { buf(offset + i) = c.toChar; i += 1 }
           }
           if (i > 0) i else -1
         })
     val restricted_seq = new Restricted_Seq(seq, 0, stream_length)
 
     class Paged_Reader(override val offset: Int) extends Byte_Reader
     {
       override lazy val source: CharSequence = restricted_seq
       def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\u001a'
       def rest: Paged_Reader = if (seq.isDefinedAt(offset)) new Paged_Reader(offset + 1) else this
       def pos: InputPosition = new OffsetPosition(source, offset)
       def atEnd: Boolean = !seq.isDefinedAt(offset)
       override def drop(n: Int): Paged_Reader = new Paged_Reader(offset + n)
       def close { buffered_stream.close }
     }
     new Paged_Reader(0)
   }
 
   def byte_reader(file: JFile): Byte_Reader =
     make_byte_reader(new FileInputStream(file), file.length.toInt)
 
   def byte_reader(url: URL): Byte_Reader =
   {
     val connection = url.openConnection
     val stream = connection.getInputStream
     val stream_length = connection.getContentLength
     make_byte_reader(stream, stream_length)
   }
 
   def reader_is_utf8(reader: Reader[Char]): Boolean =
     reader.isInstanceOf[Byte_Reader]
 
   def reader_decode_utf8(is_utf8: Boolean, s: String): String =
     if (is_utf8) UTF8.decode_permissive(s) else s
 
   def reader_decode_utf8(reader: Reader[Char], s: String): String =
     reader_decode_utf8(reader_is_utf8(reader), s)
 
 
   /* plain text reader */
 
   def char_reader(text: CharSequence): CharSequenceReader =
     new CharSequenceReader(text)
 }
diff --git a/src/Pure/General/ssh.scala b/src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala
+++ b/src/Pure/General/ssh.scala
@@ -1,484 +1,484 @@
 /*  Title:      Pure/General/ssh.scala
     Author:     Makarius
 
 SSH client based on JSch (see also http://www.jcraft.com/jsch/examples).
 */
 
 package isabelle
 
 
 import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
 
 import scala.collection.mutable
 
 import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
   OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS}
 
 
 object SSH
 {
   /* target machine: user@host syntax */
 
   object Target
   {
     val User_Host = "^([^@]+)@(.+)$".r
 
     def parse(s: String): (String, String) =
       s match {
         case User_Host(user, host) => (user, host)
         case _ => ("", s)
       }
 
     def unapplySeq(s: String): Option[List[String]] =
       parse(s) match {
         case (_, "") => None
         case (user, host) => Some(List(user, host))
       }
   }
 
   val default_port = 22
   def make_port(port: Int): Int = if (port > 0) port else default_port
 
   def connect_timeout(options: Options): Int =
     options.seconds("ssh_connect_timeout").ms.toInt
 
   def alive_interval(options: Options): Int =
     options.seconds("ssh_alive_interval").ms.toInt
 
   def alive_count_max(options: Options): Int =
     options.int("ssh_alive_count_max")
 
 
   /* init context */
 
   def init_context(options: Options): Context =
   {
     val config_dir = Path.explode(options.string("ssh_config_dir"))
     if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
 
     val jsch = new JSch
 
     val config_file = Path.explode(options.string("ssh_config_file"))
     if (config_file.is_file)
       jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
 
     val known_hosts = config_dir + Path.explode("known_hosts")
     if (!known_hosts.is_file) known_hosts.file.createNewFile
     jsch.setKnownHosts(File.platform_path(known_hosts))
 
     val identity_files =
       space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
     for (identity_file <- identity_files if identity_file.is_file)
       jsch.addIdentity(File.platform_path(identity_file))
 
     new Context(options, jsch)
   }
 
   def open_session(options: Options, host: String, user: String = "", port: Int = 0,
       proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
       permissive: Boolean = false): Session =
     init_context(options).open_session(host = host, user = user, port = port,
       proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
       permissive = permissive)
 
   class Context private[SSH](val options: Options, val jsch: JSch)
   {
     def update_options(new_options: Options): Context = new Context(new_options, jsch)
 
     def connect_session(host: String, user: String = "", port: Int = 0,
       host_key_permissive: Boolean = false,
       host_key_alias: String = "",
       on_close: () => Unit = () => ()): Session =
     {
-      val session = jsch.getSession(proper_string(user) getOrElse null, host, make_port(port))
+      val session = jsch.getSession(proper_string(user).orNull, host, make_port(port))
 
       session.setUserInfo(No_User_Info)
       session.setServerAliveInterval(alive_interval(options))
       session.setServerAliveCountMax(alive_count_max(options))
       session.setConfig("MaxAuthTries", "3")
       if (host_key_permissive) session.setConfig("StrictHostKeyChecking", "no")
       if (host_key_alias != "") session.setHostKeyAlias(host_key_alias)
 
       if (options.bool("ssh_compression")) {
         session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
         session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
         session.setConfig("compression_level", "9")
       }
       session.connect(connect_timeout(options))
       new Session(options, session, on_close)
     }
 
     def open_session(host: String, user: String = "", port: Int = 0,
       proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
       permissive: Boolean = false): Session =
     {
       if (proxy_host == "") connect_session(host = host, user = user, port = port)
       else {
         val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user)
 
         val fw =
           try { proxy.port_forwarding(remote_host = host, remote_port = make_port(port)) }
           catch { case exn: Throwable => proxy.close; throw exn }
 
         try {
           connect_session(host = fw.local_host, port = fw.local_port,
             host_key_permissive = permissive, host_key_alias = host,
             user = user, on_close = () => { fw.close; proxy.close })
         }
         catch { case exn: Throwable => fw.close; proxy.close; throw exn }
       }
     }
   }
 
 
   /* logging */
 
   def logging(verbose: Boolean = true, debug: Boolean = false)
   {
     JSch.setLogger(if (verbose) new Logger(debug) else null)
   }
 
   private class Logger(debug: Boolean) extends JSch_Logger
   {
     def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug
 
     def log(level: Int, msg: String)
     {
       level match {
         case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)
         case JSch_Logger.WARN => Output.warning(msg)
         case _ => Output.writeln(msg)
       }
     }
   }
 
 
   /* user info */
 
   object No_User_Info extends UserInfo
   {
     def getPassphrase: String = null
     def getPassword: String = null
     def promptPassword(msg: String): Boolean = false
     def promptPassphrase(msg: String): Boolean = false
     def promptYesNo(msg: String): Boolean = false
     def showMessage(msg: String): Unit = Output.writeln(msg)
   }
 
 
   /* port forwarding */
 
   object Port_Forwarding
   {
     def open(ssh: Session, ssh_close: Boolean,
       local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding =
     {
       val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port)
       new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port)
     }
   }
 
   class Port_Forwarding private[SSH](
     ssh: SSH.Session,
     ssh_close: Boolean,
     val local_host: String,
     val local_port: Int,
     val remote_host: String,
     val remote_port: Int) extends AutoCloseable
   {
     override def toString: String =
       local_host + ":" + local_port + ":" + remote_host + ":" + remote_port
 
     def close()
     {
       ssh.session.delPortForwardingL(local_host, local_port)
       if (ssh_close) ssh.close()
     }
   }
 
 
   /* Sftp channel */
 
   type Attrs = SftpATTRS
 
   sealed case class Dir_Entry(name: String, is_dir: Boolean)
   {
     def is_file: Boolean = !is_dir
   }
 
 
   /* exec channel */
 
   private val exec_wait_delay = Time.seconds(0.3)
 
   class Exec private[SSH](session: Session, channel: ChannelExec) extends AutoCloseable
   {
     override def toString: String = "exec " + session.toString
 
     def close() { channel.disconnect }
 
     val exit_status: Future[Int] =
       Future.thread("ssh_wait") {
         while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms)
         channel.getExitStatus
       }
 
     val stdin: OutputStream = channel.getOutputStream
     val stdout: InputStream = channel.getInputStream
     val stderr: InputStream = channel.getErrStream
 
     // connect after preparing streams
     channel.connect(connect_timeout(session.options))
 
     def result(
       progress_stdout: String => Unit = (_: String) => (),
       progress_stderr: String => Unit = (_: String) => (),
       strict: Boolean = true): Process_Result =
     {
       stdin.close
 
       def read_lines(stream: InputStream, progress: String => Unit): List[String] =
       {
         val result = new mutable.ListBuffer[String]
         val line_buffer = new ByteArrayOutputStream(100)
         def line_flush()
         {
           val line = Library.trim_line(line_buffer.toString(UTF8.charset_name))
           progress(line)
           result += line
           line_buffer.reset
         }
 
         var c = 0
         var finished = false
         while (!finished) {
           while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c)
           if (c == 10) line_flush()
           else if (channel.isClosed) {
             if (line_buffer.size > 0) line_flush()
             finished = true
           }
           else Thread.sleep(exec_wait_delay.ms)
         }
 
         result.toList
       }
 
       val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) }
       val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) }
 
       def terminate()
       {
         close
         out_lines.join
         err_lines.join
         exit_status.join
       }
 
       val rc =
         try { exit_status.join }
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 
       close
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join)
     }
   }
 
 
   /* session */
 
   class Session private[SSH](
     val options: Options,
     val session: JSch_Session,
     on_close: () => Unit) extends System with AutoCloseable
   {
     def update_options(new_options: Options): Session =
       new Session(new_options, session, on_close)
 
     def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@"
     def host: String = if (session.getHost == null) "" else session.getHost
     def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort
     override def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/"
 
     override def prefix: String =
       user_prefix + host + port_suffix + ":"
 
     override def toString: String =
       user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)")
 
 
     /* port forwarding */
 
     def port_forwarding(
         remote_port: Int, remote_host: String = "localhost",
         local_port: Int = 0, local_host: String = "localhost",
         ssh_close: Boolean = false): Port_Forwarding =
       Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port)
 
 
     /* sftp channel */
 
     val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
     sftp.connect(connect_timeout(options))
 
     def close() { sftp.disconnect; session.disconnect; on_close() }
 
     val settings: Map[String, String] =
     {
       val home = sftp.getHome
       Map("HOME" -> home, "USER_HOME" -> home)
     }
     override def expand_path(path: Path): Path = path.expand_env(settings)
     def remote_path(path: Path): String = expand_path(path).implode
     override def bash_path(path: Path): String = Bash.string(remote_path(path))
 
     def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path))
     def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2))
     def rm(path: Path): Unit = sftp.rm(remote_path(path))
     def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path))
     def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path))
 
     private def test_entry(path: Path, as_dir: Boolean): Boolean =
       try {
         val is_dir = sftp.stat(remote_path(path)).isDir
         if (as_dir) is_dir else !is_dir
       }
       catch { case _: SftpException => false }
 
     override def is_dir(path: Path): Boolean = test_entry(path, true)
     override def is_file(path: Path): Boolean = test_entry(path, false)
 
     def is_link(path: Path): Boolean =
       try { sftp.lstat(remote_path(path)).isLink }
       catch { case _: SftpException => false }
 
     override def mkdirs(path: Path): Unit =
       if (!is_dir(path)) {
         execute(
           "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
         if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path)))
       }
 
     def read_dir(path: Path): List[Dir_Entry] =
     {
       if (!is_dir(path)) error("No such directory: " + path.toString)
 
       val dir_name = remote_path(path)
       val dir = sftp.ls(dir_name)
       (for {
         i <- (0 until dir.size).iterator
         a = dir.get(i).asInstanceOf[AnyRef]
         name = Untyped.get[String](a, "filename")
         attrs = Untyped.get[Attrs](a, "attrs")
         if name != "." && name != ".."
       }
       yield {
         Dir_Entry(name,
           if (attrs.isLink) {
             try { sftp.stat(dir_name + "/" + name).isDir }
             catch { case _: SftpException => false }
           }
           else attrs.isDir)
       }).toList.sortBy(_.name)
     }
 
     def find_files(
       start: Path,
       pred: Path => Boolean = _ => true,
       include_dirs: Boolean = false,
       follow_links: Boolean = false): List[Path] =
     {
       val result = new mutable.ListBuffer[Path]
       def check(path: Path) { if (pred(path)) result += path }
 
       def find(dir: Path)
       {
         if (include_dirs) check(dir)
         if (follow_links || !is_link(dir)) {
           for (entry <- read_dir(dir)) {
             val path = dir + Path.basic(entry.name)
             if (entry.is_file) check(path) else find(path)
           }
         }
       }
       if (is_file(start)) check(start) else find(start)
 
       result.toList
     }
 
     def open_input(path: Path): InputStream = sftp.get(remote_path(path))
     def open_output(path: Path): OutputStream = sftp.put(remote_path(path))
 
     def read_file(path: Path, local_path: Path): Unit =
       sftp.get(remote_path(path), File.platform_path(local_path))
     def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
     def read(path: Path): String = using(open_input(path))(File.read_stream(_))
 
     def write_file(path: Path, local_path: Path): Unit =
       sftp.put(File.platform_path(local_path), remote_path(path))
     def write_bytes(path: Path, bytes: Bytes): Unit =
       using(open_output(path))(bytes.write_stream(_))
     def write(path: Path, text: String): Unit =
       using(open_output(path))(stream => Bytes(text).write_stream(stream))
 
 
     /* exec channel */
 
     def exec(command: String): Exec =
     {
       val channel = session.openChannel("exec").asInstanceOf[ChannelExec]
       channel.setCommand("export USER_HOME=\"$HOME\"\n" + command)
       new Exec(this, channel)
     }
 
     override def execute(command: String,
         progress_stdout: String => Unit = (_: String) => (),
         progress_stderr: String => Unit = (_: String) => (),
         strict: Boolean = true): Process_Result =
       exec(command).result(progress_stdout, progress_stderr, strict)
 
 
     /* tmp dirs */
 
     def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
 
     def rm_tree(remote_dir: String): Unit =
       execute("rm -r -f " + Bash.string(remote_dir)).check
 
     def tmp_dir(): String =
       execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
 
     def with_tmp_dir[A](body: Path => A): A =
     {
       val remote_dir = tmp_dir()
       try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
     }
   }
 
 
 
   /* system operations */
 
   trait System
   {
     def hg_url: String = ""
     def prefix: String = ""
 
     def expand_path(path: Path): Path = path.expand
     def bash_path(path: Path): String = File.bash_path(path)
     def is_dir(path: Path): Boolean = path.is_dir
     def is_file(path: Path): Boolean = path.is_file
     def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)
 
     def execute(command: String,
         progress_stdout: String => Unit = (_: String) => (),
         progress_stderr: String => Unit = (_: String) => (),
         strict: Boolean = true): Process_Result =
       Isabelle_System.bash(command, progress_stdout = progress_stdout,
         progress_stderr = progress_stderr, strict = strict)
   }
 
   object Local extends System
 }
diff --git a/src/Pure/General/symbol.scala b/src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala
+++ b/src/Pure/General/symbol.scala
@@ -1,658 +1,657 @@
 /*  Title:      Pure/General/symbol.scala
     Author:     Makarius
 
 Isabelle text symbols.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 import scala.util.matching.Regex
 import scala.annotation.tailrec
 
 
 object Symbol
 {
   type Symbol = String
 
   // counting Isabelle symbols, starting from 1
   type Offset = Text.Offset
   type Range = Text.Range
 
 
   /* spaces */
 
   val space = " "
 
   private val static_spaces = space * 4000
 
   def spaces(n: Int): String =
   {
     require(n >= 0)
     if (n < static_spaces.length) static_spaces.substring(0, n)
     else space * n
   }
 
 
   /* ASCII characters */
 
   def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
 
   def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
 
   def is_ascii_hex(c: Char): Boolean =
     '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
 
   def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''
 
   def is_ascii_blank(c: Char): Boolean = " \t\n\u000b\f\r".contains(c)
 
   def is_ascii_line_terminator(c: Char): Boolean = "\r\n".contains(c)
 
   def is_ascii_letdig(c: Char): Boolean =
     is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)
 
   def is_ascii_identifier(s: String): Boolean =
     s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig)
 
   def ascii(c: Char): Symbol =
   {
     if (c > 127) error("Non-ASCII character: " + quote(c.toString))
     else char_symbols(c.toInt)
   }
 
   def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128
 
 
   /* symbol matching */
 
   private val symbol_total = new Regex("""(?xs)
     [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""")
 
   private def is_plain(c: Char): Boolean =
     !(c == '\r' || c == '\\' || Character.isHighSurrogate(c))
 
   def is_malformed(s: Symbol): Boolean =
     s.length match {
       case 1 =>
         val c = s(0)
         Character.isHighSurrogate(c) || Character.isLowSurrogate(c) || c == '\ufffd'
       case 2 =>
         val c1 = s(0)
         val c2 = s(1)
         !(c1 == '\r' && c2 == '\n' || Character.isSurrogatePair(c1, c2))
       case _ => !s.endsWith(">") || s == "\\<>" || s == "\\<^>"
     }
 
   def is_newline(s: Symbol): Boolean =
     s == "\n" || s == "\r" || s == "\r\n"
 
   class Matcher(text: CharSequence)
   {
     private val matcher = symbol_total.pattern.matcher(text)
     def apply(start: Int, end: Int): Int =
     {
       require(0 <= start && start < end && end <= text.length)
       if (is_plain(text.charAt(start))) 1
       else {
         matcher.region(start, end).lookingAt
         matcher.group.length
       }
     }
   }
 
 
   /* iterator */
 
   private val char_symbols: Array[Symbol] =
     (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
 
   def iterator(text: CharSequence): Iterator[Symbol] =
     new Iterator[Symbol]
     {
       private val matcher = new Matcher(text)
       private var i = 0
       def hasNext = i < text.length
       def next =
       {
         val n = matcher(i, text.length)
         val s =
           if (n == 0) ""
           else if (n == 1) {
             val c = text.charAt(i)
             if (c < char_symbols.length) char_symbols(c)
             else text.subSequence(i, i + n).toString
           }
           else text.subSequence(i, i + n).toString
         i += n
         s
       }
     }
 
   def explode(text: CharSequence): List[Symbol] = iterator(text).toList
 
   def length(text: CharSequence): Int = iterator(text).length
 
   def trim_blanks(text: CharSequence): String =
     Library.trim(is_blank(_), explode(text)).mkString
 
   def all_blank(str: String): Boolean =
     iterator(str).forall(is_blank(_))
 
   def trim_blank_lines(text: String): String =
     cat_lines(split_lines(text).dropWhile(all_blank).reverse.dropWhile(all_blank).reverse)
 
 
   /* decoding offsets */
 
   object Index
   {
     private sealed case class Entry(chr: Int, sym: Int)
 
     val empty: Index = new Index(Nil)
 
     def apply(text: CharSequence): Index =
     {
       val matcher = new Matcher(text)
       val buf = new mutable.ListBuffer[Entry]
       var chr = 0
       var sym = 0
       while (chr < text.length) {
         val n = matcher(chr, text.length)
         chr += n
         sym += 1
         if (n > 1) buf += Entry(chr, sym)
       }
       if (buf.isEmpty) empty else new Index(buf.toList)
     }
   }
 
   final class Index private(entries: List[Index.Entry])
   {
     private val hash: Int = entries.hashCode
     private val index: Array[Index.Entry] = entries.toArray
 
     def decode(symbol_offset: Offset): Text.Offset =
     {
       val sym = symbol_offset - 1
       val end = index.length
       @tailrec def bisect(a: Int, b: Int): Int =
       {
         if (a < b) {
           val c = (a + b) / 2
           if (sym < index(c).sym) bisect(a, c)
           else if (c + 1 == end || sym < index(c + 1).sym) c
           else bisect(c + 1, b)
         }
         else -1
       }
       val i = bisect(0, end)
       if (i < 0) sym
       else index(i).chr + sym - index(i).sym
     }
     def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
 
     override def hashCode: Int = hash
     override def equals(that: Any): Boolean =
       that match {
         case other: Index => index.sameElements(other.index)
         case _ => false
       }
   }
 
 
   /* symbolic text chunks -- without actual text */
 
   object Text_Chunk
   {
     sealed abstract class Name
     case object Default extends Name
     case class Id(id: Document_ID.Generic) extends Name
     case class File(name: String) extends Name
 
     val encode_name: XML.Encode.T[Name] =
     {
       import XML.Encode._
       variant(List(
         { case Default => (Nil, Nil) },
         { case Id(a) => (List(long_atom(a)), Nil) },
         { case File(a) => (List(a), Nil) }))
     }
 
     val decode_name: XML.Decode.T[Name] =
     {
       import XML.Decode._
       variant(List(
         { case (Nil, Nil) => Default },
         { case (List(a), Nil) => Id(long_atom(a)) },
         { case (List(a), Nil) => File(a) }))
     }
 
     def apply(text: CharSequence): Text_Chunk =
       new Text_Chunk(Text.Range(0, text.length), Index(text))
   }
 
   final class Text_Chunk private(val range: Text.Range, private val index: Index)
   {
     override def hashCode: Int = (range, index).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Text_Chunk =>
           range == other.range &&
           index == other.index
         case _ => false
       }
 
     override def toString: String = "Text_Chunk" + range.toString
 
     def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset)
     def decode(symbol_range: Range): Text.Range = index.decode(symbol_range)
     def incorporate(symbol_range: Range): Option[Text.Range] =
     {
       def in(r: Range): Option[Text.Range] =
         range.try_restrict(decode(r)) match {
           case Some(r1) if !r1.is_singularity => Some(r1)
           case _ => None
         }
      in(symbol_range) orElse in(symbol_range - 1)
     }
   }
 
 
   /* recoding text */
 
   private class Recoder(list: List[(String, String)])
   {
     private val (min, max) =
     {
       var min = '\uffff'
       var max = '\u0000'
       for ((x, _) <- list) {
         val c = x(0)
         if (c < min) min = c
         if (c > max) max = c
       }
       (min, max)
     }
     private val table =
     {
       var tab = Map[String, String]()
       for ((x, y) <- list) {
         tab.get(x) match {
           case None => tab += (x -> y)
           case Some(z) =>
             error("Duplicate symbol mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z))
         }
       }
       tab
     }
     def recode(text: String): String =
     {
       val len = text.length
       val matcher = symbol_total.pattern.matcher(text)
       val result = new StringBuilder(len)
       var i = 0
       while (i < len) {
         val c = text(i)
         if (min <= c && c <= max) {
           matcher.region(i, len).lookingAt
           val x = matcher.group
           result.append(table.getOrElse(x, x))
           i = matcher.end
         }
         else { result.append(c); i += 1 }
       }
       result.toString
     }
   }
 
 
 
   /** symbol interpretation **/
 
   val ARGUMENT_CARTOUCHE = "cartouche"
   val ARGUMENT_SPACE_CARTOUCHE = "space_cartouche"
 
   private lazy val symbols =
   {
     val contents =
       for (path <- Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS")) if path.is_file)
         yield (File.read(path))
     new Interpretation(cat_lines(contents))
   }
 
   private class Interpretation(symbols_spec: String)
   {
     /* read symbols */
 
     private val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
     private val Key = new Regex("""(?xs) (.+): """)
 
     private def read_decl(decl: String): (Symbol, Properties.T) =
     {
       def err() = error("Bad symbol declaration: " + decl)
 
       def read_props(props: List[String]): Properties.T =
       {
         props match {
           case Nil => Nil
           case _ :: Nil => err()
           case Key(x) :: y :: rest => (x -> y.replace('\u2423', ' ')) :: read_props(rest)
           case _ => err()
         }
       }
       decl.split("\\s+").toList match {
         case sym :: props if sym.length > 1 && !is_malformed(sym) =>
           (sym, read_props(props))
         case _ => err()
       }
     }
 
     private val symbols: List[(Symbol, Properties.T)] =
       (((List.empty[(Symbol, Properties.T)], Set.empty[Symbol]) /:
           split_lines(symbols_spec).reverse)
         { case (res, No_Decl()) => res
           case ((list, known), decl) =>
             val (sym, props) = read_decl(decl)
             if (known(sym)) (list, known)
             else ((sym, props) :: list, known + sym)
         })._1
 
 
     /* basic properties */
 
     val properties: Map[Symbol, Properties.T] = Map(symbols: _*)
 
     val names: Map[Symbol, (String, String)] =
     {
       val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
       val Argument = new Properties.String("argument")
       def argument(sym: Symbol, props: Properties.T): String =
         props match {
           case Argument(arg) =>
             if (arg == ARGUMENT_CARTOUCHE || arg == ARGUMENT_SPACE_CARTOUCHE) arg
             else error("Bad argument: " + quote(arg) + " for symbol " + quote(sym))
           case _ => ""
         }
       Map((for ((sym @ Name(a), props) <- symbols) yield sym -> (a, argument(sym, props))): _*)
     }
 
     val groups: List[(String, List[Symbol])] =
-      symbols.map({ case (sym, props) =>
+      symbols.flatMap({ case (sym, props) =>
         val gs = for (("group", g) <- props) yield g
         if (gs.isEmpty) List(sym -> "unsorted") else gs.map(sym -> _)
-      }).flatten
-        .groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
+      }).groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
         .sortBy(_._1)
 
     val abbrevs: Multi_Map[Symbol, String] =
       Multi_Map((
         for {
           (sym, props) <- symbols
           ("abbrev", a) <- props.reverse
         } yield sym -> a): _*)
 
     val codes: List[(Symbol, Int)] =
     {
       val Code = new Properties.String("code")
       for {
         (sym, props) <- symbols
         code <-
           props match {
             case Code(s) =>
               try { Some(Integer.decode(s).intValue) }
               catch { case _: NumberFormatException => error("Bad code for symbol " + sym) }
             case _ => None
           }
       } yield {
         if (code < 128) error("Illegal ASCII code for symbol " + sym)
         else (sym, code)
       }
     }
 
 
     /* recoding */
 
     private val (decoder, encoder) =
     {
       val mapping =
         for ((sym, code) <- codes) yield (sym, new String(Character.toChars(code)))
       (new Recoder(mapping), new Recoder(for ((x, y) <- mapping) yield (y, x)))
     }
 
     def decode(text: String): String = decoder.recode(text)
     def encode(text: String): String = encoder.recode(text)
 
     private def recode_set(elems: String*): Set[String] =
     {
       val content = elems.toList
       Set((content ::: content.map(decode)): _*)
     }
 
     private def recode_map[A](elems: (String, A)*): Map[String, A] =
     {
       val content = elems.toList
       Map((content ::: content.map({ case (sym, a) => (decode(sym), a) })): _*)
     }
 
 
     /* user fonts */
 
     private val Font = new Properties.String("font")
     val fonts: Map[Symbol, String] =
       recode_map((for ((sym, Font(font)) <- symbols) yield sym -> font): _*)
 
     val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
-    val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
+    val font_index: Map[String, Int] = Map((font_names zip font_names.indices.toList): _*)
 
 
     /* classification */
 
     val letters = recode_set(
       "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
       "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
       "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
       "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z",
 
       "\\<A>", "\\<B>", "\\<C>", "\\<D>", "\\<E>", "\\<F>", "\\<G>",
       "\\<H>", "\\<I>", "\\<J>", "\\<K>", "\\<L>", "\\<M>", "\\<N>",
       "\\<O>", "\\<P>", "\\<Q>", "\\<R>", "\\<S>", "\\<T>", "\\<U>",
       "\\<V>", "\\<W>", "\\<X>", "\\<Y>", "\\<Z>", "\\<a>", "\\<b>",
       "\\<c>", "\\<d>", "\\<e>", "\\<f>", "\\<g>", "\\<h>", "\\<i>",
       "\\<j>", "\\<k>", "\\<l>", "\\<m>", "\\<n>", "\\<o>", "\\<p>",
       "\\<q>", "\\<r>", "\\<s>", "\\<t>", "\\<u>", "\\<v>", "\\<w>",
       "\\<x>", "\\<y>", "\\<z>",
 
       "\\<AA>", "\\<BB>", "\\<CC>", "\\<DD>", "\\<EE>", "\\<FF>",
       "\\<GG>", "\\<HH>", "\\<II>", "\\<JJ>", "\\<KK>", "\\<LL>",
       "\\<MM>", "\\<NN>", "\\<OO>", "\\<PP>", "\\<QQ>", "\\<RR>",
       "\\<SS>", "\\<TT>", "\\<UU>", "\\<VV>", "\\<WW>", "\\<XX>",
       "\\<YY>", "\\<ZZ>", "\\<aa>", "\\<bb>", "\\<cc>", "\\<dd>",
       "\\<ee>", "\\<ff>", "\\<gg>", "\\<hh>", "\\<ii>", "\\<jj>",
       "\\<kk>", "\\<ll>", "\\<mm>", "\\<nn>", "\\<oo>", "\\<pp>",
       "\\<qq>", "\\<rr>", "\\<ss>", "\\<tt>", "\\<uu>", "\\<vv>",
       "\\<ww>", "\\<xx>", "\\<yy>", "\\<zz>",
 
       "\\<alpha>", "\\<beta>", "\\<gamma>", "\\<delta>", "\\<epsilon>",
       "\\<zeta>", "\\<eta>", "\\<theta>", "\\<iota>", "\\<kappa>",
       "\\<mu>", "\\<nu>", "\\<xi>", "\\<pi>", "\\<rho>", "\\<sigma>",
       "\\<tau>", "\\<upsilon>", "\\<phi>", "\\<chi>", "\\<psi>",
       "\\<omega>", "\\<Gamma>", "\\<Delta>", "\\<Theta>", "\\<Lambda>",
       "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
       "\\<Psi>", "\\<Omega>")
 
     val blanks = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n")
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
 
     val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
 
 
     /* misc symbols */
 
     val newline_decoded = decode(newline)
     val comment_decoded = decode(comment)
     val cancel_decoded = decode(cancel)
     val latex_decoded = decode(latex)
     val marker_decoded = decode(marker)
     val open_decoded = decode(open)
     val close_decoded = decode(close)
 
 
     /* control symbols */
 
     val control_decoded: Set[Symbol] =
       Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
 
     val sub_decoded = decode(sub)
     val sup_decoded = decode(sup)
     val bold_decoded = decode(bold)
     val emph_decoded = decode(emph)
     val bsub_decoded = decode(bsub)
     val esub_decoded = decode(esub)
     val bsup_decoded = decode(bsup)
     val esup_decoded = decode(esup)
   }
 
 
   /* tables */
 
   def properties: Map[Symbol, Properties.T] = symbols.properties
   def names: Map[Symbol, (String, String)] = symbols.names
   def groups: List[(String, List[Symbol])] = symbols.groups
   def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs
   def codes: List[(Symbol, Int)] = symbols.codes
   def groups_code: List[(String, List[Symbol])] =
   {
     val has_code = codes.iterator.map(_._1).toSet
     groups.flatMap({ case (group, symbols) =>
       val symbols1 = symbols.filter(has_code)
       if (symbols1.isEmpty) None else Some((group, symbols1))
     })
   }
 
   lazy val is_code: Int => Boolean = codes.map(_._2).toSet
   def decode(text: String): String = symbols.decode(text)
   def encode(text: String): String = symbols.encode(text)
 
   def decode_yxml(text: String): XML.Body = YXML.parse_body(decode(text))
   def decode_yxml_failsafe(text: String): XML.Body = YXML.parse_body_failsafe(decode(text))
   def encode_yxml(body: XML.Body): String = encode(YXML.string_of_body(body))
 
   def decode_strict(text: String): String =
   {
     val decoded = decode(text)
     if (encode(decoded) == text) decoded
     else {
       val bad = new mutable.ListBuffer[Symbol]
       for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s))
         bad += s
       error("Bad Unicode symbols in text: " + commas_quote(bad))
     }
   }
 
   def fonts: Map[Symbol, String] = symbols.fonts
   def font_names: List[String] = symbols.font_names
   def font_index: Map[String, Int] = symbols.font_index
   def lookup_font(sym: Symbol): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
 
 
   /* classification */
 
   def is_letter(sym: Symbol): Boolean = symbols.letters.contains(sym)
   def is_digit(sym: Symbol): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
   def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'"
   def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
   def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
 
 
   /* symbolic newline */
 
   val newline: Symbol = "\\<newline>"
   def newline_decoded: Symbol = symbols.newline_decoded
 
   def print_newlines(str: String): String =
     if (str.contains('\n'))
       (for (s <- iterator(str)) yield { if (s == "\n") newline_decoded else s }).mkString
     else str
 
 
   /* formal comments */
 
   val comment: Symbol = "\\<comment>"
   val cancel: Symbol = "\\<^cancel>"
   val latex: Symbol = "\\<^latex>"
   val marker: Symbol = "\\<^marker>"
 
   def comment_decoded: Symbol = symbols.comment_decoded
   def cancel_decoded: Symbol = symbols.cancel_decoded
   def latex_decoded: Symbol = symbols.latex_decoded
   def marker_decoded: Symbol = symbols.marker_decoded
 
 
   /* cartouches */
 
   val open: Symbol = "\\<open>"
   val close: Symbol = "\\<close>"
 
   def open_decoded: Symbol = symbols.open_decoded
   def close_decoded: Symbol = symbols.close_decoded
 
   def is_open(sym: Symbol): Boolean = sym == open_decoded || sym == open
   def is_close(sym: Symbol): Boolean = sym == close_decoded || sym == close
 
   def cartouche(s: String): String = open + s + close
   def cartouche_decoded(s: String): String = open_decoded + s + close_decoded
 
 
   /* symbols for symbolic identifiers */
 
   private def raw_symbolic(sym: Symbol): Boolean =
     sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
 
   def is_symbolic(sym: Symbol): Boolean =
     !is_open(sym) && !is_close(sym) && (raw_symbolic(sym) || symbols.symbolic.contains(sym))
 
   def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
 
 
   /* control symbols */
 
   val control_prefix = "\\<^"
   val control_suffix = ">"
 
   def control_name(sym: Symbol): Option[String] =
     if (is_control_encoded(sym))
       Some(sym.substring(control_prefix.length, sym.length - control_suffix.length))
     else None
 
   def is_control_encoded(sym: Symbol): Boolean =
     sym.startsWith(control_prefix) && sym.endsWith(control_suffix)
 
   def is_control(sym: Symbol): Boolean =
     is_control_encoded(sym) || symbols.control_decoded.contains(sym)
 
   def is_controllable(sym: Symbol): Boolean =
     !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) &&
     !is_malformed(sym) && sym != "\""
 
   val sub = "\\<^sub>"
   val sup = "\\<^sup>"
   val bold = "\\<^bold>"
   val emph = "\\<^emph>"
   val bsub = "\\<^bsub>"
   val esub = "\\<^esub>"
   val bsup = "\\<^bsup>"
   val esup = "\\<^esup>"
 
   def sub_decoded: Symbol = symbols.sub_decoded
   def sup_decoded: Symbol = symbols.sup_decoded
   def bold_decoded: Symbol = symbols.bold_decoded
   def emph_decoded: Symbol = symbols.emph_decoded
   def bsub_decoded: Symbol = symbols.bsub_decoded
   def esub_decoded: Symbol = symbols.esub_decoded
   def bsup_decoded: Symbol = symbols.bsup_decoded
   def esup_decoded: Symbol = symbols.esup_decoded
 }
diff --git a/src/Pure/ML/ml_console.scala b/src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala
+++ b/src/Pure/ML/ml_console.scala
@@ -1,84 +1,84 @@
 /*  Title:      Pure/ML/ml_console.scala
     Author:     Makarius
 
 The raw ML process in interactive mode.
 */
 
 package isabelle
 
 
 object ML_Console
 {
   /* command line entry point */
 
   def main(args: Array[String])
   {
     Command_Line.tool {
       var dirs: List[Path] = Nil
       var include_sessions: List[String] = Nil
       var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
       var modes: List[String] = Nil
       var no_build = false
       var options = Options.init()
       var raw_ml_system = false
 
       val getopts = Getopts("""
 Usage: isabelle console [OPTIONS]
 
   Options are:
     -d DIR       include session directory
     -i NAME      include session in name-space of theories
     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
     -m MODE      add print mode for output
     -n           no build of session image on startup
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -r           bootstrap from raw Poly/ML
 
   Build a logic session image and run the raw Isabelle ML process
   in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
   quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
 """,
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
         "l:" -> (arg => logic = arg),
         "m:" -> (arg => modes = arg :: modes),
         "n" -> (arg => no_build = true),
         "o:" -> (arg => options = options + arg),
         "r" -> (_ => raw_ml_system = true))
 
       val more_args = getopts(args)
-      if (!more_args.isEmpty) getopts.usage()
+      if (more_args.nonEmpty) getopts.usage()
 
 
       // build logic
       if (!no_build && !raw_ml_system) {
         val progress = new Console_Progress()
         val rc =
           progress.interrupt_handler {
             Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs)
           }
         if (rc != 0) sys.exit(rc)
       }
 
       // process loop
       val process =
         ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
           modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
           raw_ml_system = raw_ml_system,
           store = Some(Sessions.store(options)),
           session_base =
             if (raw_ml_system) None
             else Some(Sessions.base_info(
               options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
 
       val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _))
       val process_result = Future.thread[Int]("process_result") {
         val rc = process.join
         tty_loop.cancel  // FIXME does not quite work, cannot interrupt blocking read on System.in
         rc
       }
       tty_loop.join
       process_result.join
     }
   }
 }
diff --git a/src/Pure/ML/ml_process.scala b/src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala
+++ b/src/Pure/ML/ml_process.scala
@@ -1,189 +1,189 @@
 /*  Title:      Pure/ML/ml_process.scala
     Author:     Makarius
 
 The raw ML process.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 
 object ML_Process
 {
   def apply(options: Options,
     logic: String = "",
     args: List[String] = Nil,
     dirs: List[Path] = Nil,
     modes: List[String] = Nil,
     raw_ml_system: Boolean = false,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
     redirect: Boolean = false,
     cleanup: () => Unit = () => (),
     sessions_structure: Option[Sessions.Structure] = None,
     session_base: Option[Sessions.Base] = None,
     store: Option[Sessions.Store] = None): Bash.Process =
   {
     val logic_name = Isabelle_System.default_logic(logic)
     val _store = store.getOrElse(Sessions.store(options))
 
     val sessions_structure1 =
       sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
 
     val heaps: List[String] =
       if (raw_ml_system) Nil
       else {
         sessions_structure1.selection(Sessions.Selection.session(logic_name)).
           build_requirements(List(logic_name)).
           map(a => File.platform_path(_store.the_heap(a)))
       }
 
     val eval_init =
       if (heaps.isEmpty) {
         List(
           """
           fun chapter (_: string) = ();
           fun section (_: string) = ();
           fun subsection (_: string) = ();
           fun subsubsection (_: string) = ();
           fun paragraph (_: string) = ();
           fun subparagraph (_: string) = ();
           val ML_file = PolyML.use;
           """,
           if (Platform.is_windows)
             "fun exit 0 = OS.Process.exit OS.Process.success" +
             " | exit 1 = OS.Process.exit OS.Process.failure" +
             " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
           else
             "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
           "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
           "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
       }
       else
         List(
           "(PolyML.SaveState.loadHierarchy " +
             ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) +
           "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
           ML_Syntax.print_string_bytes(": " + logic_name + "\n") +
           "); OS.Process.exit OS.Process.failure)")
 
     val eval_modes =
       if (modes.isEmpty) Nil
       else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes))
 
     // options
     val isabelle_process_options = Isabelle_System.tmp_file("options")
     Isabelle_System.chmod("600", File.path(isabelle_process_options))
     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
     val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
 
     // session base
     val eval_session_base =
       session_base match {
         case None => Nil
         case Some(base) =>
           def print_table(table: List[(String, String)]): String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
                 ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
           def print_list(list: List[String]): String =
             ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
           def print_sessions(list: List[(String, Position.T)]): String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
 
           List("Resources.init_session_base" +
             " {session_positions = " + print_sessions(sessions_structure1.session_positions) +
             ", session_directories = " + print_table(sessions_structure1.dest_session_directories) +
             ", docs = " + print_list(base.doc_names) +
             ", global_theories = " + print_table(base.global_theories.toList) +
             ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}")
       }
 
     // process
     val eval_process =
       if (heaps.isEmpty)
         List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
       else List("Isabelle_Process.init ()")
 
     // ISABELLE_TMP
     val isabelle_tmp = Isabelle_System.tmp_dir("process")
     val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
 
     val ml_runtime_options =
     {
       val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
       val ml_options1 =
         if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
         else ml_options ::: List("--gcthreads", options.int("threads").toString)
       val ml_options2 =
         if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1
         else ml_options1 ::: List("--codepage", "utf8")
       ml_options2
     }
 
     // bash
     val bash_args =
       ml_runtime_options :::
-      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
-        map(eval => List("--eval", eval)).flatten ::: args
+      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process)
+        .flatMap(eval => List("--eval", eval)) ::: args
 
     Bash.process(
       "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
         Bash.strings(bash_args),
       cwd = cwd,
       env = env ++ env_options ++ env_tmp,
       redirect = redirect,
       cleanup = () =>
         {
           isabelle_process_options.delete
           Isabelle_System.rm_tree(isabelle_tmp)
           cleanup()
         })
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
   {
     var dirs: List[Path] = Nil
     var eval_args: List[String] = Nil
     var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
     var modes: List[String] = Nil
     var options = Options.init()
 
     val getopts = Getopts("""
 Usage: isabelle process [OPTIONS]
 
   Options are:
     -T THEORY    load theory
     -d DIR       include session directory
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
     -m MODE      add print mode for output
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
 
   Run the raw Isabelle ML process in batch mode.
 """,
       "T:" -> (arg =>
         eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
       "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
       "l:" -> (arg => logic = arg),
       "m:" -> (arg => modes = arg :: modes),
       "o:" -> (arg => options = options + arg))
 
     val more_args = getopts(args)
-    if (args.isEmpty || !more_args.isEmpty) getopts.usage()
+    if (args.isEmpty || more_args.nonEmpty) getopts.usage()
 
     val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
       result().print_stdout.rc
     sys.exit(rc)
   })
 }
diff --git a/src/Pure/PIDE/markup_tree.scala b/src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala
+++ b/src/Pure/PIDE/markup_tree.scala
@@ -1,268 +1,268 @@
 /*  Title:      Pure/PIDE/markup_tree.scala
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
 Markup trees over nested / non-overlapping text ranges.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.SortedMap
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 
 object Markup_Tree
 {
   /* construct trees */
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
   def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree =
     (empty /: trees)(_.merge(_, range, elements))
 
   def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
     trees match {
       case Nil => empty
       case head :: tail =>
         new Markup_Tree(
           (head.branches /: tail) {
             case (branches, tree) =>
               (branches /: tree.branches) {
                 case (bs, (r, entry)) =>
                   require(!bs.isDefinedAt(r))
                   bs + (r -> entry)
               }
           })
     }
 
 
   /* tree building blocks */
 
   object Entry
   {
     def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
       Entry(markup.range, List(markup.info), subtree)
   }
 
   sealed case class Entry(
     range: Text.Range,
     rev_markup: List[XML.Elem],
     subtree: Markup_Tree)
   {
     def markup: List[XML.Elem] = rev_markup.reverse
 
     def filter_markup(elements: Markup.Elements): List[XML.Elem] =
     {
       var result: List[XML.Elem] = Nil
       for (elem <- rev_markup if elements(elem.name))
         result ::= elem
       result.toList
     }
 
     def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)
     def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup)
   }
 
   object Branches
   {
     type T = SortedMap[Text.Range, Entry]
     val empty: T = SortedMap.empty(Text.Range.Ordering)
   }
 
 
   /* XML representation */
 
   @tailrec private def strip_elems(
       elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) =
     body match {
       case List(XML.Wrapped_Elem(markup1, body1, body2)) =>
         strip_elems(XML.Elem(markup1, body1) :: elems, body2)
       case List(XML.Elem(markup1, body1)) =>
         strip_elems(XML.Elem(markup1, Nil) :: elems, body1)
       case _ => (elems, body)
     }
 
   private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) =
     {
       val (offset, markup_trees) = acc
 
       strip_elems(Nil, List(tree)) match {
         case (Nil, body) =>
           (offset + XML.text_length(body), markup_trees)
 
         case (elems, body) =>
           val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)
           if (offset == end_offset) acc
           else {
             val range = Text.Range(offset, end_offset)
             val entry = Entry(range, elems, merge_disjoint(subtrees))
             (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
           }
       }
     }
 
   def from_XML(body: XML.Body): Markup_Tree =
     merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2)
 }
 
 
 final class Markup_Tree private(val branches: Markup_Tree.Branches.T)
 {
   import Markup_Tree._
 
   private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
     this(branches + (entry.range -> entry))
 
   private def overlapping(range: Text.Range): Branches.T =
     if (branches.isEmpty ||
         (range.contains(branches.firstKey.start) && branches.lastKey.stop <= range.stop))
       branches
     else {
       val start = Text.Range(range.start)
       val stop = Text.Range(range.stop)
       val bs = branches.range(start, stop)
       branches.get(stop) match {
         case Some(end) if range overlaps end.range => bs + (end.range -> end)
         case _ => bs
       }
     }
 
   def restrict(range: Text.Range): Markup_Tree =
     new Markup_Tree(overlapping(range))
 
   def is_empty: Boolean = branches.isEmpty
 
   def + (new_markup: Text.Markup): Markup_Tree =
   {
     val new_range = new_markup.range
 
     branches.get(new_range) match {
       case None => new Markup_Tree(branches, Entry(new_markup, empty))
       case Some(entry) =>
         if (entry.range == new_range)
           new Markup_Tree(branches, entry + new_markup)
         else if (entry.range.contains(new_range))
           new Markup_Tree(branches, entry \ new_markup)
         else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
           new Markup_Tree(Branches.empty, Entry(new_markup, this))
         else {
           val body = overlapping(new_range)
           if (body.forall(e => new_range.contains(e._1)))
             new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
           else {
             Output.warning("Ignored overlapping markup information: " + new_markup + "\n" +
-              body.filter(e => !new_range.contains(e._1)).map(_._2).mkString("\n"))
+              body.filter(e => !new_range.contains(e._1)).values.mkString("\n"))
             this
           }
         }
     }
   }
 
   def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree =
   {
     def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
       (tree1 /: tree2.branches)(
         { case (tree, (range, entry)) =>
             if (!range.overlaps(root_range)) tree
             else
               (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
                 { case (t, elem) => t + Text.Info(range, elem) })
         })
 
     if (this eq other) this
     else {
       val tree1 = this.restrict(root_range)
       val tree2 = other.restrict(root_range)
       if (tree1.is_empty) tree2
       else merge_trees(tree1, tree2)
     }
   }
 
   def cumulate[A](root_range: Text.Range, root_info: A, elements: Markup.Elements,
     result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
   {
     def results(x: A, entry: Entry): Option[A] =
     {
       var y = x
       var changed = false
       for {
         elem <- entry.filter_markup(elements)
         y1 <- result(y, Text.Info(entry.range, elem))
       } { y = y1; changed = true }
       if (changed) Some(y) else None
     }
 
     def traverse(
       last: Text.Offset,
       stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] =
     {
       stack match {
         case (parent, (range, entry) :: more) :: rest =>
           val subrange = range.restrict(root_range)
           val subtree = entry.subtree.overlapping(subrange).toList
           val start = subrange.start
 
           results(parent.info, entry) match {
             case Some(res) =>
               val next = Text.Info(subrange, res)
               val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)
               if (last < start) parent.restrict(Text.Range(last, start)) :: nexts
               else nexts
             case None => traverse(last, (parent, subtree ::: more) :: rest)
           }
 
         case (parent, Nil) :: rest =>
           val stop = parent.range.stop
           val nexts = traverse(stop, rest)
           if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts
           else nexts
 
         case Nil =>
           val stop = root_range.stop
           if (last < stop) List(Text.Info(Text.Range(last, stop), root_info))
           else Nil
       }
     }
     traverse(root_range.start,
       List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
   }
 
   def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body =
   {
     def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
       if (start == stop) Nil
       else List(XML.Text(text.subSequence(start, stop).toString))
 
     def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
       (body /: rev_markups) {
         case (b, elem) =>
           if (!elements(elem.name)) b
           else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
           else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
       }
 
     def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
       : XML.Body =
     {
       val body = new mutable.ListBuffer[XML.Tree]
       var last = elem_range.start
       for ((range, entry) <- entries) {
         val subrange = range.restrict(elem_range)
         body ++= make_text(last, subrange.start)
         body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
         last = subrange.stop
       }
       body ++= make_text(last, elem_range.stop)
       make_elems(elem_markup, body.toList)
     }
    make_body(root_range, Nil, overlapping(root_range))
   }
 
   override def toString: String =
     branches.toList.map(_._2) match {
       case Nil => "Empty"
       case list => list.mkString("Tree(", ",", ")")
     }
 }
diff --git a/src/Pure/PIDE/prover.scala b/src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala
+++ b/src/Pure/PIDE/prover.scala
@@ -1,366 +1,366 @@
 /*  Title:      Pure/PIDE/prover.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 Prover process wrapping.
 */
 
 package isabelle
 
 
 import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException}
 
 
 object Prover
 {
   /* messages */
 
   sealed abstract class Message
   type Receiver = Message => Unit
 
   class Input(val name: String, val args: List[String]) extends Message
   {
     override def toString: String =
       XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
-        args.map(s =>
-          List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
+        args.flatMap(s =>
+          List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s))))).toString
   }
 
   class Output(val message: XML.Elem) extends Message
   {
     def kind: String = message.markup.name
     def properties: Properties.T = message.markup.properties
     def body: XML.Body = message.body
 
     def is_init = kind == Markup.INIT
     def is_exit = kind == Markup.EXIT
     def is_stdout = kind == Markup.STDOUT
     def is_stderr = kind == Markup.STDERR
     def is_system = kind == Markup.SYSTEM
     def is_status = kind == Markup.STATUS
     def is_report = kind == Markup.REPORT
     def is_syslog = is_init || is_exit || is_system || is_stderr
 
     override def toString: String =
     {
       val res =
         if (is_status || is_report) message.body.map(_.toString).mkString
         else Pretty.string_of(message.body)
       if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"
       else
         kind.toString + " " +
           (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
     }
   }
 
   class Protocol_Output(props: Properties.T, val bytes: Bytes)
     extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
   {
     lazy val text: String = bytes.text
   }
 }
 
 
 class Prover(
   receiver: Prover.Receiver,
   xml_cache: XML.Cache,
   channel: System_Channel,
   process: Bash.Process) extends Protocol
 {
   /** receiver output **/
 
   private def system_output(text: String)
   {
     receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
   private def protocol_output(props: Properties.T, bytes: Bytes)
   {
     receiver(new Prover.Protocol_Output(props, bytes))
   }
 
   private def output(kind: String, props: Properties.T, body: XML.Body)
   {
     val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
     val reports = Protocol_Message.reports(props, body)
     for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
   }
 
   private def exit_message(result: Process_Result)
   {
     output(Markup.EXIT, Markup.Process_Result(result),
       List(XML.Text("Return code: " + result.rc.toString)))
   }
 
 
 
   /** process manager **/
 
   private val process_result: Future[Process_Result] =
     Future.thread("process_result") {
       val rc = process.join
       val timing = process.get_timing
       Process_Result(rc, timing = timing)
     }
 
   private def terminate_process()
   {
     try { process.terminate }
     catch {
       case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
     }
   }
 
   private val process_manager = Standard_Thread.fork("process_manager")
   {
     val (startup_failed, startup_errors) =
     {
       var finished: Option[Boolean] = None
       val result = new StringBuilder(100)
       while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
         while (finished.isEmpty && process.stderr.ready) {
           try {
             val c = process.stderr.read
             if (c == 2) finished = Some(true)
             else result += c.toChar
           }
           catch { case _: IOException => finished = Some(false) }
         }
         Thread.sleep(10)
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
     if (startup_errors != "") system_output(startup_errors)
 
     if (startup_failed) {
       terminate_process()
       process_result.join
       exit_message(Process_Result(127))
     }
     else {
       val (command_stream, message_stream) = channel.rendezvous()
 
       command_input_init(command_stream)
       val stdout = physical_output(false)
       val stderr = physical_output(true)
       val message = message_output(message_stream)
 
       val result = process_result.join
       system_output("process terminated")
       command_input_close()
       for (thread <- List(stdout, stderr, message)) thread.join
       system_output("process_manager terminated")
       exit_message(result)
     }
     channel.shutdown()
   }
 
 
   /* management methods */
 
   def join() { process_manager.join() }
 
   def terminate()
   {
     system_output("Terminating prover process")
     command_input_close()
 
     var count = 10
     while (!process_result.is_finished && count > 0) {
       Thread.sleep(100)
       count -= 1
     }
     if (!process_result.is_finished) terminate_process()
   }
 
 
 
   /** process streams **/
 
   /* command input */
 
   private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
 
   private def command_input_close(): Unit = command_input.foreach(_.shutdown)
 
   private def command_input_init(raw_stream: OutputStream)
   {
     val name = "command_input"
     val stream = new BufferedOutputStream(raw_stream)
     command_input =
       Some(
         Consumer_Thread.fork(name)(
           consume =
             {
               case chunks =>
                 try {
                   Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream)
                   chunks.foreach(_.write_stream(stream))
                   stream.flush
                   true
                 }
                 catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
             },
           finish = { case () => stream.close; system_output(name + " terminated") }
         )
       )
   }
 
 
   /* physical output */
 
   private def physical_output(err: Boolean): Thread =
   {
     val (name, reader, markup) =
       if (err) ("standard_error", process.stderr, Markup.STDERR)
       else ("standard_output", process.stdout, Markup.STDOUT)
 
     Standard_Thread.fork(name) {
       try {
         var result = new StringBuilder(100)
         var finished = false
         while (!finished) {
           //{{{
           var c = -1
           var done = false
-          while (!done && (result.length == 0 || reader.ready)) {
+          while (!done && (result.isEmpty || reader.ready)) {
             c = reader.read
             if (c >= 0) result.append(c.asInstanceOf[Char])
             else done = true
           }
-          if (result.length > 0) {
+          if (result.nonEmpty) {
             output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
             result.clear
           }
           else {
             reader.close
             finished = true
           }
           //}}}
         }
       }
       catch { case e: IOException => system_output(name + ": " + e.getMessage) }
       system_output(name + " terminated")
     }
   }
 
 
   /* message output */
 
   private def message_output(stream: InputStream): Thread =
   {
     class EOF extends Exception
     class Protocol_Error(msg: String) extends Exception(msg)
 
     val name = "message_output"
     Standard_Thread.fork(name) {
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
       def read_int(): Int =
       //{{{
       {
         var n = 0
         c = stream.read
         if (c == -1) throw new EOF
         while (48 <= c && c <= 57) {
           n = 10 * n + (c - 48)
           c = stream.read
         }
         if (c != 10)
           throw new Protocol_Error("malformed header: expected integer followed by newline")
         else n
       }
       //}}}
 
       def read_chunk_bytes(): (Array[Byte], Int) =
       //{{{
       {
         val n = read_int()
         val buf =
           if (n <= default_buffer.length) default_buffer
           else new Array[Byte](n)
 
         var i = 0
         var m = 0
         do {
           m = stream.read(buf, i, n - i)
           if (m != -1) i += m
         }
         while (m != -1 && n > i)
 
         if (i != n)
           throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
 
         (buf, n)
       }
       //}}}
 
       def read_chunk(): XML.Body =
       {
         val (buf, n) = read_chunk_bytes()
         YXML.parse_body_failsafe(UTF8.decode_chars(Symbol.decode, buf, 0, n))
       }
 
       try {
         do {
           try {
             val header = read_chunk()
             header match {
               case List(XML.Elem(Markup(name, props), Nil)) =>
                 val kind = name.intern
                 if (kind == Markup.PROTOCOL) {
                   val (buf, n) = read_chunk_bytes()
                   protocol_output(props, Bytes(buf, 0, n))
                 }
                 else {
                   val body = read_chunk()
                   output(kind, props, body)
                 }
               case _ =>
                 read_chunk()
                 throw new Protocol_Error("bad header: " + header.toString)
             }
           }
           catch { case _: EOF => }
         }
         while (c != -1)
       }
       catch {
         case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
         case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
       }
       stream.close
 
       system_output(name + " terminated")
     }
   }
 
 
 
   /** protocol commands **/
 
   var trace: Boolean = false
 
   def protocol_command_raw(name: String, args: List[Bytes]): Unit =
     command_input match {
       case Some(thread) if thread.is_active =>
         if (trace) {
           val payload = (0 /: args)({ case (n, b) => n + b.length })
           Output.writeln(
             "protocol_command " + name + ", args = " + args.length + ", payload = " + payload)
         }
         thread.send(Bytes(name) :: args)
       case _ => error("Inactive prover input thread for command " + quote(name))
     }
 
   def protocol_command_args(name: String, args: List[String])
   {
     receiver(new Prover.Input(name, args))
     protocol_command_raw(name, args.map(Bytes(_)))
   }
 
   def protocol_command(name: String, args: String*): Unit =
     protocol_command_args(name, args.toList)
 }
diff --git a/src/Pure/System/getopts.scala b/src/Pure/System/getopts.scala
--- a/src/Pure/System/getopts.scala
+++ b/src/Pure/System/getopts.scala
@@ -1,69 +1,69 @@
 /*  Title:      Pure/System/getopts.scala
     Author:     Makarius
 
 Support for command-line options as in GNU bash.
 */
 
 package isabelle
 
 
 object Getopts
 {
   def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
   {
     val options =
       (Map.empty[Char, (Boolean, String => Unit)] /: option_specs) {
         case (m, (s, f)) =>
           val (a, entry) =
             if (s.size == 1) (s(0), (false, f))
             else if (s.size == 2 && s.endsWith(":")) (s(0), (true, f))
             else error("Bad option specification: " + quote(s))
           if (m.isDefinedAt(a)) error("Duplicate option specification: " + quote(a.toString))
           else m + (a -> entry)
       }
     new Getopts(usage_text, options)
   }
 }
 
 class Getopts private(usage_text: String, options: Map[Char, (Boolean, String => Unit)])
 {
   def usage(): Nothing =
   {
     Output.writeln(usage_text, stdout = true)
     sys.exit(1)
   }
 
   private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
   private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
   private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
   private def print_option(opt: Char): String = quote("-" + opt.toString)
   private def option(opt: Char, opt_arg: List[Char]): Unit =
     try { options(opt)._2.apply(opt_arg.mkString) }
     catch {
       case ERROR(msg) =>
         cat_error(msg, "The error(s) above occurred in command-line option " + print_option(opt))
     }
 
   private def getopts(args: List[List[Char]]): List[List[Char]] =
     args match {
       case List('-', '-') :: rest_args => rest_args
-      case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && !rest_opts.isEmpty =>
+      case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && rest_opts.nonEmpty =>
         option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args)
       case List('-', opt) :: rest_args if is_option0(opt) =>
         option(opt, Nil); getopts(rest_args)
-      case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && !opt_arg.isEmpty =>
+      case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && opt_arg.nonEmpty =>
         option(opt, opt_arg); getopts(rest_args)
       case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
         option(opt, opt_arg); getopts(rest_args)
       case List(List('-', opt)) if is_option1(opt) =>
         Output.error_message("Command-line option " + print_option(opt) + " requires an argument")
         usage()
       case ('-' :: opt :: _) :: _ if !is_option(opt) =>
         if (opt != '?') Output.error_message("Illegal command-line option " + print_option(opt))
         usage()
       case _ => args
   }
 
   def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString)
   def apply(args: Array[String]): List[String] = apply(args.toList)
 }
diff --git a/src/Pure/System/isabelle_tool.scala b/src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala
+++ b/src/Pure/System/isabelle_tool.scala
@@ -1,182 +1,182 @@
 /*  Title:      Pure/System/isabelle_tool.scala
     Author:     Makarius
     Author:     Lars Hupel
 
 Isabelle system tools: external executables or internal Scala functions.
 */
 
 package isabelle
 
 import java.net.URLClassLoader
 import scala.reflect.runtime.universe
 import scala.tools.reflect.{ToolBox,ToolBoxError}
 
 
 object Isabelle_Tool
 {
   /* Scala source tools */
 
   abstract class Body extends Function[List[String], Unit]
 
   private def compile(path: Path): Body =
   {
     def err(msg: String): Nothing =
       cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path)
 
     val source = File.read(path)
 
     val class_loader = new URLClassLoader(Array(), getClass.getClassLoader)
     val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
 
     try {
       val symbol = tool_box.parse(source) match {
         case tree: universe.ModuleDef => tool_box.define(tree)
         case _ => err("Source does not describe a module (Scala object)")
       }
       tool_box.compile(universe.Ident(symbol))() match {
         case body: Body => body
         case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
       }
     }
     catch {
       case e: ToolBoxError =>
         if (tool_box.frontEnd.hasErrors) {
           val infos = tool_box.frontEnd.infos.toList
           val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg)
           err(msgs.mkString("\n"))
         }
         else
           err(e.toString)
     }
   }
 
 
   /* external tools */
 
   private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
 
   private def is_external(dir: Path, file_name: String): Boolean =
   {
     val file = (dir + Path.explode(file_name)).file
     try {
       file.isFile && file.canRead &&
         (file_name.endsWith(".scala") || file.canExecute) &&
         !file_name.endsWith("~") && !file_name.endsWith(".orig")
     }
     catch { case _: SecurityException => false }
   }
 
   private def list_external(): List[(String, String)] =
   {
     val Description = """.*\bDESCRIPTION: *(.*)""".r
     for {
       dir <- dirs() if dir.is_dir
       file_name <- File.read_dir(dir) if is_external(dir, file_name)
     } yield {
       val source = File.read(dir + Path.explode(file_name))
       val name = Library.perhaps_unsuffix(".scala", file_name)
       val description =
         split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
       (name, description)
     }
   }
 
   private def find_external(name: String): Option[List[String] => Unit] =
-    dirs.collectFirst({
+    dirs().collectFirst({
       case dir if is_external(dir, name + ".scala") =>
         compile(dir + Path.explode(name + ".scala"))
       case dir if is_external(dir, name) =>
         (args: List[String]) =>
           {
             val tool = dir + Path.explode(name)
             val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
             sys.exit(result.print_stdout.rc)
           }
     })
 
 
   /* internal tools */
 
   private lazy val internal_tools: List[Isabelle_Tool] =
     Isabelle_System.init_classes[Isabelle_Scala_Tools]("ISABELLE_SCALA_TOOLS")
       .flatMap(_.tools.toList)
 
   private def list_internal(): List[(String, String)] =
     for (tool <- internal_tools.toList)
       yield (tool.name, tool.description)
 
   private def find_internal(name: String): Option[List[String] => Unit] =
     internal_tools.collectFirst({
       case tool if tool.name == name =>
         args => Command_Line.tool0 { tool.body(args) }
       })
 
 
   /* command line entry point */
 
   def main(args: Array[String])
   {
     Command_Line.tool0 {
       args.toList match {
         case Nil | List("-?") =>
           val tool_descriptions =
             (list_external() ::: list_internal()).sortBy(_._1).
               map({ case (a, "") => a case (a, b) => a + " - " + b })
           Getopts("""
 Usage: isabelle TOOL [ARGS ...]
 
   Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
 
 Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
         case tool_name :: tool_args =>
           find_external(tool_name) orElse find_internal(tool_name) match {
             case Some(tool) => tool(tool_args)
             case None => error("Unknown Isabelle tool: " + quote(tool_name))
           }
       }
     }
   }
 }
 
 sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
 
 class Isabelle_Scala_Tools(val tools: Isabelle_Tool*)
 
 class Tools extends Isabelle_Scala_Tools(
   Build.isabelle_tool,
   Build_Docker.isabelle_tool,
   Doc.isabelle_tool,
   Dump.isabelle_tool,
   Export.isabelle_tool,
   ML_Process.isabelle_tool,
   Mercurial.isabelle_tool,
   Mkroot.isabelle_tool,
   Options.isabelle_tool,
   Phabricator.isabelle_tool1,
   Phabricator.isabelle_tool2,
   Phabricator.isabelle_tool3,
   Phabricator.isabelle_tool4,
   Present.isabelle_tool,
   Profiling_Report.isabelle_tool,
   Server.isabelle_tool,
   Scala_Project.isabelle_tool,
   Update.isabelle_tool,
   Update_Cartouches.isabelle_tool,
   Update_Comments.isabelle_tool,
   Update_Header.isabelle_tool,
   Update_Then.isabelle_tool,
   Update_Theorems.isabelle_tool,
   isabelle.vscode.Grammar.isabelle_tool,
   isabelle.vscode.Server.isabelle_tool)
 
 class Admin_Tools extends Isabelle_Scala_Tools(
   Build_Cygwin.isabelle_tool,
   Build_Doc.isabelle_tool,
   Build_Fonts.isabelle_tool,
   Build_JDK.isabelle_tool,
   Build_PolyML.isabelle_tool1,
   Build_PolyML.isabelle_tool2,
   Build_Status.isabelle_tool,
   Check_Sources.isabelle_tool,
   Components.isabelle_tool,
   isabelle.vscode.Build_VSCode.isabelle_tool)
diff --git a/src/Pure/System/platform.scala b/src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala
+++ b/src/Pure/System/platform.scala
@@ -1,71 +1,71 @@
 /*  Title:      Pure/System/platform.scala
     Author:     Makarius
 
 System platform identification.
 */
 
 package isabelle
 
 
 object Platform
 {
   /* platform family */
 
-  val is_linux = System.getProperty("os.name", "") == "Linux"
-  val is_macos = System.getProperty("os.name", "") == "Mac OS X"
-  val is_windows = System.getProperty("os.name", "").startsWith("Windows")
+  val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
+  val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X"
+  val is_windows: Boolean = System.getProperty("os.name", "").startsWith("Windows")
 
   def family: Family.Value =
     if (is_linux) Family.linux
     else if (is_macos) Family.macos
     else if (is_windows) Family.windows
     else error("Failed to determine current platform family")
 
   object Family extends Enumeration
   {
     val linux, macos, windows = Value
 
     def unapply(name: String): Option[Value] =
       try { Some(withName(name)) }
       catch { case _: NoSuchElementException => None }
 
     def parse(name: String): Value =
       unapply(name) getOrElse error("Bad platform family: " + quote(name))
   }
 
 
   /* platform identifiers */
 
   private val X86 = """i.86|x86""".r
   private val X86_64 = """amd64|x86_64""".r
 
   def cpu_arch: String =
     System.getProperty("os.arch", "") match {
       case X86() => "x86"
       case X86_64() => "x86_64"
       case _ => error("Failed to determine CPU architecture")
     }
 
   def os_name: String =
     family match {
       case Family.macos => "darwin"
       case _ => family.toString
     }
 
   lazy val jvm_platform: String = cpu_arch + "-" + os_name
 
 
   /* JVM version */
 
   private val Version = """1\.(\d+)\.0_(\d+)""".r
-  lazy val jvm_version =
+  lazy val jvm_version: String =
     System.getProperty("java.version") match {
       case Version(a, b) => a + "u" + b
       case a => a
     }
 
 
   /* JVM name */
 
   val jvm_name: String = System.getProperty("java.vm.name", "")
 }
diff --git a/src/Pure/System/tty_loop.scala b/src/Pure/System/tty_loop.scala
--- a/src/Pure/System/tty_loop.scala
+++ b/src/Pure/System/tty_loop.scala
@@ -1,74 +1,74 @@
 /*  Title:      Pure/System/tty_loop.scala
     Author:     Makarius
 
 Line-oriented TTY loop.
 */
 
 package isabelle
 
 
 import java.io.{IOException, Writer, Reader, InputStreamReader, BufferedReader}
 
 
 class TTY_Loop(writer: Writer, reader: Reader,
   writer_lock: AnyRef = new Object,
   interrupt: Option[() => Unit] = None)
 {
   private val console_output = Future.thread[Unit]("console_output") {
     try {
       var result = new StringBuilder(100)
       var finished = false
       while (!finished) {
         var c = -1
         var done = false
-        while (!done && (result.length == 0 || reader.ready)) {
+        while (!done && (result.isEmpty || reader.ready)) {
           c = reader.read
           if (c >= 0) result.append(c.asInstanceOf[Char])
           else done = true
         }
-        if (result.length > 0) {
+        if (result.nonEmpty) {
           System.out.print(result.toString)
           System.out.flush()
           result.clear
         }
         else {
           reader.close()
           finished = true
         }
       }
     }
     catch { case e: IOException => case Exn.Interrupt() => }
   }
 
   private val console_input = Future.thread[Unit]("console_input") {
     val console_reader = new BufferedReader(new InputStreamReader(System.in))
     def body
     {
       try {
         var finished = false
         while (!finished) {
           console_reader.readLine() match {
             case null =>
               writer.close()
               finished = true
             case line =>
               writer_lock.synchronized {
                 writer.write(line)
                 writer.write("\n")
                 writer.flush()
               }
           }
         }
       }
       catch { case e: IOException => case Exn.Interrupt() => }
     }
     interrupt match {
       case None => body
       case Some(int) => POSIX_Interrupt.handler { int() } { body }
     }
   }
 
   def join { console_output.join; console_input.join }
 
   def cancel { console_input.cancel }
 }
diff --git a/src/Pure/Tools/server.scala b/src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala
+++ b/src/Pure/Tools/server.scala
@@ -1,619 +1,619 @@
 /*  Title:      Pure/Tools/server.scala
     Author:     Makarius
 
 Resident Isabelle servers.
 
 Message formats:
   - short message (single line):
       NAME ARGUMENT
   - long message (multiple lines):
       BYTE_LENGTH
       NAME ARGUMENT
 
 Argument formats:
   - Unit as empty string
   - XML.Elem in YXML notation
   - JSON.T in standard notation
 */
 
 package isabelle
 
 
 import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter,
   IOException}
 import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress}
 
 
 object Server
 {
   /* message argument */
 
   object Argument
   {
     def is_name_char(c: Char): Boolean =
       Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || c == '_' || c == '.'
 
     def split(msg: String): (String, String) =
     {
       val name = msg.takeWhile(is_name_char(_))
       val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
       (name, argument)
     }
 
     def print(arg: Any): String =
       arg match {
         case () => ""
         case t: XML.Elem => YXML.string_of_tree(t)
         case t: JSON.T => JSON.Format(t)
       }
 
     def parse(argument: String): Any =
       if (argument == "") ()
       else if (YXML.detect_elem(argument)) YXML.parse_elem(argument)
       else JSON.parse(argument, strict = false)
 
     def unapply(argument: String): Option[Any] =
       try { Some(parse(argument)) }
       catch { case ERROR(_) => None }
   }
 
 
   /* input command */
 
   object Command
   {
     type T = PartialFunction[(Context, Any), Any]
 
     private val table: Map[String, T] =
       Map(
         "help" -> { case (_, ()) => table.keySet.toList.sorted },
         "echo" -> { case (_, t) => t },
         "shutdown" -> { case (context, ()) => context.server.shutdown() },
         "cancel" ->
           { case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) },
         "session_build" ->
           { case (context, Server_Commands.Session_Build(args)) =>
               context.make_task(task =>
                 Server_Commands.Session_Build.command(args, progress = task.progress)._1)
           },
         "session_start" ->
           { case (context, Server_Commands.Session_Start(args)) =>
               context.make_task(task =>
                 {
                   val (res, entry) =
                     Server_Commands.Session_Start.command(
                       args, progress = task.progress, log = context.server.log)
                   context.server.add_session(entry)
                   res
                 })
           },
         "session_stop" ->
           { case (context, Server_Commands.Session_Stop(id)) =>
               context.make_task(_ =>
                 {
                   val session = context.server.remove_session(id)
                   Server_Commands.Session_Stop.command(session)._1
                 })
           },
         "use_theories" ->
           { case (context, Server_Commands.Use_Theories(args)) =>
               context.make_task(task =>
                 {
                   val session = context.server.the_session(args.session_id)
                   Server_Commands.Use_Theories.command(
                     args, session, id = task.id, progress = task.progress)._1
                 })
           },
         "purge_theories" ->
           { case (context, Server_Commands.Purge_Theories(args)) =>
               val session = context.server.the_session(args.session_id)
               Server_Commands.Purge_Theories.command(args, session)._1
           })
 
     def unapply(name: String): Option[T] = table.get(name)
   }
 
 
   /* output reply */
 
   class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty)
     extends RuntimeException(message)
 
   def json_error(exn: Throwable): JSON.Object.T =
     exn match {
       case e: Error => Reply.error_message(e.message) ++ e.json
       case ERROR(msg) => Reply.error_message(msg)
       case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
       case _ => JSON.Object.empty
     }
 
   object Reply extends Enumeration
   {
     val OK, ERROR, FINISHED, FAILED, NOTE = Value
 
     def message(msg: String, kind: String = ""): JSON.Object.T =
       JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg)
 
     def error_message(msg: String): JSON.Object.T =
       message(msg, kind = Markup.ERROR)
 
     def unapply(msg: String): Option[(Reply.Value, Any)] =
     {
       if (msg == "") None
       else {
         val (name, argument) = Argument.split(msg)
         for {
           reply <-
             try { Some(withName(name)) }
             catch { case _: NoSuchElementException => None }
           arg <- Argument.unapply(argument)
         } yield (reply, arg)
       }
     }
   }
 
 
   /* socket connection */
 
   object Connection
   {
     def apply(socket: Socket): Connection =
       new Connection(socket)
   }
 
   class Connection private(socket: Socket) extends AutoCloseable
   {
     override def toString: String = socket.toString
 
     def close() { socket.close }
 
     def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) }
 
     private val in = new BufferedInputStream(socket.getInputStream)
     private val out = new BufferedOutputStream(socket.getOutputStream)
     private val out_lock: AnyRef = new Object
 
     def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
       new TTY_Loop(
         new OutputStreamWriter(out),
         new InputStreamReader(in),
         writer_lock = out_lock,
         interrupt = interrupt)
 
     def read_password(password: String): Boolean =
       try { Byte_Message.read_line(in).map(_.text) == Some(password) }
       catch { case _: IOException => false }
 
     def read_message(): Option[String] =
       try { Byte_Message.read_line_message(in).map(_.text) }
       catch { case _: IOException => None }
 
     def write_message(msg: String): Unit =
       out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }
 
     def reply(r: Reply.Value, arg: Any)
     {
       val argument = Argument.print(arg)
       write_message(if (argument == "") r.toString else r.toString + " " + argument)
     }
 
     def reply_ok(arg: Any) { reply(Reply.OK, arg) }
     def reply_error(arg: Any) { reply(Reply.ERROR, arg) }
     def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
       reply_error(Reply.error_message(message) ++ more)
 
     def notify(arg: Any) { reply(Reply.NOTE, arg) }
   }
 
 
   /* context with output channels */
 
   class Context private[Server](val server: Server, connection: Connection)
     extends AutoCloseable
   {
     context =>
 
     def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) }
     def notify(arg: Any) { connection.notify(arg) }
     def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
       notify(Reply.message(msg, kind = kind) ++ more)
     def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
     def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
     def error_message(msg: String, more: JSON.Object.Entry*): Unit =
       message(Markup.ERROR, msg, more:_*)
 
     def progress(more: JSON.Object.Entry*): Connection_Progress =
       new Connection_Progress(context, more:_*)
 
     override def toString: String = connection.toString
 
 
     /* asynchronous tasks */
 
     private val _tasks = Synchronized(Set.empty[Task])
 
     def make_task(body: Task => JSON.Object.T): Task =
     {
       val task = new Task(context, body)
       _tasks.change(_ + task)
       task
     }
 
     def remove_task(task: Task): Unit =
       _tasks.change(_ - task)
 
     def cancel_task(id: UUID.T): Unit =
       _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks })
 
     def close()
     {
       while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) }))
       { _tasks.value.foreach(_.join) }
     }
   }
 
   class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
     extends Progress
   {
     override def echo(msg: String): Unit = context.writeln(msg, more:_*)
     override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
     override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
 
     override def theory(theory: Progress.Theory)
     {
       val entries: List[JSON.Object.Entry] =
         List("theory" -> theory.theory, "session" -> theory.session) :::
           (theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) })
       context.writeln(theory.message, entries ::: more.toList:_*)
     }
 
     override def nodes_status(nodes_status: Document_Status.Nodes_Status)
     {
       val json =
         for ((name, node_status) <- nodes_status.present)
           yield name.json + ("status" -> nodes_status(name).json)
       context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
     }
 
     @volatile private var is_stopped = false
     override def stopped: Boolean = is_stopped
     def stop { is_stopped = true }
 
     override def toString: String = context.toString
   }
 
   class Task private[Server](val context: Context, body: Task => JSON.Object.T)
   {
     task =>
 
     val id: UUID.T = UUID.random()
     val ident: JSON.Object.Entry = ("task" -> id.toString)
 
     val progress: Connection_Progress = context.progress(ident)
     def cancel { progress.stop }
 
     private lazy val thread = Standard_Thread.fork("server_task")
     {
       Exn.capture { body(task) } match {
         case Exn.Res(res) =>
           context.reply(Reply.FINISHED, res + ident)
         case Exn.Exn(exn) =>
           val err = json_error(exn)
           if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident)
       }
       progress.stop
       context.remove_task(task)
     }
     def start { thread }
     def join { thread.join }
   }
 
 
   /* server info */
 
   val localhost_name: String = "127.0.0.1"
   def localhost: InetAddress = InetAddress.getByName(localhost_name)
 
   def print_address(port: Int): String = localhost_name + ":" + port
 
   def print(port: Int, password: String): String =
     print_address(port) + " (password " + quote(password) + ")"
 
   object Info
   {
     private val Pattern =
       ("""server "([^"]*)" = \Q""" + localhost_name + """\E:(\d+) \(password "([^"]*)"\)""").r
 
     def parse(s: String): Option[Info] =
       s match {
         case Pattern(name, Value.Int(port), password) => Some(Info(name, port, password))
         case _ => None
       }
 
     def apply(name: String, port: Int, password: String): Info =
       new Info(name, port, password)
   }
 
   class Info private(val name: String, val port: Int, val password: String)
   {
     def address: String = print_address(port)
 
     override def toString: String =
       "server " + quote(name) + " = " + print(port, password)
 
     def connection(): Connection =
     {
       val connection = Connection(new Socket(localhost, port))
       connection.write_message(password)
       connection
     }
 
     def active(): Boolean =
       try {
         using(connection())(connection =>
           {
             connection.set_timeout(Time.seconds(2.0))
             connection.read_message() match {
               case Some(Reply(Reply.OK, _)) => true
               case _ => false
             }
           })
       }
       catch {
         case _: IOException => false
         case _: SocketException => false
         case _: SocketTimeoutException => false
       }
   }
 
 
   /* per-user servers */
 
   val default_name = "isabelle"
 
   object Data
   {
     val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
 
     val name = SQL.Column.string("name").make_primary_key
     val port = SQL.Column.int("port")
     val password = SQL.Column.string("password")
     val table = SQL.Table("isabelle_servers", List(name, port, password))
   }
 
   def list(db: SQLite.Database): List[Info] =
     if (db.tables.contains(Data.table.name)) {
       db.using_statement(Data.table.select())(stmt =>
         stmt.execute_query().iterator(res =>
           Info(
             res.string(Data.name),
             res.int(Data.port),
             res.string(Data.password))).toList.sortBy(_.name))
     }
     else Nil
 
   def find(db: SQLite.Database, name: String): Option[Info] =
     list(db).find(server_info => server_info.name == name && server_info.active)
 
   def init(
     name: String = default_name,
     port: Int = 0,
     existing_server: Boolean = false,
     log: Logger = No_Logger): (Info, Option[Server]) =
   {
     using(SQLite.open_database(Data.database))(db =>
       {
         db.transaction {
           Isabelle_System.chmod("600", Data.database)
           db.create_table(Data.table)
           list(db).filterNot(_.active).foreach(server_info =>
             db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
               _.execute))
         }
         db.transaction {
           find(db, name) match {
             case Some(server_info) => (server_info, None)
             case None =>
               if (existing_server) error("Isabelle server " + quote(name) + " not running")
 
               val server = new Server(port, log)
               val server_info = Info(name, server.port, server.password)
 
               db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
               db.using_statement(Data.table.insert())(stmt =>
               {
                 stmt.string(1) = server_info.name
                 stmt.int(2) = server_info.port
                 stmt.string(3) = server_info.password
                 stmt.execute()
               })
 
               server.start
               (server_info, Some(server))
           }
         }
       })
   }
 
   def exit(name: String = default_name): Boolean =
   {
     using(SQLite.open_database(Data.database))(db =>
       db.transaction {
         find(db, name) match {
           case Some(server_info) =>
             using(server_info.connection())(_.write_message("shutdown"))
             while(server_info.active) { Thread.sleep(50) }
             true
           case None => false
         }
       })
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("server", "manage resident Isabelle servers", args =>
     {
       var console = false
       var log_file: Option[Path] = None
       var operation_list = false
       var operation_exit = false
       var name = default_name
       var port = 0
       var existing_server = false
 
       val getopts =
         Getopts("""
 Usage: isabelle server [OPTIONS]
 
   Options are:
     -L FILE      logging on FILE
     -c           console interaction with specified server
     -l           list servers (alternative operation)
     -n NAME      explicit server name (default: """ + default_name + """)
     -p PORT      explicit server port
     -s           assume existing server, no implicit startup
     -x           exit specified server (alternative operation)
 
   Manage resident Isabelle servers.
 """,
           "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
           "c" -> (_ => console = true),
           "l" -> (_ => operation_list = true),
           "n:" -> (arg => name = arg),
           "p:" -> (arg => port = Value.Int.parse(arg)),
           "s" -> (_ => existing_server = true),
           "x" -> (_ => operation_exit = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       if (operation_list) {
         for {
           server_info <- using(SQLite.open_database(Data.database))(list(_))
           if server_info.active
         } Output.writeln(server_info.toString, stdout = true)
       }
       else if (operation_exit) {
         val ok = Server.exit(name)
         sys.exit(if (ok) 0 else 2)
       }
       else {
         val log = Logger.make(log_file)
         val (server_info, server) =
           init(name, port = port, existing_server = existing_server, log = log)
         Output.writeln(server_info.toString, stdout = true)
         if (console) {
           using(server_info.connection())(connection => connection.tty_loop().join)
         }
         server.foreach(_.join)
       }
     })
 }
 
 class Server private(_port: Int, val log: Logger)
 {
   server =>
 
   private val server_socket = new ServerSocket(_port, 50, Server.localhost)
 
   private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session])
   def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString))
-  def the_session(id: UUID.T): Headless.Session = _sessions.value.get(id) getOrElse err_session(id)
+  def the_session(id: UUID.T): Headless.Session = _sessions.value.getOrElse(id, err_session(id))
   def add_session(entry: (UUID.T, Headless.Session)) { _sessions.change(_ + entry) }
   def remove_session(id: UUID.T): Headless.Session =
   {
     _sessions.change_result(sessions =>
       sessions.get(id) match {
         case Some(session) => (session, sessions - id)
         case None => err_session(id)
       })
   }
 
   def shutdown()
   {
     server_socket.close
 
     val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
     for ((_, session) <- sessions) {
       try {
         val result = session.stop()
         if (!result.ok) log("Session shutdown failed: return code " + result.rc)
       }
       catch { case ERROR(msg) => log("Session shutdown failed: " + msg) }
     }
   }
 
   def port: Int = server_socket.getLocalPort
   val password: String = UUID.random_string()
 
   override def toString: String = Server.print(port, password)
 
   private def handle(connection: Server.Connection)
   {
     using(new Server.Context(server, connection))(context =>
     {
       if (connection.read_password(password)) {
         connection.reply_ok(
           JSON.Object(
             "isabelle_id" -> Isabelle_System.isabelle_id(),
             "isabelle_version" -> Distribution.version))
 
         var finished = false
         while (!finished) {
           connection.read_message() match {
             case None => finished = true
             case Some("") => context.notify("Command 'help' provides list of commands")
             case Some(msg) =>
               val (name, argument) = Server.Argument.split(msg)
               name match {
                 case Server.Command(cmd) =>
                   argument match {
                     case Server.Argument(arg) =>
                       if (cmd.isDefinedAt((context, arg))) {
                         Exn.capture { cmd((context, arg)) } match {
                           case Exn.Res(task: Server.Task) =>
                             connection.reply_ok(JSON.Object(task.ident))
                             task.start
                           case Exn.Res(res) => connection.reply_ok(res)
                           case Exn.Exn(exn) =>
                             val err = Server.json_error(exn)
                             if (err.isEmpty) throw exn else connection.reply_error(err)
                         }
                       }
                       else {
                         connection.reply_error_message(
                           "Bad argument for command " + Library.single_quote(name),
                           "argument" -> argument)
                       }
                     case _ =>
                       connection.reply_error_message(
                         "Malformed argument for command " + Library.single_quote(name),
                         "argument" -> argument)
                   }
                 case _ => connection.reply_error("Bad command " + Library.single_quote(name))
               }
           }
         }
       }
     })
   }
 
   private lazy val server_thread: Thread =
     Standard_Thread.fork("server") {
       var finished = false
       while (!finished) {
         Exn.capture(server_socket.accept) match {
           case Exn.Res(socket) =>
             Standard_Thread.fork("server_connection")
               { using(Server.Connection(socket))(handle(_)) }
           case Exn.Exn(_) => finished = true
         }
       }
     }
 
   def start { server_thread }
 
   def join { server_thread.join; shutdown() }
 }
diff --git a/src/Pure/Tools/spell_checker.scala b/src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala
+++ b/src/Pure/Tools/spell_checker.scala
@@ -1,291 +1,291 @@
 /*  Title:      Pure/Tools/spell_checker.scala
     Author:     Makarius
 
 Spell checker with completion, based on JOrtho (see
 https://sourceforge.net/projects/jortho).
 */
 
 package isabelle
 
 
 import java.lang.Class
 
 import scala.collection.mutable
 import scala.annotation.tailrec
 import scala.collection.immutable.SortedMap
 
 
 object Spell_Checker
 {
   /* words within text */
 
   def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean)
     : List[Text.Info[String]] =
   {
     val result = new mutable.ListBuffer[Text.Info[String]]
     var offset = 0
 
     def apostrophe(c: Int): Boolean =
       c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
 
     @tailrec def scan(pred: Int => Boolean)
     {
       if (offset < text.length) {
         val c = text.codePointAt(offset)
         if (pred(c)) {
           offset += Character.charCount(c)
           scan(pred)
         }
       }
     }
 
     while (offset < text.length) {
       scan(c => !Character.isLetter(c))
       val start = offset
       scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
       val stop = offset
       if (stop - start >= 2) {
         val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop))
         if (mark(info)) result += info
       }
     }
     result.toList
   }
 
   def current_word(rendering: Rendering, range: Text.Range): Option[Text.Info[String]] =
   {
     for {
       spell_range <- rendering.spell_checker_point(range)
       text <- rendering.model.get_text(spell_range)
       info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
     } yield info
   }
 
 
   /* dictionaries */
 
   class Dictionary private[Spell_Checker](val path: Path)
   {
     val lang = path.drop_ext.file_name
     val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
     override def toString: String = lang
   }
 
   private object Decl
   {
     def apply(name: String, include: Boolean): String =
       if (include) name else "-" + name
 
     def unapply(decl: String): Option[(String, Boolean)] =
     {
       val decl1 = decl.trim
       if (decl1 == "" || decl1.startsWith("#")) None
       else
         Library.try_unprefix("-", decl1.trim) match {
           case None => Some((decl1, true))
           case Some(decl2) => Some((decl2, false))
         }
     }
   }
 
   def dictionaries(): List[Dictionary] =
     for {
       path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
       if path.is_file
     } yield new Dictionary(path)
 
 
   /* create spell checker */
 
   def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
 
   private sealed case class Update(include: Boolean, permanent: Boolean)
 }
 
 
 class Spell_Checker private(dictionary: Spell_Checker.Dictionary)
 {
   override def toString: String = dictionary.toString
 
 
   /* main dictionary content */
 
   private var dict = new Object
   private var updates = SortedMap.empty[String, Spell_Checker.Update]
 
   private def included_iterator(): Iterator[String] =
     for {
       (word, upd) <- updates.iterator
       if upd.include
     } yield word
 
   private def excluded(word: String): Boolean =
     updates.get(word) match {
       case Some(upd) => !upd.include
       case None => false
     }
 
   private def load()
   {
     val main_dictionary = split_lines(File.read_gzip(dictionary.path))
 
     val permanent_updates =
       if (dictionary.user_path.is_file)
         for {
           Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
         } yield (word, Spell_Checker.Update(include, true))
       else Nil
 
     updates =
       updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
         permanent_updates
 
     val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
     val factory_cons = factory_class.getConstructor()
     factory_cons.setAccessible(true)
     val factory = factory_cons.newInstance()
 
     val add = Untyped.method(factory_class, "add", classOf[String])
 
     for {
       word <- main_dictionary.iterator ++ included_iterator()
       if !excluded(word)
     } add.invoke(factory, word)
 
     dict = Untyped.method(factory_class, "create").invoke(factory)
   }
   load()
 
   private def save()
   {
     val permanent_decls =
       (for {
         (word, upd) <- updates.iterator
         if upd.permanent
       } yield Spell_Checker.Decl(word, upd.include)).toList
 
     if (permanent_decls.nonEmpty || dictionary.user_path.is_file) {
       val header = """# User updates for spell-checker dictionary
 #
 #   * each line contains at most one word
 #   * extra blanks are ignored
 #   * lines starting with "#" are stripped
 #   * lines starting with "-" indicate excluded words
 #
 #:mode=text:encoding=UTF-8:
 
 """
       Isabelle_System.mkdirs(dictionary.user_path.expand.dir)
       File.write(dictionary.user_path, header + cat_lines(permanent_decls))
     }
   }
 
   def update(word: String, include: Boolean, permanent: Boolean)
   {
     updates += (word -> Spell_Checker.Update(include, permanent))
 
     if (include) {
       if (permanent) save()
       Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
     }
     else { save(); load() }
   }
 
   def reset()
   {
     updates = SortedMap.empty
     load()
   }
 
   def reset_enabled(): Int =
-    updates.valuesIterator.filter(upd => !upd.permanent).length
+    updates.valuesIterator.count(upd => !upd.permanent)
 
 
   /* check known words */
 
   def contains(word: String): Boolean =
     Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]).
       invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
 
   def check(word: String): Boolean =
     word match {
       case Word.Case(c) if c != Word.Lowercase =>
         contains(word) || contains(Word.lowercase(word))
       case _ =>
         contains(word)
     }
 
   def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] =
     Spell_Checker.marked_words(base, text, info => !check(info.info))
 
 
   /* completion: suggestions for unknown words */
 
   private def suggestions(word: String): Option[List[String]] =
   {
     val res =
       Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
         invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
     if (res.isEmpty) None else Some(res)
   }
 
   def complete(word: String): List[String] =
     if (check(word)) Nil
     else {
       val word_case = Word.Case.unapply(word)
       def recover_case(s: String) =
         word_case match {
           case Some(c) => Word.Case(c, s)
           case None => s
         }
       val result =
         word_case match {
           case Some(c) if c != Word.Lowercase =>
             suggestions(word) orElse suggestions(Word.lowercase(word))
           case _ =>
             suggestions(word)
         }
       result.getOrElse(Nil).map(recover_case)
     }
 
   def completion(rendering: Rendering, caret: Text.Offset): Option[Completion.Result] =
   {
     val caret_range = rendering.before_caret_range(caret)
     for {
       word <- Spell_Checker.current_word(rendering, caret_range)
       words = complete(word.info)
       if words.nonEmpty
       descr = "(from dictionary " + quote(dictionary.toString) + ")"
       items =
         words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
     } yield Completion.Result(word.range, word.info, false, items)
   }
 }
 
 class Spell_Checker_Variable
 {
   private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None)
   private var current_spell_checker = no_spell_checker
 
   def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 }
 
   def update(options: Options): Unit = synchronized {
     if (options.bool("spell_checker")) {
       val lang = options.string("spell_checker_dictionary")
       if (current_spell_checker._1 != lang) {
         Spell_Checker.dictionaries.find(_.lang == lang) match {
           case Some(dictionary) =>
             val spell_checker =
               Exn.capture { Spell_Checker(dictionary) } match {
                 case Exn.Res(spell_checker) => Some(spell_checker)
                 case Exn.Exn(_) => None
               }
             current_spell_checker = (lang, spell_checker)
           case None =>
             current_spell_checker = no_spell_checker
         }
       }
     }
     else current_spell_checker = no_spell_checker
   }
 }
diff --git a/src/Tools/Graphview/graph_panel.scala b/src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala
+++ b/src/Tools/Graphview/graph_panel.scala
@@ -1,360 +1,360 @@
 /*  Title:      Tools/Graphview/graph_panel.scala
     Author:     Markus Kaiser, TU Muenchen
     Author:     Makarius
 
 GUI panel for graph layout.
 */
 
 package isabelle.graphview
 
 
 import isabelle._
 
 import java.awt.{Dimension, Graphics2D, Point, Rectangle}
 import java.awt.geom.{AffineTransform, Point2D}
 import javax.imageio.ImageIO
 import javax.swing.{JScrollPane, JComponent, SwingUtilities}
 import javax.swing.border.EmptyBorder
 
 import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser, Panel, ScrollPane}
 import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent}
 
 
 class Graph_Panel(val graphview: Graphview) extends BorderPanel
 {
   graph_panel =>
 
 
 
   /** graph **/
 
   /* painter */
 
   private val painter = new Panel
   {
     override def paint(gfx: Graphics2D)
     {
       super.paintComponent(gfx)
 
       gfx.setColor(graphview.background_color)
       gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
 
       gfx.transform(Transform())
       graphview.paint(gfx)
     }
   }
 
   def set_preferred_size()
   {
     val box = graphview.bounding_box()
     val s = Transform.scale_discrete
     painter.preferredSize = new Dimension((box.width * s).ceil.toInt, (box.height * s).ceil.toInt)
     painter.revalidate()
   }
 
   def refresh()
   {
     if (painter != null) {
       set_preferred_size()
       painter.repaint()
     }
   }
 
   def scroll_to_node(node: Graph_Display.Node)
   {
     val gap = graphview.metrics.gap
     val info = graphview.layout.get_node(node)
 
     val t = Transform()
     val p =
       t.transform(new Point2D.Double(info.x - info.width2 - gap, info.y - info.height2 - gap), null)
     val q =
       t.transform(new Point2D.Double(info.x + info.width2 + gap, info.y + info.height2 + gap), null)
 
     painter.peer.scrollRectToVisible(
       new Rectangle(p.getX.toInt, p.getY.toInt,
         (q.getX - p.getX).ceil.toInt, (q.getY - p.getY).ceil.toInt))
   }
 
 
   /* scrollable graph pane */
 
   private val graph_pane: ScrollPane = new ScrollPane(painter) {
     tooltip = ""
 
     override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
       override def getToolTipText(event: java.awt.event.MouseEvent): String =
         graphview.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
           case Some(node) =>
             graphview.model.full_graph.get_node(node) match {
               case Nil => null
               case content =>
                 graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, content)
             }
           case None => null
         }
     }
 
     horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
     verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
 
     listenTo(mouse.moves)
     listenTo(mouse.clicks)
     reactions +=
     {
       case MousePressed(_, p, _, _, _) =>
         Mouse_Interaction.pressed(p)
         painter.repaint()
       case MouseDragged(_, to, _) =>
         Mouse_Interaction.dragged(to)
         painter.repaint()
       case e @ MouseClicked(_, p, m, n, _) =>
         Mouse_Interaction.clicked(p, m, n, SwingUtilities.isRightMouseButton(e.peer))
         painter.repaint()
     }
 
     contents = painter
   }
   graph_pane.peer.getVerticalScrollBar.setUnitIncrement(10)
 
 
   /* transform */
 
   def rescale(s: Double)
   {
     Transform.scale = s
     if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt)
     refresh()
   }
 
   def fit_to_window()
   {
     Transform.fit_to_window()
     refresh()
   }
 
   private object Transform
   {
     private var _scale: Double = 1.0
     def scale: Double = _scale
     def scale_=(s: Double)
     {
       _scale = (s min 10.0) max 0.1
     }
 
     def scale_discrete: Double =
     {
       val font_height = GUI.line_metrics(graphview.metrics.font).getHeight.toInt
       (scale * font_height).floor / font_height
     }
 
-    def apply() =
+    def apply(): AffineTransform =
     {
       val box = graphview.bounding_box()
       val t = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
       t.translate(- box.x, - box.y)
       t
     }
 
     def fit_to_window()
     {
       if (graphview.visible_graph.is_empty)
         rescale(1.0)
       else {
         val box = graphview.bounding_box()
         rescale((size.width / box.width) min (size.height / box.height))
       }
     }
 
     def pane_to_graph_coordinates(at: Point2D): Point2D =
     {
       val s = Transform.scale_discrete
       val p = Transform().inverseTransform(graph_pane.peer.getViewport.getViewPosition, null)
 
       p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s)
       p
     }
   }
 
 
   /* interaction */
 
   graphview.model.Colors.events += { case _ => painter.repaint() }
   graphview.model.Mutators.events += { case _ => painter.repaint() }
 
   private object Mouse_Interaction
   {
     private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) =
       (new Point(0, 0), Nil, Nil)
 
     def pressed(at: Point)
     {
       val c = Transform.pane_to_graph_coordinates(at)
       val l =
         graphview.find_node(c) match {
           case Some(node) =>
             if (graphview.Selection.contains(node)) graphview.Selection.get()
             else List(node)
           case None => Nil
         }
       val d =
         l match {
           case Nil => graphview.find_dummy(c).toList
           case _ => Nil
         }
       draginfo = (at, l, d)
     }
 
     def dragged(to: Point)
     {
       val (from, p, d) = draginfo
 
       val s = Transform.scale_discrete
       val dx = to.x - from.x
       val dy = to.y - from.y
 
       (p, d) match {
         case (Nil, Nil) =>
           val r = graph_pane.peer.getViewport.getViewRect
           r.translate(- dx, - dy)
           painter.peer.scrollRectToVisible(r)
 
         case (Nil, ds) =>
           ds.foreach(d => graphview.translate_vertex(d, dx / s, dy / s))
 
         case (ls, _) =>
           ls.foreach(l => graphview.translate_vertex(Layout.Node(l), dx / s, dy / s))
       }
 
       draginfo = (to, p, d)
     }
 
     def clicked(at: Point, m: Key.Modifiers, clicks: Int, right_click: Boolean)
     {
       val c = Transform.pane_to_graph_coordinates(at)
 
       if (clicks < 2) {
         if (right_click) {
           // FIXME
           if (false) {
             val menu = Popups(graph_panel, graphview.find_node(c), graphview.Selection.get())
             menu.show(graph_pane.peer, at.x, at.y)
           }
         }
         else {
           (graphview.find_node(c), m) match {
             case (Some(node), Key.Modifier.Control) => graphview.Selection.add(node)
             case (None, Key.Modifier.Control) =>
 
             case (Some(node), Key.Modifier.Shift) => graphview.Selection.add(node)
             case (None, Key.Modifier.Shift) =>
 
             case (Some(node), _) =>
               graphview.Selection.clear()
               graphview.Selection.add(node)
             case (None, _) =>
               graphview.Selection.clear()
           }
         }
       }
     }
   }
 
 
 
   /** controls **/
 
   private val mutator_dialog =
     new Mutator_Dialog(graphview, graphview.model.Mutators, "Filters", "Hide", false)
   private val color_dialog =
     new Mutator_Dialog(graphview, graphview.model.Colors, "Colorations")
 
   private val chooser = new FileChooser {
     fileSelectionMode = FileChooser.SelectionMode.FilesOnly
     title = "Save image (.png or .pdf)"
   }
 
   private val show_content = new CheckBox() {
     selected = graphview.show_content
     action = Action("Show content") {
       graphview.show_content = selected
       graphview.update_layout()
       refresh()
     }
     tooltip = "Show full node content within graph layout"
   }
 
   private val show_arrow_heads = new CheckBox() {
     selected = graphview.show_arrow_heads
     action = Action("Show arrow heads") {
       graphview.show_arrow_heads = selected
       painter.repaint()
     }
     tooltip = "Draw edges with explicit arrow heads"
   }
 
   private val show_dummies = new CheckBox() {
     selected = graphview.show_dummies
     action = Action("Show dummies") {
       graphview.show_dummies = selected
       painter.repaint()
     }
     tooltip = "Draw dummy nodes within graph layout, for easier mouse dragging"
   }
 
   private val save_image = new Button {
     action = Action("Save image") {
       chooser.showSaveDialog(this) match {
         case FileChooser.Result.Approve =>
           try { Graph_File.write(chooser.selectedFile, graphview) }
           catch {
             case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg))
           }
         case _ =>
       }
     }
     tooltip = "Save current graph layout as PNG or PDF"
   }
 
   private val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
 
   private val fit_window = new Button {
     action = Action("Fit to window") { fit_to_window() }
     tooltip = "Zoom to fit window width and height"
   }
 
   private val update_layout = new Button {
     action = Action("Update layout") {
       graphview.update_layout()
       refresh()
     }
     tooltip = "Regenerate graph layout according to built-in algorithm"
   }
 
   private val editor_style = new CheckBox() {
     selected = graphview.editor_style
     action = Action("Editor style") {
       graphview.editor_style = selected
       graphview.update_layout()
       refresh()
     }
     tooltip = "Use editor font and colors for painting"
   }
 
   private val colorations = new Button { action = Action("Colorations") { color_dialog.open } }
   private val filters = new Button { action = Action("Filters") { mutator_dialog.open } }
 
   private val controls =
     Wrap_Panel(
       List(show_content, show_arrow_heads, show_dummies,
         save_image, zoom, fit_window, update_layout, editor_style)) // FIXME colorations, filters
 
 
 
   /** main layout **/
 
   layout(graph_pane) = BorderPanel.Position.Center
   layout(controls) = BorderPanel.Position.North
 
   rescale(1.0)
 }
diff --git a/src/Tools/Graphview/layout.scala b/src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala
+++ b/src/Tools/Graphview/layout.scala
@@ -1,407 +1,407 @@
 /*  Title:      Tools/Graphview/layout.scala
     Author:     Markus Kaiser, TU Muenchen
     Author:     Makarius
 
 DAG layout according to:
 
   Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing,
   DIMACS International Workshop (GD'94), Springer LNCS 894, 1995.
 
   https://doi.org/10.1007/3-540-58950-3_371
   ftp://ftp.cs.uni-sb.de/pub/graphics/vcg/doc/tr-A03-94.ps.gz
 */
 
 package isabelle.graphview
 
 
 import isabelle._
 
 
 object Layout
 {
   /* graph structure */
 
   object Vertex
   {
     object Ordering extends scala.math.Ordering[Vertex]
     {
       def compare(v1: Vertex, v2: Vertex): Int =
         (v1, v2) match {
           case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b)
           case (Dummy(a1, a2, i), Dummy(b1, b2, j)) =>
             Graph_Display.Node.Ordering.compare(a1, b1) match {
               case 0 =>
                 Graph_Display.Node.Ordering.compare(a2, b2) match {
                   case 0 => i compare j
                   case ord => ord
                 }
               case ord => ord
             }
           case (Node(a), Dummy(b, _, _)) =>
             Graph_Display.Node.Ordering.compare(a, b) match {
               case 0 => -1
               case ord => ord
             }
           case (Dummy(a, _, _), Node(b)) =>
             Graph_Display.Node.Ordering.compare(a, b) match {
               case 0 => 1
               case ord => ord
             }
         }
     }
   }
 
   sealed abstract class Vertex
   case class Node(node: Graph_Display.Node) extends Vertex
   case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex
 
   sealed case class Info(
     x: Double, y: Double, width2: Double, height2: Double, lines: List[String])
   {
     def left: Double = x - width2
     def right: Double = x + width2
     def width: Double = 2 * width2
     def height: Double = 2 * height2
   }
 
   type Graph = isabelle.Graph[Vertex, Info]
 
   def make_graph(entries: List[((Vertex, Info), List[Vertex])]): Graph =
     isabelle.Graph.make(entries)(Vertex.Ordering)
 
   val empty_graph: Graph = make_graph(Nil)
 
 
   /* vertex x coordinate */
 
   private def vertex_left(graph: Graph, v: Vertex) = graph.get_node(v).left
   private def vertex_right(graph: Graph, v: Vertex) = graph.get_node(v).right
 
   private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph =
     if (dx == 0.0) graph else graph.map_node(v, info => info.copy(x = info.x + dx))
 
 
   /* layout */
 
   val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph)
 
 
   private type Levels = Map[Vertex, Int]
   private val empty_levels: Levels = Map.empty
 
   def make(options: Options, metrics: Metrics,
     node_text: (Graph_Display.Node, XML.Body) => String,
     input_graph: Graph_Display.Graph): Layout =
   {
     if (input_graph.is_empty) empty
     else {
       /* initial graph */
 
       val initial_graph =
         make_graph(
           input_graph.iterator.map(
             { case (a, (content, (_, bs))) =>
                 val lines = split_lines(node_text(a, content))
                 val w2 = metrics.node_width2(lines)
                 val h2 = metrics.node_height2(lines.length)
                 ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node(_)))
             }).toList)
 
       val initial_levels: Levels =
         (empty_levels /: initial_graph.topological_order) {
           case (levels, vertex) =>
             val level =
               1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) }
             levels + (vertex -> level)
         }
 
 
       /* graph with dummies */
 
       val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil)
 
       val (dummy_graph, dummy_levels) =
         ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
             case ((graph, levels), (node1, node2)) =>
               val v1 = Node(node1); val l1 = levels(v1)
               val v2 = Node(node2); val l2 = levels(v2)
               if (l2 - l1 <= 1) (graph, levels)
               else {
                 val dummies_levels =
                   (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
                     yield (Dummy(node1, node2, i), l)).toList
                 val dummies = dummies_levels.map(_._1)
 
                 val levels1 = (levels /: dummies_levels)(_ + _)
                 val graph1 =
                   ((graph /: dummies)(_.new_node(_, dummy_info)).del_edge(v1, v2) /:
                     (v1 :: dummies ::: List(v2)).sliding(2)) {
                       case (g, List(a, b)) => g.add_edge(a, b) }
                 (graph1, levels1)
               }
           }
 
 
       /* minimize edge crossings and initial coordinates */
 
       val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels))
 
       val levels_graph: Graph =
         (((dummy_graph, 0.0) /: levels) {
           case ((graph, y), level) =>
             val num_lines = (0 /: level) { case (n, v) => n max graph.get_node(v).lines.length }
             val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size }
 
             val y1 = y + metrics.node_height2(num_lines)
 
             val graph1 =
               (((graph, 0.0) /: level) { case ((g, x), v) =>
                 val info = g.get_node(v)
                 val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
                 val x1 = x + info.width + metrics.gap
                 (g1, x1)
               })._1
 
             val y2 = y1 + metrics.level_height2(num_lines, num_edges)
 
             (graph1, y2)
         })._1
 
 
       /* pendulum/rubberband layout */
 
       val output_graph =
         rubberband(options, metrics, levels,
           pendulum(options, metrics, levels, levels_graph))
 
       new Layout(metrics, input_graph, output_graph)
     }
   }
 
 
 
   /** edge crossings **/
 
   private type Level = List[Vertex]
 
   private def minimize_crossings(
     options: Options, graph: Graph, levels: List[Level]): List[Level] =
   {
     def resort(parent: Level, child: Level, top_down: Boolean): Level =
       child.map(v => {
           val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
           val weight =
             (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
           (v, weight)
       }).sortBy(_._2).map(_._1)
 
     ((levels, count_crossings(graph, levels)) /:
       (1 to (2 * options.int("graphview_iterations_minimize_crossings")))) {
       case ((old_levels, old_crossings), iteration) =>
         val top_down = (iteration % 2 == 1)
         val new_levels =
           if (top_down)
             (List(old_levels.head) /: old_levels.tail)((tops, bot) =>
               resort(tops.head, bot, top_down) :: tops).reverse
           else {
             val rev_old_levels = old_levels.reverse
             (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) =>
               resort(bots.head, top, top_down) :: bots)
           }
         val new_crossings = count_crossings(graph, new_levels)
         if (new_crossings < old_crossings)
           (new_levels, new_crossings)
         else
           (old_levels, old_crossings)
     }._1
   }
 
   private def level_list(levels: Levels): List[Level] =
   {
     val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
     val buckets = new Array[Level](max_lev + 1)
     for (l <- 0 to max_lev) { buckets(l) = Nil }
     for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
     buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
   }
 
   private def count_crossings(graph: Graph, levels: List[Level]): Int =
     levels.iterator.sliding(2).map {
       case List(top, bot) =>
         top.iterator.zipWithIndex.map {
           case (outer_parent, outer_parent_index) =>
             graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child =>
               (0 until outer_parent_index).iterator.map(inner_parent =>
-                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)).
-                  filter(inner_child => outer_child < inner_child).size).sum).sum
+                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
+                  .count(inner_child => outer_child < inner_child)).sum).sum
         }.sum
       case _ => 0
     }.sum
 
 
 
   /** pendulum method **/
 
   /*This is an auxiliary class which is used by the layout algorithm when
     calculating coordinates with the "pendulum method". A "region" is a
     group of vertices which "stick together".*/
   private class Region(val content: List[Vertex])
   {
     def distance(metrics: Metrics, graph: Graph, that: Region): Double =
       vertex_left(graph, that.content.head) -
       vertex_right(graph, this.content.last) -
       metrics.gap
 
     def deflection(graph: Graph, top_down: Boolean): Double =
       ((for (a <- content.iterator) yield {
         val x = graph.get_node(a).x
         val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
         bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
       }).sum / content.length).round.toDouble
 
     def move(graph: Graph, dx: Double): Graph =
       if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx))
 
     def combine(that: Region): Region = new Region(content ::: that.content)
   }
 
   private def pendulum(
     options: Options, metrics: Metrics, levels: List[Level], levels_graph: Graph): Graph =
   {
     def combine_regions(graph: Graph, top_down: Boolean, level: List[Region]): List[Region] =
       level match {
         case r1 :: rest =>
           val rest1 = combine_regions(graph, top_down, rest)
           rest1 match {
             case r2 :: rest2 =>
               val d1 = r1.deflection(graph, top_down)
               val d2 = r2.deflection(graph, top_down)
               if (// Do regions touch?
                   r1.distance(metrics, graph, r2) <= 0.0 &&
                   // Do they influence each other?
                   (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0))
                 r1.combine(r2) :: rest2
               else r1 :: rest1
             case _ => r1 :: rest1
           }
         case _ => level
       }
 
     def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) =
     {
-      ((graph, false) /: (0 until level.length)) {
+      ((graph, false) /: level.indices) {
         case ((graph, moved), i) =>
           val r = level(i)
           val d = r.deflection(graph, top_down)
           val dx =
             if (d < 0.0 && i > 0)
               - (level(i - 1).distance(metrics, graph, r) min (- d))
             else if (d >= 0.0 && i < level.length - 1)
               r.distance(metrics, graph, level(i + 1)) min d
             else d
           (r.move(graph, dx), moved || d != 0.0)
       }
     }
 
     val initial_regions = levels.map(level => level.map(l => new Region(List(l))))
 
     ((levels_graph, initial_regions, true) /:
       (1 to (2 * options.int("graphview_iterations_pendulum")))) {
       case ((graph, regions, moved), iteration) =>
         val top_down = (iteration % 2 == 1)
         if (moved) {
           val (graph1, regions1, moved1) =
             ((graph, List.empty[List[Region]], false) /:
               (if (top_down) regions else regions.reverse)) { case ((graph, tops, moved), bot) =>
                 val bot1 = combine_regions(graph, top_down, bot)
                 val (graph1, moved1) = deflect(bot1, top_down, graph)
                 (graph1, bot1 :: tops, moved || moved1)
             }
           (graph1, regions1.reverse, moved1)
         }
         else (graph, regions, moved)
     }._1
   }
 
 
 
   /** rubberband method **/
 
   private def force_weight(graph: Graph, v: Vertex): Double =
   {
     val preds = graph.imm_preds(v)
     val succs = graph.imm_succs(v)
     val n = preds.size + succs.size
     if (n == 0) 0.0
     else {
       val x = graph.get_node(v).x
       ((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n
     }
   }
 
   private def rubberband(
     options: Options, metrics: Metrics, levels: List[Level], graph: Graph): Graph =
   {
     val gap = metrics.gap
 
     (graph /: (1 to (2 * options.int("graphview_iterations_rubberband")))) { case (graph, _) =>
       (graph /: levels) { case (graph, level) =>
         val m = level.length - 1
         (graph /: level.iterator.zipWithIndex) {
           case (g, (v, i)) =>
             val d = force_weight(g, v)
             if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
                 d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
               move_vertex(g, v, d.round.toDouble)
             else g
         }
       }
     }
   }
 }
 
 final class Layout private(
   val metrics: Metrics,
   val input_graph: Graph_Display.Graph,
   val output_graph: Layout.Graph)
 {
   /* vertex coordinates */
 
   def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout =
   {
     if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this
     else {
       val output_graph1 =
         output_graph.map_node(v, info => info.copy(x = info.x + dx, y = info.y + dy))
       new Layout(metrics, input_graph, output_graph1)
     }
   }
 
 
   /* regular nodes */
 
   def get_node(node: Graph_Display.Node): Layout.Info =
     output_graph.get_node(Layout.Node(node))
 
   def nodes_iterator: Iterator[Layout.Info] =
     for ((_: Layout.Node, (info, _)) <- output_graph.iterator) yield info
 
 
   /* dummies */
 
   def dummies_iterator: Iterator[Layout.Info] =
     for ((_: Layout.Dummy, (info, _)) <- output_graph.iterator) yield info
 
   def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Info] =
     new Iterator[Layout.Info] {
       private var index = 0
       def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index))
       def next: Layout.Info =
       {
         val info = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
         index += 1
         info
       }
     }
 }
 
diff --git a/src/Tools/Graphview/metrics.scala b/src/Tools/Graphview/metrics.scala
--- a/src/Tools/Graphview/metrics.scala
+++ b/src/Tools/Graphview/metrics.scala
@@ -1,63 +1,63 @@
 /*  Title:      Tools/Graphview/metrics.scala
     Author:     Makarius
 
 Physical metrics for layout and painting.
 */
 
 package isabelle.graphview
 
 
 import isabelle._
 
 import java.awt.{Font, RenderingHints}
 import java.awt.font.FontRenderContext
 import java.awt.geom.Rectangle2D
 
 
 object Metrics
 {
   val rendering_hints: RenderingHints =
   {
     val hints = new java.util.HashMap[RenderingHints.Key, AnyRef]
     hints.put(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON)
     hints.put(RenderingHints.KEY_FRACTIONALMETRICS, RenderingHints.VALUE_FRACTIONALMETRICS_ON)
     new RenderingHints(hints)
   }
 
   val font_render_context: FontRenderContext =
     new FontRenderContext(null, true, true)
 
   def apply(font: Font): Metrics = new Metrics(font)
 
   val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12))
 }
 
 class Metrics private(val font: Font)
 {
   def string_bounds(s: String): Rectangle2D = font.getStringBounds(s, Metrics.font_render_context)
   private val mix = string_bounds("mix")
-  val space_width = string_bounds(" ").getWidth
+  val space_width: Double = string_bounds(" ").getWidth
   def char_width: Double = mix.getWidth / 3
   def height: Double = mix.getHeight
   def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent
 
   def gap: Double = mix.getWidth.ceil
 
   def dummy_size2: Double = (char_width / 2).ceil
 
   def node_width2(lines: List[String]): Double =
     (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2).ceil
 
   def node_height2(num_lines: Int): Double =
     ((height.ceil * (num_lines max 1) + char_width) / 2).ceil
 
   def level_height2(num_lines: Int, num_edges: Int): Double =
     (node_height2(num_lines) + gap) max (node_height2(1) * (num_edges max 5))
 
   object Pretty_Metric extends Pretty.Metric
   {
-    val unit = space_width max 1.0
+    val unit: Double = space_width max 1.0
     def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit
   }
 }
 
diff --git a/src/Tools/Graphview/mutator_dialog.scala b/src/Tools/Graphview/mutator_dialog.scala
--- a/src/Tools/Graphview/mutator_dialog.scala
+++ b/src/Tools/Graphview/mutator_dialog.scala
@@ -1,382 +1,381 @@
 /*  Title:      Tools/Graphview/mutator_dialog.scala
     Author:     Markus Kaiser, TU Muenchen
     Author:     Makarius
 
 Mutator selection and configuration dialog.
 */
 
 package isabelle.graphview
 
 
 import isabelle._
 
 import java.awt.Color
 import java.awt.FocusTraversalPolicy
 import javax.swing.JColorChooser
 import javax.swing.border.EmptyBorder
 import scala.swing.{Dialog, Button, BoxPanel, Swing, Orientation, ComboBox, Action,
   Dimension, BorderPanel, ScrollPane, Label, CheckBox, Alignment, Component, TextField}
 import scala.swing.event.ValueChanged
 
 
 class Mutator_Dialog(
     graphview: Graphview,
     container: Mutator_Container,
     caption: String,
     reverse_caption: String = "Inverse",
     show_color_chooser: Boolean = true)
   extends Dialog
 {
   title = caption
 
   private var _panels: List[Mutator_Panel] = Nil
   private def panels = _panels
   private def panels_=(panels: List[Mutator_Panel])
   {
     _panels = panels
     paint_panels()
   }
 
   container.events +=
   {
     case Mutator_Event.Add(m) => add_panel(new Mutator_Panel(m))
     case Mutator_Event.New_List(ms) => panels = get_panels(ms)
   }
 
   override def open()
   {
     if (!visible) panels = get_panels(container())
     super.open
   }
 
   minimumSize = new Dimension(700, 200)
   preferredSize = new Dimension(1000, 300)
   peer.setFocusTraversalPolicy(Focus_Traveral_Policy)
 
   private def get_panels(m: List[Mutator.Info]): List[Mutator_Panel] =
     m.filter({ case Mutator.Info(_, _, Mutator.Identity()) => false case _ => true })
     .map(m => new Mutator_Panel(m))
 
   private def get_mutators(panels: List[Mutator_Panel]): List[Mutator.Info] =
     panels.map(panel => panel.get_mutator)
 
   private def movePanelUp(m: Mutator_Panel) =
   {
     def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] =
       l match {
         case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs)
         case _ => l
       }
 
     panels = moveUp(panels)
   }
 
   private def movePanelDown(m: Mutator_Panel) =
   {
     def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] =
       l match {
         case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs)
         case _ => l
       }
 
     panels = moveDown(panels)
   }
 
   private def removePanel(m: Mutator_Panel)
   {
     panels = panels.filter(_ != m).toList
   }
 
   private def add_panel(m: Mutator_Panel)
   {
     panels = panels ::: List(m)
   }
 
   def paint_panels()
   {
     Focus_Traveral_Policy.clear
     filter_panel.contents.clear
     panels.map(x => {
         filter_panel.contents += x
         Focus_Traveral_Policy.addAll(x.focusList)
       })
     filter_panel.contents += Swing.VGlue
 
     Focus_Traveral_Policy.add(mutator_box.peer.asInstanceOf[java.awt.Component])
     Focus_Traveral_Policy.add(add_button.peer)
     Focus_Traveral_Policy.add(apply_button.peer)
     Focus_Traveral_Policy.add(cancel_button.peer)
     filter_panel.revalidate
     filter_panel.repaint
   }
 
   val filter_panel = new BoxPanel(Orientation.Vertical) {}
 
   private val mutator_box = new ComboBox[Mutator](container.available)
 
   private val add_button = new Button {
     action = Action("Add") {
       add_panel(
         new Mutator_Panel(Mutator.Info(true, graphview.Colors.next, mutator_box.selection.item)))
     }
   }
 
   private val apply_button = new Button {
     action = Action("Apply") { container(get_mutators(panels)) }
   }
 
   private val reset_button = new Button {
     action = Action("Reset") { panels = get_panels(container()) }
   }
 
   private val cancel_button = new Button {
     action = Action("Close") { close }
   }
   defaultButton = cancel_button
 
   private val botPanel = new BoxPanel(Orientation.Horizontal) {
     border = new EmptyBorder(10, 0, 0, 0)
 
     contents += mutator_box
     contents += Swing.RigidBox(new Dimension(10, 0))
     contents += add_button
 
     contents += Swing.HGlue
     contents += Swing.RigidBox(new Dimension(30, 0))
     contents += apply_button
 
     contents += Swing.RigidBox(new Dimension(5, 0))
     contents += reset_button
 
     contents += Swing.RigidBox(new Dimension(5, 0))
     contents += cancel_button
   }
 
   contents = new BorderPanel {
     border = new EmptyBorder(5, 5, 5, 5)
 
     layout(new ScrollPane(filter_panel)) = BorderPanel.Position.Center
     layout(botPanel) = BorderPanel.Position.South
   }
 
   private class Mutator_Panel(initials: Mutator.Info)
     extends BoxPanel(Orientation.Horizontal)
   {
     private val inputs: List[(String, Input)] = get_inputs()
     var focusList = List.empty[java.awt.Component]
     private val enabledBox = new Check_Box_Input("Enabled", initials.enabled)
 
     border = new EmptyBorder(5, 5, 5, 5)
     maximumSize = new Dimension(Integer.MAX_VALUE, 30)
     background = initials.color
 
     contents += new Label(initials.mutator.name) {
       preferredSize = new Dimension(175, 20)
       horizontalAlignment = Alignment.Left
       if (initials.mutator.description != "") tooltip = initials.mutator.description
     }
     contents += Swing.RigidBox(new Dimension(10, 0))
     contents += enabledBox
     contents += Swing.RigidBox(new Dimension(5, 0))
     focusList = enabledBox.peer :: focusList
-    inputs.map(_ match {
+    inputs.map({
       case (n, c) =>
         contents += Swing.RigidBox(new Dimension(10, 0))
         if (n != "") {
           contents += new Label(n)
           contents += Swing.RigidBox(new Dimension(5, 0))
         }
         contents += c.asInstanceOf[Component]
 
         focusList = c.asInstanceOf[Component].peer :: focusList
-      case _ =>
     })
 
     {
       val t = this
       contents += Swing.HGlue
       contents += Swing.RigidBox(new Dimension(10, 0))
 
       if (show_color_chooser) {
         contents += new Button {
           maximumSize = new Dimension(20, 20)
 
           action = Action("Color") {
             t.background =
               JColorChooser.showDialog(t.peer, "Choose new Color", t.background)
           }
 
           focusList = this.peer :: focusList
         }
         contents += Swing.RigidBox(new Dimension(2, 0))
       }
 
       contents += new Button {
         maximumSize = new Dimension(20, 20)
 
         action = Action("Up") {
           movePanelUp(t)
         }
 
         focusList = this.peer :: focusList
       }
       contents += Swing.RigidBox(new Dimension(2, 0))
       contents += new Button {
         maximumSize = new Dimension(20, 20)
 
         action = Action("Down") {
           movePanelDown(t)
         }
 
         focusList = this.peer :: focusList
       }
       contents += Swing.RigidBox(new Dimension(2, 0))
       contents += new Button {
         maximumSize = new Dimension(20, 20)
 
         action = Action("Del") {
           removePanel(t)
         }
 
         focusList = this.peer :: focusList
       }
     }
 
     focusList = focusList.reverse
 
     def get_mutator: Mutator.Info =
     {
       val model = graphview.model
       val m =
         initials.mutator match {
           case Mutator.Identity() =>
             Mutator.Identity()
           case Mutator.Node_Expression(r, _, _, _) =>
             val r1 = inputs(2)._2.string
             Mutator.Node_Expression(
               if (Library.make_regex(r1).isDefined) r1 else r,
               inputs(3)._2.bool,
               // "Parents" means "Show parents" or "Matching Children"
               inputs(1)._2.bool,
               inputs(0)._2.bool)
           case Mutator.Node_List(_, _, _, _) =>
             Mutator.Node_List(
               for {
                 ident <- space_explode(',', inputs(2)._2.string)
                 node <- model.find_node(ident)
               } yield node,
               inputs(3)._2.bool,
               // "Parents" means "Show parents" or "Matching Children"
               inputs(1)._2.bool,
               inputs(0)._2.bool)
           case Mutator.Edge_Endpoints(_) =>
             (model.find_node(inputs(0)._2.string), model.find_node(inputs(1)._2.string)) match {
               case (Some(node1), Some(node2)) =>
                 Mutator.Edge_Endpoints((node1, node2))
               case _ =>
                 Mutator.Identity()
             }
           case Mutator.Add_Node_Expression(r) =>
             val r1 = inputs(0)._2.string
             Mutator.Add_Node_Expression(if (Library.make_regex(r1).isDefined) r1 else r)
           case Mutator.Add_Transitive_Closure(_, _) =>
             Mutator.Add_Transitive_Closure(
               inputs(0)._2.bool,
               inputs(1)._2.bool)
           case _ =>
             Mutator.Identity()
         }
 
       Mutator.Info(enabledBox.selected, background, m)
     }
 
     private def get_inputs(): List[(String, Input)] =
       initials.mutator match {
         case Mutator.Node_Expression(regex, reverse, check_parents, check_children) =>
           List(
             ("", new Check_Box_Input("Parents", check_children)),
             ("", new Check_Box_Input("Children", check_parents)),
             ("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)),
             ("", new Check_Box_Input(reverse_caption, reverse)))
         case Mutator.Node_List(list, reverse, check_parents, check_children) =>
           List(
             ("", new Check_Box_Input("Parents", check_children)),
             ("", new Check_Box_Input("Children", check_parents)),
             ("Names", new Text_Field_Input(list.map(_.ident).mkString(","))),
             ("", new Check_Box_Input(reverse_caption, reverse)))
         case Mutator.Edge_Endpoints((source, dest)) =>
           List(
             ("Source", new Text_Field_Input(source.ident)),
             ("Destination", new Text_Field_Input(dest.ident)))
         case Mutator.Add_Node_Expression(regex) =>
           List(("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)))
         case Mutator.Add_Transitive_Closure(parents, children) =>
           List(
             ("", new Check_Box_Input("Parents", parents)),
             ("", new Check_Box_Input("Children", children)))
         case _ => Nil
       }
   }
 
   private trait Input
   {
     def string: String
     def bool: Boolean
   }
 
   private class Text_Field_Input(txt: String, check: String => Boolean = (_: String) => true)
     extends TextField(txt) with Input
   {
     preferredSize = new Dimension(125, 18)
 
     private val default_foreground = foreground
     reactions +=
     {
       case ValueChanged(_) =>
         foreground = if (check(text)) default_foreground else graphview.error_color
     }
 
     def string = text
     def bool = true
   }
 
   private class Check_Box_Input(txt: String, s: Boolean) extends CheckBox(txt) with Input
   {
     selected = s
 
     def string = ""
     def bool = selected
   }
 
   private object Focus_Traveral_Policy extends FocusTraversalPolicy
   {
     private var items = Vector.empty[java.awt.Component]
 
     def add(c: java.awt.Component) { items = items :+ c }
     def addAll(cs: TraversableOnce[java.awt.Component]) { items = items ++ cs }
     def clear() { items = Vector.empty }
 
     def getComponentAfter(root: java.awt.Container, c: java.awt.Component): java.awt.Component =
     {
       val i = items.indexOf(c)
       if (i < 0) getDefaultComponent(root)
       else items((i + 1) % items.length)
     }
 
     def getComponentBefore(root: java.awt.Container, c: java.awt.Component): java.awt.Component =
     {
       val i = items.indexOf(c)
       if (i < 0) getDefaultComponent(root)
       else items((i - 1) % items.length)
     }
 
     def getFirstComponent(root: java.awt.Container): java.awt.Component =
-      if (items.length > 0) items(0) else null
+      if (items.nonEmpty) items(0) else null
 
     def getDefaultComponent(root: java.awt.Container): java.awt.Component =
       getFirstComponent(root)
 
     def getLastComponent(root: java.awt.Container): java.awt.Component =
-      if (items.length > 0) items.last else null
+      if (items.nonEmpty) items.last else null
   }
 }
\ No newline at end of file
diff --git a/src/Tools/VSCode/src/dynamic_output.scala b/src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala
+++ b/src/Tools/VSCode/src/dynamic_output.scala
@@ -1,81 +1,81 @@
 /*  Title:      Tools/VSCode/src/dynamic_output.scala
     Author:     Makarius
 
 Dynamic output, depending on caret focus: messages, state etc.
 */
 
 package isabelle.vscode
 
 
 import isabelle._
 import isabelle.vscode.{Protocol, Server}
 
 
 object Dynamic_Output
 {
   sealed case class State(do_update: Boolean = true, output: List[XML.Tree] = Nil)
   {
     def handle_update(
       resources: VSCode_Resources, channel: Channel, restriction: Option[Set[Command]]): State =
     {
       val st1 =
         resources.get_caret() match {
           case None => copy(output = Nil)
           case Some(caret) =>
             val snapshot = caret.model.snapshot()
             if (do_update && !snapshot.is_outdated) {
               snapshot.current_command(caret.node_name, caret.offset) match {
                 case None => copy(output = Nil)
                 case Some(command) =>
                   copy(output =
-                    if (!restriction.isDefined || restriction.get.contains(command))
+                    if (restriction.isEmpty || restriction.get.contains(command))
                       Rendering.output_messages(snapshot.command_results(command))
                     else output)
               }
             }
             else this
         }
       if (st1.output != output) {
         channel.write(Protocol.Dynamic_Output(
           resources.output_pretty_message(Pretty.separate(st1.output))))
       }
       st1
     }
   }
 
   def apply(server: Server): Dynamic_Output = new Dynamic_Output(server)
 }
 
 
 class Dynamic_Output private(server: Server)
 {
   private val state = Synchronized(Dynamic_Output.State())
 
   private def handle_update(restriction: Option[Set[Command]])
   { state.change(_.handle_update(server.resources, server.channel, restriction)) }
 
 
   /* main */
 
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case changed: Session.Commands_Changed =>
         handle_update(if (changed.assignment) None else Some(changed.commands))
 
       case Session.Caret_Focus =>
         handle_update(None)
     }
 
   def init()
   {
     server.session.commands_changed += main
     server.session.caret_focus += main
     handle_update(None)
   }
 
   def exit()
   {
     server.session.commands_changed -= main
     server.session.caret_focus -= main
   }
 }
diff --git a/src/Tools/jEdit/src/completion_popup.scala b/src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala
+++ b/src/Tools/jEdit/src/completion_popup.scala
@@ -1,712 +1,712 @@
 /*  Title:      Tools/jEdit/src/completion_popup.scala
     Author:     Makarius
 
 Completion popup.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.{Color, Font, Point, BorderLayout, Dimension}
 import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
 import java.io.{File => JFile}
 import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
 import javax.swing.border.LineBorder
 import javax.swing.text.DefaultCaret
 
 import scala.swing.{ListView, ScrollPane}
 import scala.swing.event.MouseClicked
 
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection}
 import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
 import org.gjt.sp.util.StandardUtilities
 
 
 object Completion_Popup
 {
   /** items with HTML rendering **/
 
   private class Item(val item: Completion.Item)
   {
     private val html =
       item.description match {
         case a :: bs =>
           "<html><b>" + HTML.output(Symbol.print_newlines(a)) + "</b>" +
             HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "</html>"
         case Nil => ""
       }
     override def toString: String = html
   }
 
 
 
   /** jEdit text area **/
 
   object Text_Area
   {
     private val key = new Object
 
     def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
     {
       GUI_Thread.require {}
       text_area.getClientProperty(key) match {
         case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
         case _ => None
       }
     }
 
     def active_range(text_area: TextArea): Option[Text.Range] =
       apply(text_area) match {
         case Some(text_area_completion) => text_area_completion.active_range
         case None => None
       }
 
     def action(text_area: TextArea, word_only: Boolean): Boolean =
       apply(text_area) match {
         case Some(text_area_completion) =>
           if (text_area_completion.active_range.isDefined)
             text_area_completion.action(word_only = word_only)
           else
             text_area_completion.action(immediate = true, explicit = true, word_only = word_only)
           true
         case None => false
       }
 
     def exit(text_area: JEditTextArea)
     {
       GUI_Thread.require {}
       apply(text_area) match {
         case None =>
         case Some(text_area_completion) =>
           text_area_completion.deactivate()
           text_area.putClientProperty(key, null)
       }
     }
 
     def init(text_area: JEditTextArea): Completion_Popup.Text_Area =
     {
       exit(text_area)
       val text_area_completion = new Text_Area(text_area)
       text_area.putClientProperty(key, text_area_completion)
       text_area_completion.activate()
       text_area_completion
     }
 
     def dismissed(text_area: TextArea): Boolean =
     {
       GUI_Thread.require {}
       apply(text_area) match {
         case Some(text_area_completion) => text_area_completion.dismissed()
         case None => false
       }
     }
   }
 
   class Text_Area private(text_area: JEditTextArea)
   {
     // owned by GUI thread
     private var completion_popup: Option[Completion_Popup] = None
 
     def active_range: Option[Text.Range] =
       completion_popup match {
         case Some(completion) => completion.active_range
         case None => None
       }
 
 
     /* rendering */
 
     def rendering(rendering: JEdit_Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
     {
       active_range match {
         case Some(range) => range.try_restrict(line_range)
         case None =>
           val caret = text_area.getCaretPosition
           if (line_range.contains(caret)) {
             rendering.before_caret_range(caret).try_restrict(line_range) match {
               case Some(range) if !range.is_singularity =>
                 val range0 =
                   Completion.Result.merge(Completion.History.empty,
                     syntax_completion(Completion.History.empty, true, Some(rendering)),
                     rendering.path_completion(caret),
                     Document_Model.bibtex_completion(Completion.History.empty, rendering, caret))
                   .map(_.range)
                 rendering.semantic_completion(range0, range) match {
                   case None => range0
                   case Some(Text.Info(_, Completion.No_Completion)) => None
                   case Some(Text.Info(range1, _: Completion.Names)) => Some(range1)
                 }
               case _ => None
             }
           }
           else None
       }
     }.map(range => Text.Info(range, rendering.completion_color))
 
 
     /* syntax completion */
 
     def syntax_completion(
       history: Completion.History,
       explicit: Boolean,
       opt_rendering: Option[JEdit_Rendering]): Option[Completion.Result] =
     {
       val buffer = text_area.getBuffer
       val unicode = Isabelle_Encoding.is_active(buffer)
 
       Isabelle.buffer_syntax(buffer) match {
         case Some(syntax) =>
           val context =
             (for {
               rendering <- opt_rendering
               if PIDE.options.bool("jedit_completion_context")
               caret_range = rendering.before_caret_range(text_area.getCaretPosition)
               context <- rendering.language_context(caret_range)
             } yield context) getOrElse syntax.language_context
 
           val caret = text_area.getCaretPosition
           val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine)
           val line_start = line_range.start
           for {
             line_text <- JEdit_Lib.get_text(buffer, line_range)
             result <-
               syntax.complete(
                 history, unicode, explicit, line_start, line_text, caret - line_start, context)
           } yield result
 
         case None => None
       }
     }
 
 
     /* completion action: text area */
 
     private def insert(item: Completion.Item)
     {
       GUI_Thread.require {}
 
       val buffer = text_area.getBuffer
       val range = item.range
       if (buffer.isEditable) {
         JEdit_Lib.buffer_edit(buffer) {
           JEdit_Lib.get_text(buffer, range) match {
             case Some(text) if text == item.original =>
               text_area.getSelectionAtOffset(text_area.getCaretPosition) match {
 
                 /*rectangular selection as "tall caret"*/
                 case selection : Selection.Rect
                 if selection.getStart(buffer, text_area.getCaretLine) == range.stop =>
                   text_area.moveCaretPosition(range.stop)
                   (0 until Character.codePointCount(item.original, 0, item.original.length))
                     .foreach(_ => text_area.backspace())
                   text_area.setSelectedText(selection, item.replacement)
                   text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
 
                 /*other selections: rectangular, multiple range, ...*/
                 case selection
                 if selection != null &&
                     selection.getStart(buffer, text_area.getCaretLine) == range.start &&
                     selection.getEnd(buffer, text_area.getCaretLine) == range.stop =>
                   text_area.moveCaretPosition(range.stop + item.move)
                   text_area.getSelection.foreach(text_area.setSelectedText(_, item.replacement))
 
                 /*no selection*/
                 case _ =>
                   buffer.remove(range.start, range.length)
                   buffer.insert(range.start, item.replacement)
                   text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
                   Isabelle.indent_input(text_area)
               }
             case _ =>
           }
         }
       }
     }
 
     def action(
       immediate: Boolean = false,
       explicit: Boolean = false,
       delayed: Boolean = false,
       word_only: Boolean = false): Boolean =
     {
       val view = text_area.getView
       val layered = view.getLayeredPane
       val buffer = text_area.getBuffer
       val painter = text_area.getPainter
 
       val history = PIDE.plugin.completion_history.value
       val unicode = Isabelle_Encoding.is_active(buffer)
 
       def open_popup(result: Completion.Result)
       {
         val font =
           painter.getFont.deriveFont(
             Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
 
         val range = result.range
 
         val loc1 = text_area.offsetToXY(range.start)
         if (loc1 != null) {
           val loc2 =
             SwingUtilities.convertPoint(painter,
               loc1.x, loc1.y + painter.getLineHeight, layered)
 
           val items = result.items.map(new Item(_))
           val completion =
             new Completion_Popup(Some(range), layered, loc2, font, items)
             {
               override def complete(item: Completion.Item) {
                 PIDE.plugin.completion_history.update(item)
                 insert(item)
               }
               override def propagate(evt: KeyEvent) {
                 if (view.getKeyEventInterceptor == null)
                   JEdit_Lib.propagate_key(view, evt)
                 else if (view.getKeyEventInterceptor == inner_key_listener) {
                   try {
                     view.setKeyEventInterceptor(null)
                     JEdit_Lib.propagate_key(view, evt)
                   }
                   finally {
                     if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener)
                   }
                 }
                 if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
               }
               override def shutdown(focus: Boolean) {
                 if (view.getKeyEventInterceptor == inner_key_listener)
                   view.setKeyEventInterceptor(null)
                 if (focus) text_area.requestFocus
                 JEdit_Lib.invalidate_range(text_area, range)
               }
             }
           dismissed()
           completion_popup = Some(completion)
           view.setKeyEventInterceptor(completion.inner_key_listener)
           JEdit_Lib.invalidate_range(text_area, range)
           Pretty_Tooltip.dismissed_all()
           completion.show_popup(false)
         }
       }
 
       if (buffer.isEditable) {
         val caret = text_area.getCaretPosition
         val opt_rendering = Document_View.get(text_area).map(_.get_rendering())
         val result0 = syntax_completion(history, explicit, opt_rendering)
         val (no_completion, semantic_completion) =
         {
           opt_rendering match {
             case Some(rendering) =>
               rendering.semantic_completion_result(history, unicode, result0.map(_.range),
                 rendering.before_caret_range(caret))
             case None => (false, None)
           }
         }
         if (no_completion) false
         else {
           val result =
           {
             val result1 =
               if (word_only) None
               else Completion.Result.merge(history, semantic_completion, result0)
             opt_rendering match {
               case None => result1
               case Some(rendering) =>
                 Completion.Result.merge(history,
                   result1,
                   JEdit_Spell_Checker.completion(rendering, explicit, caret),
                   rendering.path_completion(caret),
                   Document_Model.bibtex_completion(history, rendering, caret))
             }
           }
           result match {
             case Some(result) =>
               result.items match {
                 case List(item) if result.unique && item.immediate && immediate =>
                   insert(item)
                   true
                 case _ :: _ if !delayed =>
                   open_popup(result)
                   false
                 case _ => false
               }
             case None => false
           }
         }
       }
       else false
     }
 
 
     /* input key events */
 
     def input(evt: KeyEvent)
     {
       GUI_Thread.require {}
 
       if (!evt.isConsumed) {
         val special = JEdit_Lib.special_key(evt)
 
         if (PIDE.options.bool("jedit_completion")) {
           dismissed()
           if (evt.getKeyChar != '\b') {
             val immediate = PIDE.options.bool("jedit_completion_immediate")
             if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
               input_delay.revoke()
               action(immediate = immediate)
             }
             else {
               if (!special && action(immediate = immediate, delayed = true))
                 input_delay.revoke()
               else
                 input_delay.invoke()
             }
           }
         }
 
         val selection = text_area.getSelection()
-        if (!special && (selection == null || selection.length == 0))
+        if (!special && (selection == null || selection.isEmpty))
           Isabelle.indent_input(text_area)
       }
     }
 
     private val input_delay =
       GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
         action()
       }
 
 
     /* dismiss popup */
 
     def dismissed(): Boolean =
     {
       GUI_Thread.require {}
 
       completion_popup match {
         case Some(completion) =>
           completion.hide_popup()
           completion_popup = None
           true
         case None =>
           false
       }
     }
 
 
     /* activation */
 
     private val outer_key_listener =
       JEdit_Lib.key_listener(key_typed = input _)
 
     private def activate()
     {
       text_area.addKeyListener(outer_key_listener)
     }
 
     private def deactivate()
     {
       dismissed()
       text_area.removeKeyListener(outer_key_listener)
     }
   }
 
 
 
   /** history text field **/
 
   class History_Text_Field(
     name: String = null,
     instant_popups: Boolean = false,
     enter_adds_to_history: Boolean = true,
     syntax: Outer_Syntax = Outer_Syntax.empty) extends
     HistoryTextField(name, instant_popups, enter_adds_to_history)
   {
     text_field =>
 
     // see https://forums.oracle.com/thread/1361677
     if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
 
     // owned by GUI thread
     private var completion_popup: Option[Completion_Popup] = None
 
 
     /* dismiss */
 
     private def dismissed(): Boolean =
     {
       completion_popup match {
         case Some(completion) =>
           completion.hide_popup()
           completion_popup = None
           true
         case None =>
           false
       }
     }
 
 
     /* insert */
 
     private def insert(item: Completion.Item)
     {
       GUI_Thread.require {}
 
       val range = item.range
       if (text_field.isEditable) {
         val content = text_field.getText
         range.try_substring(content) match {
           case Some(text) if text == item.original =>
             text_field.setText(
               content.substring(0, range.start) +
               item.replacement +
               content.substring(range.stop))
             text_field.getCaret.setDot(range.start + item.replacement.length + item.move)
           case _ =>
         }
       }
     }
 
 
     /* completion action: text field */
 
     def action()
     {
       GUI.layered_pane(text_field) match {
         case Some(layered) if text_field.isEditable =>
           val history = PIDE.plugin.completion_history.value
 
           val caret = text_field.getCaret.getDot
           val text = text_field.getText
 
           val context = syntax.language_context
 
           syntax.complete(history, true, false, 0, text, caret, context) match {
             case Some(result) =>
               val fm = text_field.getFontMetrics(text_field.getFont)
               val loc =
                 SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
 
               val items = result.items.map(new Item(_))
               val completion =
                 new Completion_Popup(None, layered, loc, text_field.getFont, items)
                 {
                   override def complete(item: Completion.Item) {
                     PIDE.plugin.completion_history.update(item)
                     insert(item)
                   }
                   override def propagate(evt: KeyEvent) {
                     if (!evt.isConsumed) text_field.processKeyEvent(evt)
                   }
                   override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
                 }
               dismissed()
               completion_popup = Some(completion)
               completion.show_popup(true)
 
             case None =>
           }
         case _ =>
       }
     }
 
 
     /* process key event */
 
     private def process(evt: KeyEvent)
     {
       if (PIDE.options.bool("jedit_completion")) {
         dismissed()
         if (evt.getKeyChar != '\b') {
           val special = JEdit_Lib.special_key(evt)
           if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
             process_delay.revoke()
             action()
           }
           else process_delay.invoke()
         }
       }
     }
 
     private val process_delay =
       GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
         action()
       }
 
     override def processKeyEvent(evt0: KeyEvent)
     {
       val evt = KeyEventWorkaround.processKeyEvent(evt0)
       if (evt != null) {
         evt.getID match {
           case KeyEvent.KEY_PRESSED =>
             val key_code = evt.getKeyCode
             if (key_code == KeyEvent.VK_ESCAPE) {
               if (dismissed()) evt.consume
             }
           case KeyEvent.KEY_TYPED =>
             super.processKeyEvent(evt)
             process(evt)
             evt.consume
           case _ =>
         }
         if (!evt.isConsumed) super.processKeyEvent(evt)
       }
     }
   }
 }
 
 
 class Completion_Popup private(
   opt_range: Option[Text.Range],
   layered: JLayeredPane,
   location: Point,
   font: Font,
   items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
 {
   completion =>
 
   GUI_Thread.require {}
 
   require(items.nonEmpty)
   val multi = items.length > 1
 
 
   /* actions */
 
   def complete(item: Completion.Item) { }
   def propagate(evt: KeyEvent) { }
   def shutdown(focus: Boolean) { }
 
 
   /* list view */
 
   private val list_view = new ListView(items)
   list_view.font = font
   list_view.selection.intervalMode = ListView.IntervalMode.Single
   list_view.peer.setFocusTraversalKeysEnabled(false)
   list_view.peer.setVisibleRowCount(items.length min 8)
   list_view.peer.setSelectedIndex(0)
 
   for (cond <-
     List(JComponent.WHEN_FOCUSED,
       JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT,
       JComponent.WHEN_IN_FOCUSED_WINDOW)) list_view.peer.setInputMap(cond, null)
 
   private def complete_selected(): Boolean =
   {
     list_view.selection.items.toList match {
       case item :: _ => complete(item.item); true
       case _ => false
     }
   }
 
   private def move_items(n: Int)
   {
     val i = list_view.peer.getSelectedIndex
     val j = ((i + n) min (items.length - 1)) max 0
     if (i != j) {
       list_view.peer.setSelectedIndex(j)
       list_view.peer.ensureIndexIsVisible(j)
     }
   }
 
   private def move_pages(n: Int)
   {
     val page_size = list_view.peer.getVisibleRowCount - 1
     move_items(page_size * n)
   }
 
 
   /* event handling */
 
   val inner_key_listener =
     JEdit_Lib.key_listener(
       key_pressed = (e: KeyEvent) =>
         {
           if (!e.isConsumed) {
             e.getKeyCode match {
               case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
                 if (complete_selected()) e.consume
                 hide_popup()
               case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") =>
                 if (complete_selected()) e.consume
                 hide_popup()
               case KeyEvent.VK_ESCAPE =>
                 hide_popup()
                 e.consume
               case KeyEvent.VK_UP | KeyEvent.VK_KP_UP if multi =>
                 move_items(-1)
                 e.consume
               case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN if multi =>
                 move_items(1)
                 e.consume
               case KeyEvent.VK_PAGE_UP if multi =>
                 move_pages(-1)
                 e.consume
               case KeyEvent.VK_PAGE_DOWN if multi =>
                 move_pages(1)
                 e.consume
               case _ =>
                 if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
                   hide_popup()
             }
           }
           propagate(e)
         },
       key_typed = propagate _
     )
 
   list_view.peer.addKeyListener(inner_key_listener)
 
   list_view.peer.addMouseListener(new MouseAdapter {
     override def mouseClicked(e: MouseEvent) {
       if (complete_selected()) e.consume
       hide_popup()
     }
   })
 
   list_view.peer.addFocusListener(new FocusAdapter {
     override def focusLost(e: FocusEvent) { hide_popup() }
   })
 
 
   /* main content */
 
   override def getFocusTraversalKeysEnabled = false
   completion.setBorder(new LineBorder(Color.BLACK))
   completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
 
 
   /* popup */
 
   def active_range: Option[Text.Range] =
     if (isDisplayable) opt_range else None
 
   private val popup =
   {
     val screen = JEdit_Lib.screen_location(layered, location)
     val size =
     {
       val geometry = JEdit_Lib.window_geometry(completion, completion)
       val bounds = JEdit_Rendering.popup_bounds
       val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth
       val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight
       new Dimension(w, h)
     }
     new Popup(layered, completion, screen.relative(layered, size), size)
   }
 
   private def show_popup(focus: Boolean)
   {
     popup.show
     if (focus) list_view.requestFocus
   }
 
   private def hide_popup()
   {
     shutdown(list_view.peer.isFocusOwner)
     popup.hide
   }
 }