diff --git a/src/Pure/General/pretty.scala b/src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala
+++ b/src/Pure/General/pretty.scala
@@ -1,189 +1,189 @@
 /*  Title:      Pure/General/pretty.scala
     Author:     Makarius
 
 Generic pretty printing module.
 */
 
 package isabelle
 
 import scala.annotation.tailrec
 
 
 object Pretty
 {
   /* XML constructors */
 
   val space: XML.Body = List(XML.Text(Symbol.space))
   def spaces(n: Int): XML.Body =
     if (n == 0) Nil
     else if (n == 1) space
     else List(XML.Text(Symbol.spaces(n)))
 
   def block(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
     XML.Elem(Markup.Block(consistent, indent), body)
   def block(indent: Int, body: XML.Body): XML.Tree = block(false, indent, body)
   def block(body: XML.Body): XML.Tree = block(2, body)
 
   def brk(width: Int, indent: Int = 0): XML.Tree =
     XML.Elem(Markup.Break(width, indent), spaces(width))
 
   val fbrk: XML.Tree = XML.newline
   def fbreaks(ts: List[XML.Tree]): XML.Body = Library.separate(fbrk, ts)
 
   val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
   def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
 
 
   /* text metric -- standardized to width of space */
 
   abstract class Metric
   {
     val unit: Double
     def apply(s: String): Double
   }
 
   object Default_Metric extends Metric
   {
     val unit = 1.0
     def apply(s: String): Double = s.length.toDouble
   }
 
 
   /* markup trees with physical blocks and breaks */
 
   private def force_nat(i: Int): Int = i max 0
 
   private sealed abstract class Tree { def length: Double }
   private case class Block(
     markup: Option[(Markup, Option[XML.Body])],
     consistent: Boolean, indent: Int, body: List[Tree], length: Double) extends Tree
   private case class Break(force: Boolean, width: Int, indent: Int) extends Tree
   { def length: Double = width.toDouble }
   private case class Str(string: String, length: Double) extends Tree
 
   private val FBreak = Break(true, 1, 0)
 
   private def make_block(
       markup: Option[(Markup, Option[XML.Body])],
       consistent: Boolean,
       indent: Int,
       body: List[Tree]): Tree =
   {
     val indent1 = force_nat(indent)
 
     @tailrec def body_length(prts: List[Tree], len: Double): Double =
     {
       val (line, rest) =
         Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
       val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
-      rest match {
+      (rest: @unchecked) match {
         case Break(true, _, ind) :: rest1 =>
           body_length(Break(false, indent1 + ind, 0) :: rest1, len1)
         case Nil => len1
       }
     }
     Block(markup, consistent, indent1, body, body_length(body, 0.0))
   }
 
 
   /* formatted output */
 
   private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
   {
     def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
     def string(s: String, len: Double): Text =
       copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
     def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
     def content: XML.Body = tx.reverse
   }
 
   private def break_dist(trees: List[Tree], after: Double): Double =
     trees match {
       case (_: Break) :: _ => 0.0
       case t :: ts => t.length + break_dist(ts, after)
       case Nil => after
     }
 
   private def force_break(tree: Tree): Tree =
     tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
   private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break)
 
   private def force_next(trees: List[Tree]): List[Tree] =
     trees match {
       case Nil => Nil
       case (t: Break) :: ts => force_break(t) :: ts
       case t :: ts => t :: force_next(ts)
     }
 
   val default_margin: Double = 76.0
   val default_breakgain: Double = default_margin / 20
 
   def formatted(input: XML.Body,
     margin: Double = default_margin,
     breakgain: Double = default_breakgain,
     metric: Metric = Default_Metric): XML.Body =
   {
     val emergencypos = (margin / 2).round.toInt
 
     def make_tree(inp: XML.Body): List[Tree] =
       inp flatMap {
         case XML.Wrapped_Elem(markup, body1, body2) =>
           List(make_block(Some(markup, Some(body1)), false, 0, make_tree(body2)))
         case XML.Elem(markup, body) =>
           markup match {
             case Markup.Block(consistent, indent) =>
               List(make_block(None, consistent, indent, make_tree(body)))
             case Markup.Break(width, indent) =>
               List(Break(false, force_nat(width), force_nat(indent)))
             case Markup(Markup.ITEM, _) =>
               List(make_block(None, false, 2,
                 make_tree(XML.elem(Markup.BULLET, space) :: space ::: body)))
             case _ =>
               List(make_block(Some((markup, None)), false, 0, make_tree(body)))
           }
         case XML.Text(text) =>
           Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
       }
 
     def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text =
       trees match {
         case Nil => text
 
         case Block(markup, consistent, indent, body, blen) :: ts =>
           val pos1 = (text.pos + indent).ceil.toInt
           val pos2 = pos1 % emergencypos
           val blockin1 = if (pos1 < emergencypos) pos1 else pos2
           val d = break_dist(ts, after)
           val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body
           val btext =
             markup match {
               case None => format(body1, blockin1, d, text)
               case Some((m, markup_body)) =>
                 val btext0 = format(body1, blockin1, d, text.copy(tx = Nil))
                 val elem =
                   markup_body match {
                     case None => XML.Elem(m, btext0.content)
                     case Some(b) => XML.Wrapped_Elem(m, b, btext0.content)
                   }
                 btext0.copy(tx = elem :: text.tx)
             }
           val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
           format(ts1, blockin, after, btext)
 
         case Break(force, wd, ind) :: ts =>
           if (!force &&
               text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain)))
             format(ts, blockin, after, text.blanks(wd))
           else format(ts, blockin, after, text.newline.blanks(blockin + ind))
 
         case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len))
       }
     format(make_tree(input), 0, 0.0, Text()).content
   }
 
   def string_of(input: XML.Body,
       margin: Double = default_margin,
       breakgain: Double = default_breakgain,
       metric: Metric = Default_Metric): String =
     XML.content(formatted(input, margin = margin, breakgain = breakgain, metric = metric))
 }
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,501 +1,507 @@
 /*  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 scala.util.matching.Regex
 
 import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
-  OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS}
+  OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS,
+  JSchException}
 
 
 object SSH
 {
   /* target machine: user@host syntax */
 
   object Target
   {
     val User_Host: Regex = "^([^@]+)@(.+)$".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 port_suffix(port: Int): String =
     if (port == default_port) "" else ":" + port
 
   def user_prefix(user: String): String =
     proper_string(user) match {
       case None => ""
       case Some(name) => name + "@"
     }
 
   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))
+    for (identity_file <- identity_files if identity_file.is_file) {
+      try { jsch.addIdentity(File.platform_path(identity_file)) }
+      catch {
+        case exn: JSchException =>
+          error("Error in ssh identity file " + identity_file + ": " + exn.getMessage)
+      }
+    }
 
     new Context(options, jsch)
   }
 
   def open_session(options: Options,
       host: String, user: String = "", port: Int = 0, actual_host: String = "",
       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, actual_host = actual_host,
       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)
 
     private def connect_session(host: String, user: String = "", port: Int = 0,
       host_key_permissive: Boolean = false,
       nominal_host: String = "",
       nominal_user: String = "",
       on_close: () => Unit = () => ()): Session =
     {
       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 (nominal_host != "") session.setHostKeyAlias(nominal_host)
 
       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,
         proper_string(nominal_host) getOrElse host,
         proper_string(nominal_user) getOrElse user)
     }
 
     def open_session(
       host: String, user: String = "", port: Int = 0, actual_host: String = "",
       proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
       permissive: Boolean = false): Session =
     {
       val connect_host = proper_string(actual_host) getOrElse host
       if (proxy_host == "") connect_session(host = connect_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 = connect_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,
             nominal_host = host, nominal_user = user, 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) exec_wait_delay.sleep
         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 exec_wait_delay.sleep
         }
 
         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,
     val nominal_host: String,
     val nominal_user: String) extends System with AutoCloseable
   {
     def update_options(new_options: Options): Session =
       new Session(new_options, session, on_close, nominal_host, nominal_user)
 
     def host: String = if (session.getHost == null) "" else session.getHost
 
     override def hg_url: String =
       "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
 
     override def toString: String =
       user_prefix(session.getUserName) + host + port_suffix(session.getPort) +
       (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 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/timing.scala b/src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala
+++ b/src/Pure/General/timing.scala
@@ -1,76 +1,76 @@
 /*  Title:      Pure/General/timing.scala
     Author:     Makarius
 
 Support for time measurement.
 */
 
 package isabelle
 
 
 import java.util.Locale
 
 
 object Timing
 {
   val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)
 
   def timeit[A](
     message: String = "",
     enabled: Boolean = true,
     output: String => Unit = Output.warning(_))(e: => A): A =
   {
     if (enabled) {
       val start = Time.now()
       val result = Exn.capture(e)
       val stop = Time.now()
 
       val timing = stop - start
       if (timing.is_relevant) {
         output(
           (if (message == null || message == "") "" else message + ": ") +
             timing.message + " elapsed time")
       }
 
       Exn.release(result)
     }
     else e
   }
 }
 
 sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
 {
   def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
   def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
 
   def resources: Time = cpu + gc
 
   def factor: Option[Double] =
   {
     val t1 = elapsed.seconds
     val t2 = resources.seconds
     if (t1 >= 3.0 && t2 >= 3.0) Some(t2 / t1) else None
   }
 
   def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)
 
   def message: String =
     elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
 
   def message_resources: String =
   {
     val factor_text =
       factor match {
-        case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f))
+        case Some(f) => String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f))
         case None => ""
       }
     if (resources.seconds >= 3.0)
       elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text
     else
       elapsed.message_hms + " elapsed time" + factor_text
   }
 
   override def toString: String = message
 
   def json: JSON.Object.T =
     JSON.Object("elapsed" -> elapsed.seconds, "cpu" -> cpu.seconds, "gc" -> gc.seconds)
 }
diff --git a/src/Pure/Thy/latex.scala b/src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala
+++ b/src/Pure/Thy/latex.scala
@@ -1,178 +1,179 @@
 /*  Title:      Pure/Thy/latex.scala
     Author:     Makarius
 
 Support for LaTeX.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 import scala.annotation.tailrec
 import scala.util.matching.Regex
 
 
 object Latex
 {
   /** latex errors **/
 
   def latex_errors(dir: Path, root_name: String): List[String] =
   {
     val root_log_path = dir + Path.explode(root_name).ext("log")
     if (root_log_path.is_file) {
       for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
       yield "Latex error" + Position.here(pos) + ":\n" + Library.prefix_lines("  ", msg)
     }
     else Nil
   }
 
 
   /* generated .tex file */
 
   private val File_Pattern = """^%:%file=(.+)%:%$""".r
   private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r
 
   def read_tex_file(tex_file: Path): Tex_File =
   {
     val positions =
       Line.logical_lines(File.read(tex_file)).reverse.
         takeWhile(_ != "\\endinput").reverse
 
     val source_file =
       positions match {
         case File_Pattern(file) :: _ => Some(file)
         case _ => None
       }
 
     val source_lines =
       if (source_file.isEmpty) Nil
       else
         positions.flatMap(line =>
           line match {
             case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line)
             case _ => None
           })
 
     new Tex_File(tex_file, source_file, source_lines)
   }
 
   final class Tex_File private[Latex](
     tex_file: Path, source_file: Option[String], source_lines: List[(Int, Int)])
   {
     override def toString: String = tex_file.toString
 
     def source_position(l: Int): Option[Position.T] =
       source_file match {
         case None => None
         case Some(file) =>
           val source_line =
             (0 /: source_lines.iterator.takeWhile({ case (m, _) => m <= l }))(
               { case (_, (_, n)) => n })
           if (source_line == 0) None else Some(Position.Line_File(source_line, file))
       }
 
     def position(line: Int): Position.T =
       source_position(line) getOrElse Position.Line_File(line, tex_file.implode)
   }
 
 
   /* latex log */
 
   def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] =
   {
     val seen_files = Synchronized(Map.empty[JFile, Tex_File])
 
     def check_tex_file(path: Path): Option[Tex_File] =
       seen_files.change_result(seen =>
         seen.get(path.file) match {
           case None =>
             if (path.is_file) {
               val tex_file = read_tex_file(path)
               (Some(tex_file), seen + (path.file -> tex_file))
             }
             else (None, seen)
           case some => (some, seen)
         })
 
     def tex_file_position(path: Path, line: Int): Position.T =
       check_tex_file(path) match {
         case Some(tex_file) => tex_file.position(line)
         case None => Position.Line_File(line, path.implode)
       }
 
     object File_Line_Error
     {
       val Pattern: Regex = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
       def unapply(line: String): Option[(Path, Int, String)] =
         line match {
           case Pattern(file, Value.Int(line), message) =>
             val path = File.standard_path(file)
             if (Path.is_wellformed(path)) {
               val file = (dir + Path.explode(path)).canonical
               val msg = Library.perhaps_unprefix("LaTeX Error: ", message)
               if (file.is_file) Some((file, line, msg)) else None
             }
             else None
           case _ => None
         }
     }
 
     val Line_Error = """^l\.\d+ (.*)$""".r
     val More_Error =
       List(
         "<argument>",
         "<template>",
         "<recently read>",
         "<to be read again>",
         "<inserted text>",
         "<output>",
         "<everypar>",
         "<everymath>",
         "<everydisplay>",
         "<everyhbox>",
         "<everyvbox>",
         "<everyjob>",
         "<everycr>",
         "<mark>",
         "<everyeof>",
         "<write>").mkString("^(?:", "|", ") (.*)$").r
 
     val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r
 
     val error_ignore =
       Set(
         "See the LaTeX manual or LaTeX Companion for explanation.",
         "Type  H <return>  for immediate help.")
 
     def error_suffix1(lines: List[String]): Option[String] =
     {
-      val lines1 = lines.take(20).takeWhile({ case File_Line_Error(_) => false case _ => true })
+      val lines1 =
+        lines.take(20).takeWhile({ case File_Line_Error((_, _, _)) => false case _ => true })
       lines1.zipWithIndex.collectFirst({
         case (Line_Error(msg), i) =>
           cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) })
     }
     def error_suffix2(lines: List[String]): Option[String] =
       lines match {
         case More_Error(msg) :: _ => Some(msg)
         case _ => None
       }
 
     @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
       : List[(String, Position.T)] =
     {
       lines match {
         case File_Line_Error((file, line, msg1)) :: rest1 =>
           val pos = tex_file_position(file, line)
           val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse ""
           filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
         case Bad_File(msg) :: rest =>
           filter(rest, (msg, Position.none) :: result)
         case _ :: rest => filter(rest, result)
         case Nil => result.reverse
       }
     }
 
     filter(Line.logical_lines(root_log), Nil)
   }
 }
diff --git a/src/Pure/term.scala b/src/Pure/term.scala
--- a/src/Pure/term.scala
+++ b/src/Pure/term.scala
@@ -1,228 +1,228 @@
 /*  Title:      Pure/term.scala
     Author:     Makarius
 
 Lambda terms, types, sorts.
 
 Note: Isabelle/ML is the primary environment for logical operations.
 */
 
 package isabelle
 
 
 object Term
 {
   /* types and terms */
 
   sealed case class Indexname(name: String, index: Int = 0)
   {
     override def toString: String =
       if (index == -1) name
       else {
         val dot =
           Symbol.explode(name).reverse match {
             case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false
             case c :: _ => Symbol.is_digit(c)
             case _ => true
           }
         if (dot) "?" + name + "." + index
         else if (index != 0) "?" + name + index
         else "?" + name
       }
   }
 
   type Class = String
   type Sort = List[Class]
 
   sealed abstract class Typ
   case class Type(name: String, args: List[Typ] = Nil) extends Typ
   {
     override def toString: String =
       if (this == dummyT) "_"
       else "Type(" + name + (if (args.isEmpty) "" else "," + args) + ")"
   }
   case class TFree(name: String, sort: Sort = Nil) extends Typ
   {
     override def toString: String =
       "TFree(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
   }
   case class TVar(name: Indexname, sort: Sort = Nil) extends Typ
   {
     override def toString: String =
       "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
   }
   val dummyT: Type = Type("dummy")
 
   sealed abstract class Term
   {
     def head: Term =
       this match {
         case App(fun, _) => fun.head
         case _ => this
       }
   }
   case class Const(name: String, typargs: List[Typ] = Nil) extends Term
   {
     override def toString: String =
       if (this == dummy) "_"
       else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")"
   }
   case class Free(name: String, typ: Typ = dummyT) extends Term
   {
     override def toString: String =
       "Free(" + name + (if (typ == dummyT) "" else "," + typ) + ")"
   }
   case class Var(name: Indexname, typ: Typ = dummyT) extends Term
   {
     override def toString: String =
       "Var(" + name + (if (typ == dummyT) "" else "," + typ) + ")"
   }
   case class Bound(index: Int) extends Term
   case class Abs(name: String, typ: Typ, body: Term) extends Term
   case class App(fun: Term, arg: Term) extends Term
   {
     override def toString: String =
       this match {
         case OFCLASS(ty, c) => "OFCLASS(" + ty + "," + c + ")"
         case _ => "App(" + fun + "," + arg + ")"
       }
   }
 
   def dummy_pattern(ty: Typ): Term = Const("Pure.dummy_pattern", List(ty))
   val dummy: Term = dummy_pattern(dummyT)
 
   sealed abstract class Proof
   case object MinProof extends Proof
   case class PBound(index: Int) extends Proof
   case class Abst(name: String, typ: Typ, body: Proof) extends Proof
   case class AbsP(name: String, hyp: Term, body: Proof) extends Proof
   case class Appt(fun: Proof, arg: Term) extends Proof
   case class AppP(fun: Proof, arg: Proof) extends Proof
   case class Hyp(hyp: Term) extends Proof
   case class PAxm(name: String, types: List[Typ]) extends Proof
   case class PClass(typ: Typ, cls: Class) extends Proof
   case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
   case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof
 
 
   /* type classes within the logic */
 
   object Class_Const
   {
     val suffix = "_class"
     def apply(c: Class): String = c + suffix
     def unapply(s: String): Option[Class] =
       if (s.endsWith(suffix)) Some(s.substring(0, s.length - suffix.length)) else None
   }
 
   object OFCLASS
   {
     def apply(ty: Typ, s: Sort): List[Term] = s.map(c => apply(ty, c))
 
     def apply(ty: Typ, c: Class): Term =
       App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty)))
 
     def unapply(t: Term): Option[(Typ, String)] =
       t match {
         case App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty1)))
         if ty == ty1 => Some((ty, c))
         case _ => None
       }
   }
 
 
 
   /** cache **/
 
   def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
     new Cache(initial_size, max_string)
 
   class Cache private[Term](initial_size: Int, max_string: Int)
     extends isabelle.Cache(initial_size, max_string)
   {
     protected def cache_indexname(x: Indexname): Indexname =
       lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
 
     protected def cache_sort(x: Sort): Sort =
       if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string))
 
     protected def cache_typ(x: Typ): Typ =
     {
       if (x == dummyT) dummyT
       else
         lookup(x) match {
           case Some(y) => y
           case None =>
             x match {
               case Type(name, args) => store(Type(cache_string(name), cache_typs(args)))
               case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
               case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
             }
         }
     }
 
     protected def cache_typs(x: List[Typ]): List[Typ] =
     {
       if (x.isEmpty) Nil
       else {
         lookup(x) match {
           case Some(y) => y
           case None => store(x.map(cache_typ))
         }
       }
     }
 
     protected def cache_term(x: Term): Term =
     {
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
             case Const(name, typargs) => store(Const(cache_string(name), cache_typs(typargs)))
             case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
             case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
             case Bound(_) => store(x)
             case Abs(name, typ, body) =>
               store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
             case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
           }
       }
     }
 
     protected def cache_proof(x: Proof): Proof =
     {
       if (x == MinProof) MinProof
       else {
         lookup(x) match {
           case Some(y) => y
           case None =>
-            x match {
+            (x: @unchecked) match {
               case PBound(_) => store(x)
               case Abst(name, typ, body) =>
                 store(Abst(cache_string(name), cache_typ(typ), cache_proof(body)))
               case AbsP(name, hyp, body) =>
                 store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body)))
               case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg)))
               case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg)))
               case Hyp(hyp) => store(Hyp(cache_term(hyp)))
               case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types)))
               case PClass(typ, cls) => store(PClass(cache_typ(typ), cache_string(cls)))
               case Oracle(name, prop, types) =>
                 store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
               case PThm(serial, theory_name, name, types) =>
                 store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
             }
         }
       }
     }
 
     // main methods
     def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
     def sort(x: Sort): Sort = synchronized { cache_sort(x) }
     def typ(x: Typ): Typ = synchronized { cache_typ(x) }
     def term(x: Term): Term = synchronized { cache_term(x) }
     def proof(x: Proof): Proof = synchronized { cache_proof(x) }
 
     def position(x: Position.T): Position.T =
       synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
   }
 }
diff --git a/src/Tools/jEdit/src/fold_handling.scala b/src/Tools/jEdit/src/fold_handling.scala
--- a/src/Tools/jEdit/src/fold_handling.scala
+++ b/src/Tools/jEdit/src/fold_handling.scala
@@ -1,81 +1,80 @@
 /*  Title:      Tools/jEdit/src/fold_handling.scala
     Author:     Makarius
 
 Handling of folds within the text structure.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import javax.swing.text.Segment
 
-import scala.collection.convert.WrapAsJava
+import scala.collection.JavaConverters
 
 import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
 
 
 object Fold_Handling
 {
   /* input: dynamic line context  */
 
   class Fold_Handler extends FoldHandler("isabelle")
   {
     override def equals(other: Any): Boolean =
       other match {
         case that: Fold_Handler => true
         case _ => false
       }
 
     override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
       Token_Markup.Line_Context.after(buffer, line).structure.depth max 0
 
     override def getPrecedingFoldLevels(
       buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
     {
       val structure = Token_Markup.Line_Context.after(buffer, line).structure
       val result =
         if (line > 0 && structure.command)
           Range.inclusive(line - 1, 0, -1).iterator.
             map(i => Token_Markup.Line_Context.after(buffer, i).structure).
             takeWhile(_.improper).map(_ => structure.depth max 0).toList
         else Nil
 
       if (result.isEmpty) null
-      else WrapAsJava.seqAsJavaList(result.map(Integer.valueOf))
+      else JavaConverters.seqAsJavaList(result.map(Integer.valueOf))
     }
   }
 
 
   /* output: static document rendering */
 
   class Document_Fold_Handler(private val rendering: JEdit_Rendering)
     extends FoldHandler("isabelle-document")
   {
     override def equals(other: Any): Boolean =
       other match {
         case that: Document_Fold_Handler => this.rendering == that.rendering
         case _ => false
       }
 
     override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
     {
       def depth(i: Text.Offset): Int =
         if (i < 0) 0
         else {
           rendering.fold_depth(Text.Range(i, i + 1)) match {
             case Text.Info(_, d) :: _ => d
             case _ => 0
           }
         }
 
       if (line <= 0) 0
       else {
         val range = JEdit_Lib.line_range(buffer, line - 1)
         buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1)
       }
     }
   }
 }
-
diff --git a/src/Tools/jEdit/src/keymap_merge.scala b/src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala
+++ b/src/Tools/jEdit/src/keymap_merge.scala
@@ -1,259 +1,259 @@
 /*  Title:      Tools/jEdit/src/keymap_merge.scala
     Author:     Makarius
 
 Merge of Isabelle shortcuts vs. jEdit keymap.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
-import java.lang.Class
 import java.awt.{Color, Dimension, BorderLayout}
 import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
 import javax.swing.table.AbstractTableModel
 
 import scala.collection.JavaConverters
 
-import org.gjt.sp.jedit.{jEdit, View, GUIUtilities}
+import org.gjt.sp.jedit.{jEdit, View}
+import org.gjt.sp.util.GenericGUIUtilities
 import org.jedit.keymap.{KeymapManager, Keymap}
 
 
 object Keymap_Merge
 {
   /** shortcuts **/
 
   private def is_shortcut(property: String): Boolean =
     (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) &&
     !property.startsWith("options.shortcuts.")
 
   class Shortcut(val property: String, val binding: String)
   {
     override def toString: String = property + "=" + binding
 
     def primary: Boolean = property.endsWith(".shortcut")
 
     val action: String =
       Library.try_unsuffix(".shortcut", property) orElse
       Library.try_unsuffix(".shortcut2", property) getOrElse
       error("Bad shortcut property: " + quote(property))
 
     val label: String =
-      GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", ""))
+      GenericGUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", ""))
 
 
     /* ignore wrt. keymap */
 
     private def prop_ignore: String = property + ".ignore"
 
     def ignored_keymaps(): List[String] =
       space_explode(',', jEdit.getProperty(prop_ignore, ""))
 
     def is_ignored(keymap_name: String): Boolean =
       ignored_keymaps().contains(keymap_name)
 
     def ignore(keymap_name: String): Unit =
       jEdit.setProperty(prop_ignore,
         Library.insert(keymap_name)(ignored_keymaps()).sorted.mkString(","))
 
     def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding)
     def reset(keymap: Keymap): Unit = keymap.setShortcut(property, null)
   }
 
 
   /* content wrt. keymap */
 
   def convert_properties(props: java.util.Properties): List[Shortcut] =
     if (props == null) Nil
     else {
       var result = List.empty[Shortcut]
       for (entry <- JavaConverters.mapAsScalaMap(props)) {
         entry match {
           case (a: String, b: String) if is_shortcut(a) =>
             result ::= new Shortcut(a, b)
           case _ =>
         }
       }
       result.sortBy(_.property)
     }
 
   def get_shortcut_conflicts(keymap_name: String, keymap: Keymap): List[(Shortcut, List[Shortcut])] =
   {
     val keymap_shortcuts =
       if (keymap == null) Nil
       else convert_properties(Untyped.get[java.util.Properties](keymap, "props"))
 
     for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield {
       val conflicts =
         keymap_shortcuts.filter(s1 =>
           s.property == s1.property && s.binding != s1.binding ||
           s.property != s1.property && s.binding == s1.binding && s1.binding != "")
       (s, conflicts)
     }
   }
 
 
 
   /** table **/
 
   private def conflict_color: Color =
     PIDE.options.color_value("error_color")
 
   private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int])
   {
     override def toString: String =
       if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>"
       else
         "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" +
           HTML.output("--- " + shortcut.toString) +
         "</font></html>"
   }
 
   private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel
   {
     private val entries_count = entries.length
     private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count
     private def get_entry(row: Int): Option[Table_Entry] =
       if (has_entry(row)) Some(entries(row)) else None
 
     private val selected =
       Synchronized[Set[Int]](
         (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet)
 
     private def is_selected(row: Int): Boolean =
       selected.value.contains(row)
 
     private def select(head: Int, tail: List[Int], b: Boolean): Unit =
       selected.change(set => if (b) set + head -- tail else set - head ++ tail)
 
     def apply(keymap_name: String, keymap: Keymap)
     {
       GUI_Thread.require {}
 
       for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) {
         val b = is_selected(row)
         if (b) {
           entry.tail.foreach(i => entries(i).shortcut.reset(keymap))
           entry.shortcut.set(keymap)
         }
         else
           entry.shortcut.ignore(keymap_name)
       }
     }
 
     override def getColumnCount: Int = 2
 
     override def getColumnClass(i: Int): Class[_ <: Object] =
       if (i == 0) classOf[java.lang.Boolean] else classOf[Object]
 
     override def getColumnName(i: Int): String =
       if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???"
 
     override def getRowCount: Int = entries_count
 
     override def getValueAt(row: Int, column: Int): AnyRef =
     {
       get_entry(row) match {
         case Some(entry) if column == 0 => java.lang.Boolean.valueOf(is_selected(row))
         case Some(entry) if column == 1 => entry
         case _ => null
       }
     }
 
     override def isCellEditable(row: Int, column: Int): Boolean =
       has_entry(row) && column == 0
 
     override def setValueAt(value: AnyRef, row: Int, column: Int)
     {
       value match {
         case obj: java.lang.Boolean if has_entry(row) && column == 0 =>
           val b = obj.booleanValue
           val entry = entries(row)
           entry.head match {
             case None => select(row, entry.tail, b)
             case Some(head_row) =>
               val head_entry = entries(head_row)
               select(head_row, head_entry.tail, !b)
           }
           GUI_Thread.later { fireTableDataChanged() }
         case _ =>
       }
     }
   }
 
   private class Table(table_model: Table_Model) extends JPanel(new BorderLayout)
   {
-    private val cell_size = GUIUtilities.defaultTableCellSize()
+    private val cell_size = GenericGUIUtilities.defaultTableCellSize()
     private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15)
 
     val table = new JTable(table_model)
     table.setShowGrid(false)
     table.setIntercellSpacing(new Dimension(0, 0))
     table.setRowHeight(cell_size.height + 2)
     table.setPreferredScrollableViewportSize(table_size)
     table.setFillsViewportHeight(true)
     table.getTableHeader.setReorderingAllowed(false)
 
 		table.getColumnModel.getColumn(0).setPreferredWidth(30)
 		table.getColumnModel.getColumn(0).setMinWidth(30)
 		table.getColumnModel.getColumn(0).setMaxWidth(30)
 		table.getColumnModel.getColumn(0).setResizable(false)
 		table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30)
 
     val scroller = new JScrollPane(table)
 		scroller.getViewport.setBackground(table.getBackground)
 		scroller.setPreferredSize(table_size)
 
     add(scroller, BorderLayout.CENTER)
   }
 
 
 
   /** check with optional dialog **/
 
   def check_dialog(view: View)
   {
     GUI_Thread.require {}
 
     val keymap_manager = jEdit.getKeymapManager
     val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
     val keymap =
       keymap_manager.getKeymap(keymap_name) match {
         case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
         case keymap => keymap
       }
 
     val all_shortcut_conflicts = get_shortcut_conflicts(keymap_name, keymap)
     val no_shortcut_conflicts = for ((s, cs) <- all_shortcut_conflicts if cs.isEmpty) yield s
     val shortcut_conflicts = all_shortcut_conflicts.filter(_._2.nonEmpty)
 
     val table_entries =
       for {
         ((shortcut, conflicts), i) <- shortcut_conflicts zip
           shortcut_conflicts.scanLeft(0)({ case (i, (_, cs)) => i + 1 + cs.length })
         entry <-
           Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) ::
           conflicts.map(Table_Entry(_, Some(i), Nil))
       } yield entry
 
     val table_model = new Table_Model(table_entries)
 
     if (table_entries.nonEmpty &&
         GUI.confirm_dialog(view,
           "Pending Isabelle/jEdit keymap changes",
           JOptionPane.OK_CANCEL_OPTION,
           "The following Isabelle keymap changes are in conflict with the current",
           "jEdit keymap " + quote(keymap_name) + ":",
           new Table(table_model),
           "Selected shortcuts will be applied, unselected changes will be ignored.",
           "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0)
     { table_model.apply(keymap_name, keymap) }
 
     no_shortcut_conflicts.foreach(_.set(keymap))
 
     keymap.save()
     jEdit.saveSettings()
     jEdit.propertiesChanged()
   }
 }
diff --git a/src/Tools/jEdit/src/rich_text_area.scala b/src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala
+++ b/src/Tools/jEdit/src/rich_text_area.scala
@@ -1,697 +1,697 @@
 /*  Title:      Tools/jEdit/src/rich_text_area.scala
     Author:     Makarius
 
 Enhanced version of jEdit text area, with rich text rendering,
 tooltips, hyperlinks etc.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo}
 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
 import java.awt.font.TextAttribute
 import javax.swing.SwingUtilities
 import java.text.AttributedString
 import java.util.ArrayList
 
 import scala.util.matching.Regex
 
 import org.gjt.sp.util.Log
 import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
 import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
 
 
 class Rich_Text_Area(
   view: View,
   text_area: TextArea,
   get_rendering: () => JEdit_Rendering,
   close_action: () => Unit,
   get_search_pattern: () => Option[Regex],
   caret_update: () => Unit,
   caret_visible: Boolean,
   enable_hovering: Boolean)
 {
   private val buffer = text_area.getBuffer
 
 
   /* robust extension body */
 
   def check_robust_body: Boolean =
     GUI_Thread.require { buffer == text_area.getBuffer }
 
   def robust_body[A](default: A)(body: => A): A =
   {
     try {
       if (check_robust_body) body
       else {
         Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
         default
       }
     }
     catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default }
   }
 
 
   /* original painters */
 
   private def pick_extension(name: String): TextAreaExtension =
   {
     text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
     match {
       case List(x) => x
       case _ => error("Expected exactly one " + name)
     }
   }
 
   private val orig_text_painter =
     pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
 
 
   /* common painter state */
 
   @volatile private var painter_rendering: JEdit_Rendering = null
   @volatile private var painter_clip: Shape = null
   @volatile private var caret_focus: Set[Long] = Set.empty
 
   private val set_state = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       painter_rendering = get_rendering()
       painter_clip = gfx.getClip
       caret_focus =
         JEdit_Lib.visible_range(text_area) match {
           case Some(visible_range) if caret_enabled && !painter_rendering.snapshot.is_outdated =>
             painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range)
           case _ => Set.empty[Long]
         }
     }
   }
 
   private val reset_state = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       painter_rendering = null
       painter_clip = null
       caret_focus = Set.empty
     }
   }
 
   def robust_rendering(body: JEdit_Rendering => Unit)
   {
     robust_body(()) { body(painter_rendering) }
   }
 
 
   /* active areas within the text */
 
   private class Active_Area[A](
     rendering: JEdit_Rendering => Text.Range => Option[Text.Info[A]],
     cursor: Option[Int])
   {
     private var the_text_info: Option[(String, Text.Info[A])] = None
 
     def is_active: Boolean = the_text_info.isDefined
     def text_info: Option[(String, Text.Info[A])] = the_text_info
     def info: Option[Text.Info[A]] = the_text_info.map(_._2)
 
     def update(new_info: Option[Text.Info[A]])
     {
       val old_text_info = the_text_info
       val new_text_info =
         new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
 
       if (new_text_info != old_text_info) {
         caret_update()
         if (cursor.isDefined) {
           if (new_text_info.isDefined)
             text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))
           else
             text_area.getPainter.resetCursor()
         }
         for {
           r0 <- JEdit_Lib.visible_range(text_area)
           opt <- List(old_text_info, new_text_info)
           (_, Text.Info(r1, _)) <- opt
           r2 <- r1.try_restrict(r0)  // FIXME more precise?!
         } JEdit_Lib.invalidate_range(text_area, r2)
         the_text_info = new_text_info
       }
     }
 
     def update_rendering(r: JEdit_Rendering, range: Text.Range)
     { update(rendering(r)(range)) }
 
     def reset { update(None) }
   }
 
   // owned by GUI thread
 
   private val highlight_area =
     new Active_Area[Color](
       (rendering: JEdit_Rendering) => rendering.highlight, None)
 
   private val hyperlink_area =
     new Active_Area[PIDE.editor.Hyperlink](
       (rendering: JEdit_Rendering) => rendering.hyperlink, Some(Cursor.HAND_CURSOR))
 
   private val active_area =
     new Active_Area[XML.Elem](
       (rendering: JEdit_Rendering) => rendering.active, Some(Cursor.DEFAULT_CURSOR))
 
   private val active_areas =
     List((highlight_area, true), (hyperlink_area, true), (active_area, false))
   def active_reset(): Unit = active_areas.foreach(_._1.reset)
 
   private def area_active(): Boolean =
     active_areas.exists({ case (area, _) => area.is_active })
 
   private val focus_listener = new FocusAdapter {
     override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
   }
 
   private val window_listener = new WindowAdapter {
     override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
     override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
   }
 
   private val mouse_listener = new MouseAdapter {
     override def mouseClicked(e: MouseEvent) {
       robust_body(()) {
         hyperlink_area.info match {
           case Some(Text.Info(range, link)) =>
             if (!link.external) {
               try { text_area.moveCaretPosition(range.start) }
               catch {
                 case _: ArrayIndexOutOfBoundsException =>
                 case _: IllegalArgumentException =>
               }
               text_area.requestFocus
             }
             link.follow(view)
           case None =>
         }
         active_area.text_info match {
           case Some((text, Text.Info(_, markup))) =>
             Active.action(view, text, markup)
             close_action()
           case None =>
         }
       }
     }
   }
 
   private def mouse_inside_painter(): Boolean =
     MouseInfo.getPointerInfo match {
       case null => false
       case info =>
         val point = info.getLocation
         val painter = text_area.getPainter
         SwingUtilities.convertPointFromScreen(point, painter)
         painter.contains(point)
     }
 
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseDragged(evt: MouseEvent) {
       robust_body(()) {
         active_reset()
         Completion_Popup.Text_Area.dismissed(text_area)
         Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
       }
     }
 
     override def mouseMoved(evt: MouseEvent) {
       robust_body(()) {
         val x = evt.getX
         val y = evt.getY
-        val control = (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
+        val control = (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0
 
         if ((control || enable_hovering) && !buffer.isLoading) {
           JEdit_Lib.buffer_lock(buffer) {
             JEdit_Lib.pixel_range(text_area, x, y) match {
               case None => active_reset()
               case Some(range) =>
                 val rendering = get_rendering()
                 for ((area, require_control) <- active_areas)
                 {
                   if (control == require_control && !rendering.snapshot.is_outdated)
                     area.update_rendering(rendering, range)
                   else area.reset
                 }
             }
           }
         }
         else active_reset()
 
         if (evt.getSource == text_area.getPainter) {
           Pretty_Tooltip.invoke(() =>
             robust_body(()) {
               if (mouse_inside_painter()) {
                 val rendering = get_rendering()
                 val snapshot = rendering.snapshot
                 if (!snapshot.is_outdated) {
                   JEdit_Lib.pixel_range(text_area, x, y) match {
                     case None =>
                     case Some(range) =>
                       rendering.tooltip(range, control) match {
                         case None =>
                         case Some(tip) =>
                           val painter = text_area.getPainter
                           val loc = new Point(x, y + painter.getLineHeight / 2)
                           val results = snapshot.command_results(tip.range)
                           Pretty_Tooltip(view, painter, loc, rendering, results, tip)
                       }
                   }
                 }
               }
           })
         }
       }
     }
   }
 
 
   /* text background */
 
   private val background_painter = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       robust_rendering { rendering =>
         val fm = text_area.getPainter.getFontMetrics
 
         for (i <- physical_lines.indices) {
           if (physical_lines(i) != -1) {
             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
 
             // line background color
             for { (c, separator) <- rendering.line_background(line_range) }
             {
               gfx.setColor(rendering.color(c))
               val sep = if (separator) 2 min (line_height / 2) else 0
               gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
             }
 
             // background color
             for {
               Text.Info(range, c) <-
                 rendering.background(Rendering.background_elements, line_range, caret_focus)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(rendering.color(c))
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
             }
 
             // active area -- potentially from other snapshot
             for {
               info <- active_area.info
               Text.Info(range, _) <- info.try_restrict(line_range)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(rendering.active_hover_color)
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
             }
 
             // squiggly underline
             for {
               Text.Info(range, c) <- rendering.squiggly_underline(line_range)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(rendering.color(c))
               val x0 = (r.x / 2) * 2
               val y0 = r.y + fm.getAscent + 1
               for (x1 <- Range(x0, x0 + r.length, 2)) {
                 val y1 = if (x1 % 4 < 2) y0 else y0 + 1
                 gfx.drawLine(x1, y1, x1 + 1, y1)
               }
             }
 
             // spell checker
             for {
               spell_checker <- PIDE.plugin.spell_checker.get
               spell <- rendering.spell_checker(line_range)
               text <- JEdit_Lib.get_text(buffer, spell.range)
               info <- spell_checker.marked_words(spell.range.start, text)
               r <- JEdit_Lib.gfx_range(text_area, info.range)
             } {
               gfx.setColor(rendering.spell_checker_color)
               val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2))
               gfx.drawLine(r.x, y0, r.x + r.length, y0)
             }
           }
         }
       }
     }
   }
 
 
   /* text */
 
   private def caret_enabled: Boolean =
     caret_visible && (!text_area.hasFocus || text_area.isCaretVisible)
 
   private def caret_color(rendering: JEdit_Rendering, offset: Text.Offset): Color =
   {
     if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
     else {
       val debug_positions =
         (for {
           c <- PIDE.session.debugger.focus().iterator
           pos <- c.debug_position.iterator
         } yield pos).toList
       if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
         rendering.caret_debugger_color
       else rendering.caret_invisible_color
     }
   }
 
   private def paint_chunk_list(rendering: JEdit_Rendering,
     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   {
     val clip_rect = gfx.getClipBounds
     val painter = text_area.getPainter
     val font_context = painter.getFontRenderContext
 
     val caret_range =
       if (caret_enabled) JEdit_Lib.caret_range(text_area)
       else Text.Range.offside
 
     var w = 0.0f
     var chunk = head
     while (chunk != null) {
       val chunk_offset = line_start + chunk.offset
       if (x + w + chunk.width > clip_rect.x &&
           x + w < clip_rect.x + clip_rect.width && chunk.length > 0)
       {
         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
         val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
         val chunk_font = chunk.style.getFont
         val chunk_color = chunk.style.getForegroundColor
 
         def string_width(s: String): Float =
           if (s.isEmpty) 0.0f
           else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
 
         val markup =
           for {
             r1 <- rendering.text_color(chunk_range, chunk_color)
             r2 <- r1.try_restrict(chunk_range)
           } yield r2
 
         val padded_markup_iterator =
           if (markup.isEmpty)
             Iterator(Text.Info(chunk_range, chunk_color))
           else
             Iterator(
               Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
             markup.iterator ++
             Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
 
         var x1 = x + w
         gfx.setFont(chunk_font)
         for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) {
           val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
           gfx.setColor(color)
 
           range.try_restrict(caret_range) match {
             case Some(r) if !r.is_singularity =>
               val i = r.start - range.start
               val j = r.stop - range.start
               val s1 = str.substring(0, i)
               val s2 = str.substring(i, j)
               val s3 = str.substring(j)
 
               if (s1.nonEmpty) gfx.drawString(Word.bidi_override(s1), x1, y)
 
               val astr = new AttributedString(Word.bidi_override(s2))
               astr.addAttribute(TextAttribute.FONT, chunk_font)
               astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, r.start))
               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
               gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
 
               if (s3.nonEmpty)
                 gfx.drawString(Word.bidi_override(s3), x1 + string_width(str.substring(0, j)), y)
 
             case _ =>
               gfx.drawString(Word.bidi_override(str), x1, y)
           }
           x1 += string_width(str)
         }
       }
       w += chunk.width
       chunk = chunk.next.asInstanceOf[Chunk]
     }
     w
   }
 
   private val text_painter = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       robust_rendering { rendering =>
         val painter = text_area.getPainter
         val fm = painter.getFontMetrics
         val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext)
 
         val clip = gfx.getClip
         val x0 = text_area.getHorizontalOffset
         var y0 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent
 
         val (bullet_x, bullet_y, bullet_w, bullet_h) =
         {
           val w = fm.charWidth(' ')
           val b = (w / 2) max 1
           val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt
           ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
         }
 
         for (i <- physical_lines.indices) {
           val line = physical_lines(i)
           if (line != -1) {
             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
 
             // text chunks
             val screen_line = first_line + i
             val chunks = text_area.getChunksOfScreenLine(screen_line)
             if (chunks != null) {
               try {
                 val line_start = buffer.getLineStartOffset(line)
                 gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
                 val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
                 gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
                 orig_text_painter.paintValidLine(gfx,
                   screen_line, line, start(i), end(i), y + line_height * i)
               } finally { gfx.setClip(clip) }
             }
 
             // bullet bar
             for {
               Text.Info(range, color) <- rendering.bullet(line_range)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(color)
               gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
                 r.length - bullet_w, line_height - bullet_h)
             }
           }
           y0 += line_height
         }
       }
     }
   }
 
 
   /* foreground */
 
   private val foreground_painter = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       robust_rendering { rendering =>
         val search_pattern = get_search_pattern()
         for (i <- physical_lines.indices) {
           if (physical_lines(i) != -1) {
             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
 
             // foreground color
             for {
               Text.Info(range, c) <- rendering.foreground(line_range)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(rendering.color(c))
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
             }
 
             // search pattern
             for {
               regex <- search_pattern
               text <- JEdit_Lib.get_text(buffer, line_range)
               m <- regex.findAllMatchIn(text)
               range = Text.Range(m.start, m.end) + line_range.start
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(rendering.search_color)
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
             }
 
             // highlight range -- potentially from other snapshot
             for {
               info <- highlight_area.info
               Text.Info(range, color) <- info.try_restrict(line_range)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(color)
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
             }
 
             // hyperlink range -- potentially from other snapshot
             for {
               info <- hyperlink_area.info
               Text.Info(range, _) <- info.try_restrict(line_range)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(rendering.hyperlink_color)
               gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
             }
 
             // entity def range
             if (!area_active() && caret_visible) {
               for {
                 Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus)
                 r <- JEdit_Lib.gfx_range(text_area, range)
               } {
                 gfx.setColor(color)
                 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
               }
             }
 
             // completion range
             if (!area_active() && caret_visible) {
               for {
                 completion <- Completion_Popup.Text_Area(text_area)
                 Text.Info(range, color) <- completion.rendering(rendering, line_range)
                 r <- JEdit_Lib.gfx_range(text_area, range)
               } {
                 gfx.setColor(color)
                 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
               }
             }
           }
         }
       }
     }
   }
 
 
   /* caret -- outside of text range */
 
   private class Caret_Painter(before: Boolean) extends TextAreaExtension
   {
     override def paintValidLine(gfx: Graphics2D,
       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
     {
       robust_rendering { _ =>
         if (before) gfx.clipRect(0, 0, 0, 0)
         else gfx.setClip(painter_clip)
       }
     }
   }
 
   private val before_caret_painter1 = new Caret_Painter(true)
   private val after_caret_painter1 = new Caret_Painter(false)
   private val before_caret_painter2 = new Caret_Painter(true)
   private val after_caret_painter2 = new Caret_Painter(false)
 
   private val caret_painter = new TextAreaExtension
   {
     override def paintValidLine(gfx: Graphics2D,
       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
     {
       robust_rendering { rendering =>
         if (caret_visible) {
           val caret = text_area.getCaretPosition
           if (caret_enabled && start <= caret && caret == end - 1) {
             val painter = text_area.getPainter
             val fm = painter.getFontMetrics
 
             val offset = caret - text_area.getLineStartOffset(physical_line)
             val x = text_area.offsetToXY(physical_line, offset).x
             val y1 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent
 
             val astr = new AttributedString(" ")
             astr.addAttribute(TextAttribute.FONT, painter.getFont)
             astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, caret))
             astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
 
             val clip = gfx.getClip
             try {
               gfx.clipRect(x, y, Integer.MAX_VALUE, painter.getLineHeight)
               gfx.drawString(astr.getIterator, x, y1)
             }
             finally { gfx.setClip(clip) }
           }
         }
       }
     }
   }
 
 
   /* activation */
 
   def activate()
   {
     val painter = text_area.getPainter
     painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
     painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
     painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
     painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
     painter.addExtension(500, foreground_painter)
     painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
     painter.removeExtension(orig_text_painter)
     painter.addMouseListener(mouse_listener)
     painter.addMouseMotionListener(mouse_motion_listener)
     text_area.addFocusListener(focus_listener)
     view.addWindowListener(window_listener)
   }
 
   def deactivate()
   {
     active_reset()
     val painter = text_area.getPainter
     view.removeWindowListener(window_listener)
     text_area.removeFocusListener(focus_listener)
     painter.removeMouseMotionListener(mouse_motion_listener)
     painter.removeMouseListener(mouse_listener)
     painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
     painter.removeExtension(reset_state)
     painter.removeExtension(foreground_painter)
     painter.removeExtension(caret_painter)
     painter.removeExtension(after_caret_painter2)
     painter.removeExtension(before_caret_painter2)
     painter.removeExtension(after_caret_painter1)
     painter.removeExtension(before_caret_painter1)
     painter.removeExtension(text_painter)
     painter.removeExtension(background_painter)
     painter.removeExtension(set_state)
   }
 }
diff --git a/src/Tools/jEdit/src/scala_console.scala b/src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala
+++ b/src/Tools/jEdit/src/scala_console.scala
@@ -1,213 +1,212 @@
 /*  Title:      Tools/jEdit/src/scala_console.scala
     Author:     Makarius
 
 Scala instance of Console plugin.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import console.{Console, ConsolePane, Shell, Output}
 
 import org.gjt.sp.jedit.{jEdit, JARClassLoader}
 import org.gjt.sp.jedit.MiscUtilities
 
 import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
 
 import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
 import scala.tools.nsc.interpreter.IMain
 import scala.collection.mutable
 
 
 class Scala_Console extends Shell("Scala")
 {
   /* reconstructed jEdit/plugin classpath */
 
   private def reconstruct_classpath(): String =
   {
     def find_jars(start: String): List[String] =
       if (start != null)
         File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
           map(File.absolute_name)
       else Nil
 
     val initial_class_path =
       space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
 
     val path =
       initial_class_path :::
       find_jars(jEdit.getSettingsDirectory) :::
       find_jars(jEdit.getJEditHome)
     path.mkString(JFile.pathSeparator)
   }
 
 
   /* global state -- owned by GUI thread */
 
   @volatile private var interpreters = Map.empty[Console, Interpreter]
 
   @volatile private var global_console: Console = null
   @volatile private var global_out: Output = null
   @volatile private var global_err: Output = null
 
   private val console_stream = new OutputStream
   {
     val buf = new StringBuilder(100)
 
     override def flush()
     {
       val s = buf.synchronized { val s = buf.toString; buf.clear; s }
       val str = UTF8.decode_permissive(s)
       GUI_Thread.later {
         if (global_out == null) System.out.print(str)
         else global_out.writeAttrs(null, str)
       }
       Time.seconds(0.01).sleep  // FIXME adhoc delay to avoid loosing output
     }
 
     override def close() { flush () }
 
     def write(byte: Int)
     {
       val c = byte.toChar
       buf.synchronized { buf.append(c) }
       if (c == '\n') flush()
     }
   }
 
   private val console_writer = new Writer
   {
     def flush() { console_stream.flush() }
     def close() { console_stream.flush() }
 
     def write(cbuf: Array[Char], off: Int, len: Int)
     {
       if (len > 0) {
         UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_))
       }
     }
   }
 
   private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
   {
     global_console = console
     global_out = out
     global_err = if (err == null) out else err
     try {
       scala.Console.withErr(console_stream) {
         scala.Console.withOut(console_stream) { e }
       }
     }
     finally {
       console_stream.flush
       global_console = null
       global_out = null
       global_err = null
     }
   }
 
   private def report_error(str: String)
   {
     if (global_console == null || global_err == null) isabelle.Output.writeln(str)
     else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
   }
 
 
   /* interpreter thread */
 
   private abstract class Request
   private case class Start(console: Console) extends Request
   private case class Execute(console: Console, out: Output, err: Output, command: String)
     extends Request
 
   private class Interpreter
   {
     private val running = Synchronized[Option[Thread]](None)
     def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }
 
     private val settings = new GenericRunnerSettings(report_error)
     settings.classpath.value = reconstruct_classpath()
 
     private val interp = new IMain(settings, new PrintWriter(console_writer, true))
     {
       override def parentClassLoader = new JARClassLoader
     }
-    interp.setContextClassLoader
 
     val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
     {
       case Start(console) =>
         interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
         interp.bind("console", "console.Console", console)
         interp.interpret("import isabelle._; import isabelle.jedit._")
         true
 
       case Execute(console, out, err, command) =>
         with_console(console, out, err) {
           try {
             running.change(_ => Some(Thread.currentThread()))
             interp.interpret(command)
           }
           finally {
             running.change(_ => None)
             Exn.Interrupt.dispose()
           }
           GUI_Thread.later {
             if (err != null) err.commandDone()
             out.commandDone()
           }
           true
         }
     }
   }
 
 
   /* jEdit console methods */
 
   override def openConsole(console: Console)
   {
     val interp = new Interpreter
     interp.thread.send(Start(console))
     interpreters += (console -> interp)
   }
 
   override def closeConsole(console: Console)
   {
     interpreters.get(console) match {
       case Some(interp) =>
         interp.interrupt
         interp.thread.shutdown
         interpreters -= console
       case None =>
     }
   }
 
   override def printInfoMessage(out: Output)
   {
     out.print(null,
      "This shell evaluates Isabelle/Scala expressions.\n\n" +
      "The contents of package isabelle and isabelle.jedit are imported.\n" +
      "The following special toplevel bindings are provided:\n" +
      "  view    -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
      "  console -- jEdit Console plugin\n" +
      "  PIDE    -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n")
   }
 
   override def printPrompt(console: Console, out: Output)
   {
     out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
     out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
   }
 
   override def execute(console: Console, input: String, out: Output, err: Output, command: String)
   {
     interpreters(console).thread.send(Execute(console, out, err, command))
   }
 
   override def stop(console: Console)
   {
     interpreters.get(console).foreach(_.interrupt)
   }
 }
diff --git a/src/Tools/jEdit/src/token_markup.scala b/src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala
+++ b/src/Tools/jEdit/src/token_markup.scala
@@ -1,314 +1,314 @@
 /*  Title:      Tools/jEdit/src/token_markup.scala
     Author:     Makarius
 
 Outer syntax token markup.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import javax.swing.text.Segment
 
-import scala.collection.convert.WrapAsJava
+import scala.collection.JavaConverters
 
 import org.gjt.sp.jedit.{Mode, Buffer}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
   ParserRuleSet, ModeProvider, XModeHandler}
 import org.gjt.sp.jedit.indent.IndentRule
 import org.gjt.sp.jedit.buffer.JEditBuffer
 
 
 object Token_Markup
 {
   /* line context */
 
   object Line_Context
   {
     def init(mode: String): Line_Context =
       new Line_Context(mode, Some(Scan.Finished), Line_Structure.init)
 
     def before(buffer: JEditBuffer, line: Int): Line_Context =
       if (line == 0) init(JEdit_Lib.buffer_mode(buffer))
       else after(buffer, line - 1)
 
     def after(buffer: JEditBuffer, line: Int): Line_Context =
     {
       val line_mgr = JEdit_Lib.buffer_line_manager(buffer)
       def context =
         line_mgr.getLineContext(line) match {
           case c: Line_Context => Some(c)
           case _ => None
         }
       context getOrElse {
         buffer.markTokens(line, DummyTokenHandler.INSTANCE)
         context getOrElse init(JEdit_Lib.buffer_mode(buffer))
       }
     }
   }
 
   class Line_Context(
       val mode: String,
       val context: Option[Scan.Line_Context],
       val structure: Line_Structure)
     extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null)
   {
     def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished)
 
     override def hashCode: Int = (mode, context, structure).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Line_Context =>
           mode == other.mode && context == other.context && structure == other.structure
         case _ => false
       }
   }
 
 
   /* tokens from line (inclusive) */
 
   private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
     : Option[List[Token]] =
   {
     val line_context = Line_Context.before(buffer, line)
     for {
       ctxt <- line_context.context
       text <- JEdit_Lib.get_text(buffer, JEdit_Lib.line_range(buffer, line))
     } yield Token.explode_line(syntax.keywords, text, ctxt)._1
   }
 
   def line_token_iterator(
       syntax: Outer_Syntax,
       buffer: JEditBuffer,
       start_line: Int,
       end_line: Int): Iterator[Text.Info[Token]] =
     for {
       line <- Range(start_line max 0, end_line min buffer.getLineCount).iterator
       tokens <- try_line_tokens(syntax, buffer, line).iterator
       starts =
         tokens.iterator.scanLeft(buffer.getLineStartOffset(line))(
           (i, tok) => i + tok.source.length)
       (i, tok) <- starts zip tokens.iterator
     } yield Text.Info(Text.Range(i, i + tok.source.length), tok)
 
   def line_token_reverse_iterator(
       syntax: Outer_Syntax,
       buffer: JEditBuffer,
       start_line: Int,
       end_line: Int): Iterator[Text.Info[Token]] =
     for {
       line <- Range(start_line min (buffer.getLineCount - 1), end_line max -1, -1).iterator
       tokens <- try_line_tokens(syntax, buffer, line).iterator
       stops =
         tokens.reverseIterator.scanLeft(buffer.getLineEndOffset(line) min buffer.getLength)(
           (i, tok) => i - tok.source.length)
       (i, tok) <- stops zip tokens.reverseIterator
     } yield Text.Info(Text.Range(i - tok.source.length, i), tok)
 
 
   /* tokens from offset (inclusive) */
 
   def token_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
       Iterator[Text.Info[Token]] =
     if (JEdit_Lib.buffer_range(buffer).contains(offset))
       line_token_iterator(syntax, buffer, buffer.getLineOfOffset(offset), buffer.getLineCount).
         dropWhile(info => !info.range.contains(offset))
     else Iterator.empty
 
   def token_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
       Iterator[Text.Info[Token]] =
     if (JEdit_Lib.buffer_range(buffer).contains(offset))
       line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1).
         dropWhile(info => !info.range.contains(offset))
     else Iterator.empty
 
 
   /* command spans */
 
   def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
     : Option[Text.Info[Command_Span.Span]] =
   {
     val keywords = syntax.keywords
 
     def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
       token_reverse_iterator(syntax, buffer, i).
         find(info => keywords.is_before_command(info.info) || info.info.is_command)
 
     def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
       token_iterator(syntax, buffer, i).
         find(info => keywords.is_before_command(info.info) || info.info.is_command)
 
     if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
       val start_info =
       {
         val info1 = maybe_command_start(offset)
         info1 match {
           case Some(Text.Info(range1, tok1)) if tok1.is_command =>
             val info2 = maybe_command_start(range1.start - 1)
             info2 match {
               case Some(Text.Info(_, tok2)) if keywords.is_before_command(tok2) => info2
               case _ => info1
             }
           case _ => info1
         }
       }
       val (start_before_command, start, start_next) =
         start_info match {
           case Some(Text.Info(range, tok)) =>
             (keywords.is_before_command(tok), range.start, range.stop)
           case None => (false, 0, 0)
         }
 
       val stop_info =
       {
         val info1 = maybe_command_stop(start_next)
         info1 match {
           case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command =>
             maybe_command_stop(range1.stop)
           case _ => info1
         }
       }
       val stop =
         stop_info match {
           case Some(Text.Info(range, _)) => range.start
           case None => buffer.getLength
         }
 
       val text = JEdit_Lib.get_text(buffer, Text.Range(start, stop)).getOrElse("")
       val spans = syntax.parse_spans(text)
 
       (spans.iterator.scanLeft(start)(_ + _.length) zip spans.iterator).
         map({ case (i, span) => Text.Info(Text.Range(i, i + span.length), span) }).
         find(_.range.contains(offset))
     }
     else None
   }
 
   private def _command_span_iterator(
       syntax: Outer_Syntax,
       buffer: JEditBuffer,
       offset: Text.Offset,
       next_offset: Text.Range => Text.Offset): Iterator[Text.Info[Command_Span.Span]] =
     new Iterator[Text.Info[Command_Span.Span]]
     {
       private var next_span = command_span(syntax, buffer, offset)
       def hasNext: Boolean = next_span.isDefined
       def next: Text.Info[Command_Span.Span] =
       {
         val span = next_span.getOrElse(Iterator.empty.next)
         next_span = command_span(syntax, buffer, next_offset(span.range))
         span
       }
     }
 
   def command_span_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
       : Iterator[Text.Info[Command_Span.Span]] =
     _command_span_iterator(syntax, buffer, offset max 0, range => range.stop)
 
   def command_span_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
       : Iterator[Text.Info[Command_Span.Span]] =
     _command_span_iterator(syntax, buffer,
       (offset min buffer.getLength) - 1, range => range.start - 1)
 
 
   /* token marker */
 
   class Marker(
     protected val mode: String,
     protected val opt_buffer: Option[Buffer]) extends TokenMarker
   {
     override def hashCode: Int = (mode, opt_buffer).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Marker => mode == other.mode && opt_buffer == other.opt_buffer
         case _ => false
       }
 
     override def toString: String =
       opt_buffer match {
         case None => "Marker(" + mode + ")"
         case Some(buffer) => "Marker(" + mode + "," + JEdit_Lib.buffer_name(buffer) + ")"
       }
 
     override def markTokens(context: TokenMarker.LineContext,
         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
     {
       val line = if (raw_line == null) new Segment else raw_line
       val line_context =
         context match { case c: Line_Context => c case _ => Line_Context.init(mode) }
       val structure = line_context.structure
 
       val context1 =
       {
         val opt_syntax =
           opt_buffer match {
             case Some(buffer) => Isabelle.buffer_syntax(buffer)
             case None => Isabelle.mode_syntax(mode)
           }
         val (styled_tokens, context1) =
           (line_context.context, opt_syntax) match {
             case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
               val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
               val styled_tokens =
                 tokens.map(tok => (JEdit_Rendering.ml_token_markup(tok), tok.source))
               (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure))
 
             case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
               val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt)
               val structure1 = structure.update(syntax.keywords, tokens)
               val styled_tokens =
                 tokens.map(tok => (JEdit_Rendering.token_markup(syntax, tok), tok.source))
               (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1))
 
             case _ =>
               val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
               (List(styled_token), new Line_Context(line_context.mode, None, structure))
           }
 
         val extended = Syntax_Style.extended(line)
 
         var offset = 0
         for ((style, token) <- styled_tokens) {
           val length = token.length
           val offsets = offset until (offset + length)
           if (offsets.exists(i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
             for (i <- offsets) {
               val style1 =
                 extended.get(i) match {
                   case None => style
                   case Some(ext) => ext(style)
                 }
               handler.handleToken(line, style1, i, 1, context1)
             }
           }
           else handler.handleToken(line, style, offset, length, context1)
           offset += length
         }
         handler.handleToken(line, JEditToken.END, line.count, 0, context1)
         context1
       }
 
       val context2 = context1.intern
       handler.setLineContext(context2)
       context2
     }
   }
 
 
   /* mode provider */
 
   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   {
     for (mode <- orig_provider.getModes) addMode(mode)
 
     override def loadMode(mode: Mode, xmh: XModeHandler)
     {
       super.loadMode(mode, xmh)
       Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
       Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
         Untyped.set[java.util.List[IndentRule]](
-          mode, "indentRules", WrapAsJava.seqAsJavaList(List(indent_rule))))
+          mode, "indentRules", JavaConverters.seqAsJavaList(List(indent_rule))))
     }
   }
 }