diff --git a/src/Pure/Admin/build_log.scala b/src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala
+++ b/src/Pure/Admin/build_log.scala
@@ -1,1167 +1,1167 @@
 /*  Title:      Pure/Admin/build_log.scala
     Author:     Makarius
 
 Management of build log files and database storage.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
 import java.util.Locale
 
 import scala.collection.immutable.SortedMap
 import scala.collection.mutable
 import scala.util.matching.Regex
 
 
 object Build_Log
 {
   /** content **/
 
   /* properties */
 
   object Prop
   {
     val build_tags = SQL.Column.string("build_tags")  // lines
     val build_args = SQL.Column.string("build_args")  // lines
     val build_group_id = SQL.Column.string("build_group_id")
     val build_id = SQL.Column.string("build_id")
     val build_engine = SQL.Column.string("build_engine")
     val build_host = SQL.Column.string("build_host")
     val build_start = SQL.Column.date("build_start")
     val build_end = SQL.Column.date("build_end")
     val isabelle_version = SQL.Column.string("isabelle_version")
     val afp_version = SQL.Column.string("afp_version")
 
     val all_props: List[SQL.Column] =
       List(build_tags, build_args, build_group_id, build_id, build_engine,
         build_host, build_start, build_end, isabelle_version, afp_version)
   }
 
 
   /* settings */
 
   object Settings
   {
     val ISABELLE_BUILD_OPTIONS = SQL.Column.string("ISABELLE_BUILD_OPTIONS")
     val ML_PLATFORM = SQL.Column.string("ML_PLATFORM")
     val ML_HOME = SQL.Column.string("ML_HOME")
     val ML_SYSTEM = SQL.Column.string("ML_SYSTEM")
     val ML_OPTIONS = SQL.Column.string("ML_OPTIONS")
 
     val ml_settings = List(ML_PLATFORM, ML_HOME, ML_SYSTEM, ML_OPTIONS)
     val all_settings = ISABELLE_BUILD_OPTIONS :: ml_settings
 
     type Entry = (String, String)
     type T = List[Entry]
 
     object Entry
     {
       def unapply(s: String): Option[Entry] =
         for { (a, b) <- Properties.Eq.unapply(s) }
         yield (a, Library.perhaps_unquote(b))
       def getenv(a: String): String =
         Properties.Eq(a, quote(Isabelle_System.getenv(a)))
     }
 
     def show(): String =
       cat_lines(
         List(Entry.getenv("ISABELLE_TOOL_JAVA_OPTIONS"),
           Entry.getenv(ISABELLE_BUILD_OPTIONS.name), "") :::
         ml_settings.map(c => Entry.getenv(c.name)))
   }
 
 
   /* file names */
 
   def log_date(date: Date): String =
     String.format(Locale.ROOT, "%s.%05d",
       DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
       java.lang.Long.valueOf((date.time - date.midnight.time).ms / 1000))
 
   def log_subdir(date: Date): Path =
     Path.explode("log") + Path.explode(date.rep.getYear.toString)
 
   def log_filename(engine: String, date: Date, more: List[String] = Nil): Path =
     Path.explode((engine :: log_date(date) :: more).mkString("", "_", ".log"))
 
 
 
   /** log file **/
 
   def print_date(date: Date): String = Log_File.Date_Format(date)
 
   object Log_File
   {
     /* log file */
 
     def plain_name(name: String): String =
     {
       List(".log", ".log.gz", ".log.xz", ".gz", ".xz").find(name.endsWith) match {
         case Some(s) => Library.try_unsuffix(s, name).get
         case None => name
       }
     }
 
     def apply(name: String, lines: List[String]): Log_File =
       new Log_File(plain_name(name), lines.map(Library.trim_line))
 
     def apply(name: String, text: String): Log_File =
       new Log_File(plain_name(name), Library.trim_split_lines(text))
 
     def apply(file: JFile): Log_File =
     {
       val name = file.getName
       val text =
         if (name.endsWith(".gz")) File.read_gzip(file)
         else if (name.endsWith(".xz")) File.read_xz(file)
         else File.read(file)
       apply(name, text)
     }
 
     def apply(path: Path): Log_File = apply(path.file)
 
 
     /* log file collections */
 
     def is_log(file: JFile,
       prefixes: List[String] =
         List(Build_History.log_prefix, Identify.log_prefix, Identify.log_prefix2,
           Isatest.log_prefix, AFP_Test.log_prefix, Jenkins.log_prefix),
       suffixes: List[String] = List(".log", ".log.gz", ".log.xz")): Boolean =
     {
       val name = file.getName
 
       prefixes.exists(name.startsWith) &&
       suffixes.exists(name.endsWith) &&
       name != "isatest.log" &&
       name != "afp-test.log" &&
       name != "main.log"
     }
 
 
     /* date format */
 
     val Date_Format =
     {
       val fmts =
         Date.Formatter.variants(
           List("EEE MMM d HH:mm:ss O yyyy", "EEE MMM d HH:mm:ss VV yyyy"),
           List(Locale.ENGLISH, Locale.GERMAN)) :::
         List(
           DateTimeFormatter.RFC_1123_DATE_TIME,
           Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(Date.timezone_berlin))
 
       def tune_timezone(s: String): String =
         s match {
           case "CET" | "MET" => "GMT+1"
           case "CEST" | "MEST" => "GMT+2"
           case "EST" => "Europe/Berlin"
           case _ => s
         }
       def tune_weekday(s: String): String =
         s match {
           case "Die" => "Di"
           case "Mit" => "Mi"
           case "Don" => "Do"
           case "Fre" => "Fr"
           case "Sam" => "Sa"
           case "Son" => "So"
           case _ => s
         }
 
       def tune(s: String): String =
         Word.implode(
           Word.explode(s) match {
             case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone)
             case a :: bs => tune_weekday(a) :: bs.map(tune_timezone)
             case Nil => Nil
           }
         )
 
       Date.Format.make(fmts, tune)
     }
   }
 
   class Log_File private(val name: String, val lines: List[String])
   {
     log_file =>
 
     override def toString: String = name
 
     def text: String = cat_lines(lines)
 
     def err(msg: String): Nothing =
       error("Error in log file " + quote(name) + ": " + msg)
 
 
     /* date format */
 
     object Strict_Date
     {
       def unapply(s: String): Some[Date] =
         try { Some(Log_File.Date_Format.parse(s)) }
         catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
     }
 
 
     /* inlined text */
 
     def filter(Marker: Protocol_Message.Marker): List[String] =
       for (Marker(text) <- lines) yield text
 
     def find(Marker: Protocol_Message.Marker): Option[String] =
       lines.collectFirst({ case Marker(text) => text })
 
     def find_match(regexes: List[Regex]): Option[String] =
       regexes match {
         case Nil => None
         case regex :: rest =>
           lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
             map(res => res.get.head) orElse find_match(rest)
       }
 
 
     /* settings */
 
     def get_setting(name: String): Option[Settings.Entry] =
       lines.collectFirst({ case Settings.Entry(a, b) if a == name => a -> b })
 
     def get_all_settings: Settings.T =
       for { c <- Settings.all_settings; entry <- get_setting(c.name) }
       yield entry
 
 
     /* properties (YXML) */
 
     val cache: XML.Cache = XML.Cache.make()
 
     def parse_props(text: String): Properties.T =
       try { cache.props(XML.Decode.properties(YXML.parse_body(text))) }
       catch { case _: XML.Error => log_file.err("malformed properties") }
 
     def filter_props(marker: Protocol_Message.Marker): List[Properties.T] =
       for (text <- filter(marker) if YXML.detect(text)) yield parse_props(text)
 
     def find_props(marker: Protocol_Message.Marker): Option[Properties.T] =
       for (text <- find(marker) if YXML.detect(text)) yield parse_props(text)
 
 
     /* parse various formats */
 
     def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file)
 
     def parse_build_info(ml_statistics: Boolean = false): Build_Info =
       Build_Log.parse_build_info(log_file, ml_statistics)
 
     def parse_session_info(
         command_timings: Boolean = false,
         theory_timings: Boolean = false,
         ml_statistics: Boolean = false,
         task_statistics: Boolean = false): Session_Info =
       Build_Log.parse_session_info(
         log_file, command_timings, theory_timings, ml_statistics, task_statistics)
   }
 
 
 
   /** digested meta info: produced by Admin/build_history in log.xz file **/
 
   object Meta_Info
   {
     val empty: Meta_Info = Meta_Info(Nil, Nil)
   }
 
   sealed case class Meta_Info(props: Properties.T, settings: Settings.T)
   {
     def is_empty: Boolean = props.isEmpty && settings.isEmpty
 
     def get(c: SQL.Column): Option[String] =
       Properties.get(props, c.name) orElse
       Properties.get(settings, c.name)
 
     def get_date(c: SQL.Column): Option[Date] =
       get(c).map(Log_File.Date_Format.parse)
   }
 
   object Identify
   {
     val log_prefix = "isabelle_identify_"
     val log_prefix2 = "plain_identify_"
 
     def engine(log_file: Log_File): String =
       if (log_file.name.startsWith(Jenkins.log_prefix)) "jenkins_identify"
       else if (log_file.name.startsWith(log_prefix2)) "plain_identify"
       else "identify"
 
     def content(date: Date, isabelle_version: Option[String], afp_version: Option[String]): String =
       terminate_lines(
         List("isabelle_identify: " + Build_Log.print_date(date), "") :::
         isabelle_version.map("Isabelle version: " + _).toList :::
         afp_version.map("AFP version: " + _).toList)
 
     val Start = new Regex("""^isabelle_identify: (.+)$""")
     val No_End = new Regex("""$.""")
     val Isabelle_Version = List(new Regex("""^Isabelle version: (\S+)$"""))
     val AFP_Version = List(new Regex("""^AFP version: (\S+)$"""))
   }
 
   object Isatest
   {
     val log_prefix = "isatest-makeall-"
     val engine = "isatest"
     val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
     val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
     val Isabelle_Version = List(new Regex("""^Isabelle version: (\S+)$"""))
   }
 
   object AFP_Test
   {
     val log_prefix = "afp-test-devel-"
     val engine = "afp-test"
     val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
     val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
     val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
     val Isabelle_Version = List(new Regex("""^Isabelle version: .* -- hg id (\S+)$"""))
     val AFP_Version = List(new Regex("""^AFP version: .* -- hg id (\S+)$"""))
     val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
   }
 
   object Jenkins
   {
     val log_prefix = "jenkins_"
     val engine = "jenkins"
     val Host = new Regex("""^Building remotely on (\S+) \((\S+)\).*$""")
     val Start = new Regex("""^(?:Started by an SCM change|Started from command line by admin|).*$""")
     val Start_Date = new Regex("""^Build started at (.+)$""")
     val No_End = new Regex("""$.""")
     val Isabelle_Version =
       List(new Regex("""^(?:Build for Isabelle id|Isabelle id) (\w+).*$"""),
         new Regex("""^ISABELLE_CI_REPO_ID="(\w+)".*$"""),
         new Regex("""^(\w{12}) tip.*$"""))
     val AFP_Version =
       List(new Regex("""^(?:Build for AFP id|AFP id) (\w+).*$"""),
         new Regex("""^ISABELLE_CI_AFP_ID="(\w+)".*$"""))
     val CONFIGURATION = "=== CONFIGURATION ==="
     val BUILD = "=== BUILD ==="
   }
 
   private def parse_meta_info(log_file: Log_File): Meta_Info =
   {
     def parse(engine: String, host: String, start: Date,
       End: Regex, Isabelle_Version: List[Regex], AFP_Version: List[Regex]): Meta_Info =
     {
       val build_id =
       {
         val prefix = proper_string(host) orElse proper_string(engine) getOrElse "build"
         prefix + ":" + start.time.ms
       }
       val build_engine = if (engine == "") Nil else List(Prop.build_engine.name -> engine)
       val build_host = if (host == "") Nil else List(Prop.build_host.name -> host)
 
       val start_date = List(Prop.build_start.name -> print_date(start))
       val end_date =
         log_file.lines.last match {
           case End(log_file.Strict_Date(end_date)) =>
             List(Prop.build_end.name -> print_date(end_date))
           case _ => Nil
         }
 
       val isabelle_version =
         log_file.find_match(Isabelle_Version).map(Prop.isabelle_version.name -> _)
       val afp_version =
         log_file.find_match(AFP_Version).map(Prop.afp_version.name -> _)
 
       Meta_Info((Prop.build_id.name -> build_id) :: build_engine ::: build_host :::
           start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
         log_file.get_all_settings)
     }
 
     log_file.lines match {
       case line :: _ if Protocol.Meta_Info_Marker.test_yxml(line) =>
         Meta_Info(log_file.find_props(Protocol.Meta_Info_Marker).get, log_file.get_all_settings)
 
       case Identify.Start(log_file.Strict_Date(start)) :: _ =>
         parse(Identify.engine(log_file), "", start, Identify.No_End,
           Identify.Isabelle_Version, Identify.AFP_Version)
 
       case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
         parse(Isatest.engine, host, start, Isatest.End,
           Isatest.Isabelle_Version, Nil)
 
       case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ =>
         parse(AFP_Test.engine, host, start, AFP_Test.End,
           AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
 
       case AFP_Test.Start_Old(log_file.Strict_Date(start)) :: _ =>
         parse(AFP_Test.engine, "", start, AFP_Test.End,
           AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
 
       case Jenkins.Start() :: _ =>
         log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
           case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
             val host =
               log_file.lines.takeWhile(_ != Jenkins.CONFIGURATION).collectFirst({
                 case Jenkins.Host(a, b) => a + "." + b
               }).getOrElse("")
             parse(Jenkins.engine, host, start.to(Date.timezone_berlin), Jenkins.No_End,
               Jenkins.Isabelle_Version, Jenkins.AFP_Version)
           case _ => Meta_Info.empty
         }
 
       case line :: _ if line.startsWith("\u0000") => Meta_Info.empty
       case List(Isatest.End(_)) => Meta_Info.empty
       case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
       case Nil => Meta_Info.empty
 
       case _ => log_file.err("cannot detect log file format")
     }
   }
 
 
 
   /** build info: toplevel output of isabelle build or Admin/build_history **/
 
   val SESSION_NAME = "session_name"
 
   object Session_Status extends Enumeration
   {
     val existing, finished, failed, cancelled = Value
   }
 
   sealed case class Session_Entry(
     chapter: String = "",
     groups: List[String] = Nil,
     threads: Option[Int] = None,
     timing: Timing = Timing.zero,
     ml_timing: Timing = Timing.zero,
     sources: Option[String] = None,
     heap_size: Option[Long] = None,
     status: Option[Session_Status.Value] = None,
     errors: List[String] = Nil,
     theory_timings: Map[String, Timing] = Map.empty,
     ml_statistics: List[Properties.T] = Nil)
   {
     def proper_groups: Option[String] = if (groups.isEmpty) None else Some(cat_lines(groups))
     def finished: Boolean = status == Some(Session_Status.finished)
     def failed: Boolean = status == Some(Session_Status.failed)
   }
 
   object Build_Info
   {
     val sessions_dummy: Map[String, Session_Entry] =
       Map("" -> Session_Entry(theory_timings = Map("" -> Timing.zero)))
   }
 
   sealed case class Build_Info(sessions: Map[String, Session_Entry])
   {
     def finished_sessions: List[String] = for ((a, b) <- sessions.toList if b.finished) yield a
     def failed_sessions: List[String] = for ((a, b) <- sessions.toList if b.failed) yield a
   }
 
   private def parse_build_info(log_file: Log_File, parse_ml_statistics: Boolean): Build_Info =
   {
     object Chapter_Name
     {
       def unapply(s: String): Some[(String, String)] =
         space_explode('/', s) match {
           case List(chapter, name) => Some((chapter, name))
           case _ => Some(("", s))
         }
     }
 
     val Session_No_Groups = new Regex("""^Session (\S+)$""")
     val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
     val Session_Finished1 =
       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
     val Session_Finished2 =
       new Regex("""^Finished ([^\s/]+) \((\d+):(\d+):(\d+) elapsed time.*$""")
     val Session_Timing =
       new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
     val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""")
     val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
 
     object Theory_Timing
     {
       def unapply(line: String): Option[(String, (String, Timing))] =
         Protocol.Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props)
         match {
           case Some((SESSION_NAME, session) :: props) =>
             for (theory <- Markup.Name.unapply(props))
-            yield (session, theory -> Markup.Timing_Properties.parse(props))
+            yield (session, theory -> Markup.Timing_Properties.get(props))
           case _ => None
         }
     }
 
     var chapter = Map.empty[String, String]
     var groups = Map.empty[String, List[String]]
     var threads = Map.empty[String, Int]
     var timing = Map.empty[String, Timing]
     var ml_timing = Map.empty[String, Timing]
     var started = Set.empty[String]
     var sources = Map.empty[String, String]
     var heap_sizes = Map.empty[String, Long]
     var theory_timings = Map.empty[String, Map[String, Timing]]
     var ml_statistics = Map.empty[String, List[Properties.T]]
     var errors = Map.empty[String, List[String]]
 
     def all_sessions: Set[String] =
       chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
       started ++ sources.keySet ++ heap_sizes.keySet ++
       theory_timings.keySet ++ ml_statistics.keySet
 
 
     for (line <- log_file.lines) {
       line match {
         case Session_No_Groups(Chapter_Name(chapt, name)) =>
           chapter += (name -> chapt)
           groups += (name -> Nil)
 
         case Session_Groups(Chapter_Name(chapt, name), grps) =>
           chapter += (name -> chapt)
           groups += (name -> Word.explode(grps))
 
         case Session_Started(name) =>
           started += name
 
         case Session_Finished1(name,
             Value.Int(e1), Value.Int(e2), Value.Int(e3),
             Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
           val elapsed = Time.hms(e1, e2, e3)
           val cpu = Time.hms(c1, c2, c3)
           timing += (name -> Timing(elapsed, cpu, Time.zero))
 
         case Session_Finished2(name,
             Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
           val elapsed = Time.hms(e1, e2, e3)
           timing += (name -> Timing(elapsed, Time.zero, Time.zero))
 
         case Session_Timing(name,
             Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
           val elapsed = Time.seconds(e)
           val cpu = Time.seconds(c)
           val gc = Time.seconds(g)
           ml_timing += (name -> Timing(elapsed, cpu, gc))
           threads += (name -> t)
 
         case Sources(name, s) =>
           sources += (name -> s)
 
         case Heap(name, Value.Long(size)) =>
           heap_sizes += (name -> size)
 
         case _ if Protocol.Theory_Timing_Marker.test_yxml(line) =>
           line match {
             case Theory_Timing(name, theory_timing) =>
               theory_timings += (name -> (theory_timings.getOrElse(name, Map.empty) + theory_timing))
             case _ => log_file.err("malformed theory_timing " + quote(line))
           }
 
         case _ if parse_ml_statistics && Protocol.ML_Statistics_Marker.test_yxml(line) =>
           Protocol.ML_Statistics_Marker.unapply(line).map(log_file.parse_props) match {
             case Some((SESSION_NAME, name) :: props) =>
               ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
             case _ => log_file.err("malformed ML_statistics " + quote(line))
           }
 
         case _ if Protocol.Error_Message_Marker.test_yxml(line) =>
           Protocol.Error_Message_Marker.unapply(line).map(log_file.parse_props) match {
             case Some(List((SESSION_NAME, name), (Markup.CONTENT, msg))) =>
               errors += (name -> (msg :: errors.getOrElse(name, Nil)))
             case _ => log_file.err("malformed error message " + quote(line))
           }
 
         case _ =>
       }
     }
 
     val sessions =
       Map(
         (for (name <- all_sessions.toList) yield {
           val status =
             if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
               Session_Status.finished
             else if (started(name)) Session_Status.failed
             else Session_Status.existing
           val entry =
             Session_Entry(
               chapter = chapter.getOrElse(name, ""),
               groups = groups.getOrElse(name, Nil),
               threads = threads.get(name),
               timing = timing.getOrElse(name, Timing.zero),
               ml_timing = ml_timing.getOrElse(name, Timing.zero),
               sources = sources.get(name),
               heap_size = heap_sizes.get(name),
               status = Some(status),
               errors = errors.getOrElse(name, Nil).reverse,
               theory_timings = theory_timings.getOrElse(name, Map.empty),
               ml_statistics = ml_statistics.getOrElse(name, Nil).reverse)
           (name -> entry)
         }):_*)
     Build_Info(sessions)
   }
 
 
 
   /** session info: produced by isabelle build as session database **/
 
   sealed case class Session_Info(
     session_timing: Properties.T,
     command_timings: List[Properties.T],
     theory_timings: List[Properties.T],
     ml_statistics: List[Properties.T],
     task_statistics: List[Properties.T],
     errors: List[String])
   {
     def error(s: String): Session_Info =
       copy(errors = errors ::: List(s))
   }
 
   private def parse_session_info(
     log_file: Log_File,
     command_timings: Boolean,
     theory_timings: Boolean,
     ml_statistics: Boolean,
     task_statistics: Boolean): Session_Info =
   {
     Session_Info(
       session_timing = log_file.find_props(Protocol.Session_Timing_Marker) getOrElse Nil,
       command_timings =
         if (command_timings) log_file.filter_props(Protocol.Command_Timing_Marker) else Nil,
       theory_timings =
         if (theory_timings) log_file.filter_props(Protocol.Theory_Timing_Marker) else Nil,
       ml_statistics =
         if (ml_statistics) log_file.filter_props(Protocol.ML_Statistics_Marker) else Nil,
       task_statistics =
         if (task_statistics) log_file.filter_props(Protocol.Task_Statistics_Marker) else Nil,
       errors = log_file.filter(Protocol.Error_Message_Marker))
   }
 
   def compress_errors(errors: List[String], cache: XZ.Cache = XZ.Cache()): Option[Bytes] =
     if (errors.isEmpty) None
     else {
       Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
         compress(cache = cache))
     }
 
   def uncompress_errors(bytes: Bytes, cache: XML.Cache = XML.Cache.make()): List[String] =
     if (bytes.is_empty) Nil
     else {
       XML.Decode.list(YXML.string_of_body)(
         YXML.parse_body(bytes.uncompress(cache = cache.xz).text, cache = cache))
     }
 
 
 
   /** persistent store **/
 
   /* SQL data model */
 
   object Data
   {
     def build_log_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
       SQL.Table("isabelle_build_log_" + name, columns, body)
 
 
     /* main content */
 
     val log_name = SQL.Column.string("log_name").make_primary_key
     val session_name = SQL.Column.string("session_name").make_primary_key
     val theory_name = SQL.Column.string("theory_name").make_primary_key
     val chapter = SQL.Column.string("chapter")
     val groups = SQL.Column.string("groups")
     val threads = SQL.Column.int("threads")
     val timing_elapsed = SQL.Column.long("timing_elapsed")
     val timing_cpu = SQL.Column.long("timing_cpu")
     val timing_gc = SQL.Column.long("timing_gc")
     val timing_factor = SQL.Column.double("timing_factor")
     val ml_timing_elapsed = SQL.Column.long("ml_timing_elapsed")
     val ml_timing_cpu = SQL.Column.long("ml_timing_cpu")
     val ml_timing_gc = SQL.Column.long("ml_timing_gc")
     val ml_timing_factor = SQL.Column.double("ml_timing_factor")
     val theory_timing_elapsed = SQL.Column.long("theory_timing_elapsed")
     val theory_timing_cpu = SQL.Column.long("theory_timing_cpu")
     val theory_timing_gc = SQL.Column.long("theory_timing_gc")
     val heap_size = SQL.Column.long("heap_size")
     val status = SQL.Column.string("status")
     val errors = SQL.Column.bytes("errors")
     val sources = SQL.Column.string("sources")
     val ml_statistics = SQL.Column.bytes("ml_statistics")
     val known = SQL.Column.bool("known")
 
     val meta_info_table =
       build_log_table("meta_info", log_name :: Prop.all_props ::: Settings.all_settings)
 
     val sessions_table =
       build_log_table("sessions",
         List(log_name, session_name, chapter, groups, threads, timing_elapsed, timing_cpu,
           timing_gc, timing_factor, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor,
           heap_size, status, errors, sources))
 
     val theories_table =
       build_log_table("theories",
         List(log_name, session_name, theory_name, theory_timing_elapsed, theory_timing_cpu,
           theory_timing_gc))
 
     val ml_statistics_table =
       build_log_table("ml_statistics", List(log_name, session_name, ml_statistics))
 
 
     /* AFP versions */
 
     val isabelle_afp_versions_table: SQL.Table =
     {
       val version1 = Prop.isabelle_version
       val version2 = Prop.afp_version
       build_log_table("isabelle_afp_versions", List(version1.make_primary_key, version2),
         SQL.select(List(version1, version2), distinct = true) + meta_info_table +
         " WHERE " + version1.defined + " AND " + version2.defined)
     }
 
 
     /* earliest pull date for repository version (PostgreSQL queries) */
 
     def pull_date(afp: Boolean = false): SQL.Column =
       if (afp) SQL.Column.date("afp_pull_date")
       else SQL.Column.date("pull_date")
 
     def pull_date_table(afp: Boolean = false): SQL.Table =
     {
       val (name, versions) =
         if (afp) ("afp_pull_date", List(Prop.isabelle_version, Prop.afp_version))
         else ("pull_date", List(Prop.isabelle_version))
 
       build_log_table(name, versions.map(_.make_primary_key) ::: List(pull_date(afp)),
         "SELECT " + versions.mkString(", ") +
           ", min(" + Prop.build_start + ") AS " + pull_date(afp) +
         " FROM " + meta_info_table +
         " WHERE " + (versions ::: List(Prop.build_start)).map(_.defined).mkString(" AND ") +
         " GROUP BY " + versions.mkString(", "))
     }
 
 
     /* recent entries */
 
     def recent_time(days: Int): SQL.Source =
       "now() - INTERVAL '" + days.max(0) + " days'"
 
     def recent_pull_date_table(
       days: Int, rev: String = "", afp_rev: Option[String] = None): SQL.Table =
     {
       val afp = afp_rev.isDefined
       val rev2 = afp_rev.getOrElse("")
       val table = pull_date_table(afp)
 
       val version1 = Prop.isabelle_version
       val version2 = Prop.afp_version
       val eq1 = version1(table).toString + " = " + SQL.string(rev)
       val eq2 = version2(table).toString + " = " + SQL.string(rev2)
 
       SQL.Table("recent_pull_date", table.columns,
         table.select(table.columns,
           "WHERE " + pull_date(afp)(table) + " > " + recent_time(days) +
           (if (rev != "" && rev2 == "") " OR " + eq1
            else if (rev == "" && rev2 != "") " OR " + eq2
            else if (rev != "" && rev2 != "") " OR (" + eq1 + " AND " + eq2 + ")"
            else "")))
     }
 
     def select_recent_log_names(days: Int): SQL.Source =
     {
       val table1 = meta_info_table
       val table2 = recent_pull_date_table(days)
       table1.select(List(log_name), distinct = true) + SQL.join_inner + table2.query_named +
         " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
     }
 
     def select_recent_versions(days: Int,
       rev: String = "", afp_rev: Option[String] = None, sql: SQL.Source = ""): SQL.Source =
     {
       val afp = afp_rev.isDefined
       val version = Prop.isabelle_version
       val table1 = recent_pull_date_table(days, rev = rev, afp_rev = afp_rev)
       val table2 = meta_info_table
       val aux_table = SQL.Table("aux", table2.columns, table2.select(sql = sql))
 
       val columns =
         table1.columns.map(c => c(table1)) :::
           List(known.copy(expr = log_name(aux_table).defined))
       SQL.select(columns, distinct = true) +
         table1.query_named + SQL.join_outer + aux_table.query_named +
         " ON " + version(table1) + " = " + version(aux_table) +
         " ORDER BY " + pull_date(afp)(table1) + " DESC"
     }
 
 
     /* universal view on main data */
 
     val universal_table: SQL.Table =
     {
       val afp_pull_date = pull_date(afp = true)
       val version1 = Prop.isabelle_version
       val version2 = Prop.afp_version
       val table1 = meta_info_table
       val table2 = pull_date_table(afp = true)
       val table3 = pull_date_table()
 
       val a_columns = log_name :: afp_pull_date :: table1.columns.tail
       val a_table =
         SQL.Table("a", a_columns,
           SQL.select(List(log_name, afp_pull_date) ::: table1.columns.tail.map(_.apply(table1))) +
           table1 + SQL.join_outer + table2 +
           " ON " + version1(table1) + " = " + version1(table2) +
           " AND " + version2(table1) + " = " + version2(table2))
 
       val b_columns = log_name :: pull_date() :: a_columns.tail
       val b_table =
         SQL.Table("b", b_columns,
           SQL.select(
             List(log_name(a_table), pull_date()(table3)) ::: a_columns.tail.map(_.apply(a_table))) +
           a_table.query_named + SQL.join_outer + table3 +
           " ON " + version1(a_table) + " = " + version1(table3))
 
       val c_columns = b_columns ::: sessions_table.columns.tail
       val c_table =
         SQL.Table("c", c_columns,
           SQL.select(log_name(b_table) :: c_columns.tail) +
           b_table.query_named + SQL.join_inner + sessions_table +
           " ON " + log_name(b_table) + " = " + log_name(sessions_table))
 
       SQL.Table("isabelle_build_log", c_columns ::: List(ml_statistics),
         {
           SQL.select(c_columns.map(_.apply(c_table)) ::: List(ml_statistics)) +
           c_table.query_named + SQL.join_outer + ml_statistics_table +
           " ON " + log_name(c_table) + " = " + log_name(ml_statistics_table) +
           " AND " + session_name(c_table) + " = " + session_name(ml_statistics_table)
         })
     }
   }
 
 
   /* database access */
 
   def store(options: Options, cache: XML.Cache = XML.Cache.make()): Store =
     new Store(options, cache)
 
   class Store private[Build_Log](options: Options, val cache: XML.Cache)
   {
     def open_database(
       user: String = options.string("build_log_database_user"),
       password: String = options.string("build_log_database_password"),
       database: String = options.string("build_log_database_name"),
       host: String = options.string("build_log_database_host"),
       port: Int = options.int("build_log_database_port"),
       ssh_host: String = options.string("build_log_ssh_host"),
       ssh_user: String = options.string("build_log_ssh_user"),
       ssh_port: Int = options.int("build_log_ssh_port")): PostgreSQL.Database =
     {
       PostgreSQL.open_database(
         user = user, password = password, database = database, host = host, port = port,
         ssh =
           if (ssh_host == "") None
           else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = ssh_port)),
         ssh_close = true)
     }
 
     def update_database(
       db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false): Unit =
     {
       val log_files =
         dirs.flatMap(dir =>
           File.find_files(dir.file, pred = Log_File.is_log(_), follow_links = true))
       write_info(db, log_files, ml_statistics = ml_statistics)
 
       db.create_view(Data.pull_date_table())
       db.create_view(Data.pull_date_table(afp = true))
       db.create_view(Data.universal_table)
     }
 
     def snapshot_database(db: PostgreSQL.Database, sqlite_database: Path,
       days: Int = 100, ml_statistics: Boolean = false): Unit =
     {
       Isabelle_System.make_directory(sqlite_database.dir)
       sqlite_database.file.delete
 
       using(SQLite.open_database(sqlite_database))(db2 =>
       {
         db.transaction {
           db2.transaction {
             // main content
             db2.create_table(Data.meta_info_table)
             db2.create_table(Data.sessions_table)
             db2.create_table(Data.theories_table)
             db2.create_table(Data.ml_statistics_table)
 
             val recent_log_names =
               db.using_statement(Data.select_recent_log_names(days))(stmt =>
                 stmt.execute_query().iterator(_.string(Data.log_name)).toList)
 
             for (log_name <- recent_log_names) {
               read_meta_info(db, log_name).foreach(meta_info =>
                 update_meta_info(db2, log_name, meta_info))
 
               update_sessions(db2, log_name, read_build_info(db, log_name))
 
               if (ml_statistics) {
                 update_ml_statistics(db2, log_name,
                   read_build_info(db, log_name, ml_statistics = true))
               }
             }
 
             // pull_date
             for (afp <- List(false, true))
             {
               val afp_rev = if (afp) Some("") else None
               val table = Data.pull_date_table(afp)
               db2.create_table(table)
               db2.using_statement(table.insert())(stmt2 =>
               {
                 db.using_statement(
                   Data.recent_pull_date_table(days, afp_rev = afp_rev).query)(stmt =>
                 {
                   val res = stmt.execute_query()
                   while (res.next()) {
                     for ((c, i) <- table.columns.zipWithIndex) {
                       stmt2.string(i + 1) = res.get_string(c)
                     }
                     stmt2.execute()
                   }
                 })
               })
             }
 
             // full view
             db2.create_view(Data.universal_table)
           }
         }
         db2.rebuild
       })
     }
 
     def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
       db.using_statement(table.select(List(column), distinct = true))(stmt =>
         stmt.execute_query().iterator(_.string(column)).toSet)
 
     def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit =
     {
       val table = Data.meta_info_table
       db.using_statement(db.insert_permissive(table))(stmt =>
       {
         stmt.string(1) = log_name
         for ((c, i) <- table.columns.tail.zipWithIndex) {
           if (c.T == SQL.Type.Date)
             stmt.date(i + 2) = meta_info.get_date(c)
           else
             stmt.string(i + 2) = meta_info.get(c)
         }
         stmt.execute()
       })
     }
 
     def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
     {
       val table = Data.sessions_table
       db.using_statement(db.insert_permissive(table))(stmt =>
       {
         val sessions =
           if (build_info.sessions.isEmpty) Build_Info.sessions_dummy
           else build_info.sessions
         for ((session_name, session) <- sessions) {
           stmt.string(1) = log_name
           stmt.string(2) = session_name
           stmt.string(3) = proper_string(session.chapter)
           stmt.string(4) = session.proper_groups
           stmt.int(5) = session.threads
           stmt.long(6) = session.timing.elapsed.proper_ms
           stmt.long(7) = session.timing.cpu.proper_ms
           stmt.long(8) = session.timing.gc.proper_ms
           stmt.double(9) = session.timing.factor
           stmt.long(10) = session.ml_timing.elapsed.proper_ms
           stmt.long(11) = session.ml_timing.cpu.proper_ms
           stmt.long(12) = session.ml_timing.gc.proper_ms
           stmt.double(13) = session.ml_timing.factor
           stmt.long(14) = session.heap_size
           stmt.string(15) = session.status.map(_.toString)
           stmt.bytes(16) = compress_errors(session.errors, cache = cache.xz)
           stmt.string(17) = session.sources
           stmt.execute()
         }
       })
     }
 
     def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
     {
       val table = Data.theories_table
       db.using_statement(db.insert_permissive(table))(stmt =>
       {
         val sessions =
           if (build_info.sessions.forall({ case (_, session) => session.theory_timings.isEmpty }))
             Build_Info.sessions_dummy
           else build_info.sessions
         for {
           (session_name, session) <- sessions
           (theory_name, timing) <- session.theory_timings
         } {
           stmt.string(1) = log_name
           stmt.string(2) = session_name
           stmt.string(3) = theory_name
           stmt.long(4) = timing.elapsed.ms
           stmt.long(5) = timing.cpu.ms
           stmt.long(6) = timing.gc.ms
           stmt.execute()
         }
       })
     }
 
     def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
     {
       val table = Data.ml_statistics_table
       db.using_statement(db.insert_permissive(table))(stmt =>
       {
         val ml_stats: List[(String, Option[Bytes])] =
           Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
             { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.xz).proper) },
             build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
         val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
         for ((session_name, ml_statistics) <- entries) {
           stmt.string(1) = log_name
           stmt.string(2) = session_name
           stmt.bytes(3) = ml_statistics
           stmt.execute()
         }
       })
     }
 
     def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false): Unit =
     {
       abstract class Table_Status(table: SQL.Table)
       {
         db.create_table(table)
         private var known: Set[String] = domain(db, table, Data.log_name)
 
         def required(file: JFile): Boolean = !known(Log_File.plain_name(file.getName))
 
         def update_db(db: SQL.Database, log_file: Log_File): Unit
         def update(log_file: Log_File): Unit =
         {
           if (!known(log_file.name)) {
             update_db(db, log_file)
             known += log_file.name
           }
         }
       }
       val status =
         List(
           new Table_Status(Data.meta_info_table) {
             override def update_db(db: SQL.Database, log_file: Log_File): Unit =
               update_meta_info(db, log_file.name, log_file.parse_meta_info())
           },
           new Table_Status(Data.sessions_table) {
             override def update_db(db: SQL.Database, log_file: Log_File): Unit =
               update_sessions(db, log_file.name, log_file.parse_build_info())
           },
           new Table_Status(Data.theories_table) {
             override def update_db(db: SQL.Database, log_file: Log_File): Unit =
               update_theories(db, log_file.name, log_file.parse_build_info())
           },
           new Table_Status(Data.ml_statistics_table) {
             override def update_db(db: SQL.Database, log_file: Log_File): Unit =
             if (ml_statistics) {
               update_ml_statistics(db, log_file.name,
                 log_file.parse_build_info(ml_statistics = true))
             }
           })
 
       for (file_group <-
             files.filter(file => status.exists(_.required(file))).
               grouped(options.int("build_log_transaction_size") max 1))
       {
         val log_files = Par_List.map[JFile, Log_File](Log_File.apply, file_group)
         db.transaction { log_files.foreach(log_file => status.foreach(_.update(log_file))) }
       }
     }
 
     def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] =
     {
       val table = Data.meta_info_table
       val columns = table.columns.tail
       db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt =>
       {
         val res = stmt.execute_query()
         if (!res.next()) None
         else {
           val results =
             columns.map(c => c.name ->
               (if (c.T == SQL.Type.Date)
                 res.get_date(c).map(Log_File.Date_Format(_))
                else
                 res.get_string(c)))
           val n = Prop.all_props.length
           val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
           val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
           Some(Meta_Info(props, settings))
         }
       })
     }
 
     def read_build_info(
       db: SQL.Database,
       log_name: String,
       session_names: List[String] = Nil,
       ml_statistics: Boolean = false): Build_Info =
     {
       val table1 = Data.sessions_table
       val table2 = Data.ml_statistics_table
 
       val where_log_name =
         Data.log_name(table1).where_equal(log_name) + " AND " +
         Data.session_name(table1) + " <> ''"
       val where =
         if (session_names.isEmpty) where_log_name
         else where_log_name + " AND " + SQL.member(Data.session_name(table1).ident, session_names)
 
       val columns1 = table1.columns.tail.map(_.apply(table1))
       val (columns, from) =
         if (ml_statistics) {
           val columns = columns1 ::: List(Data.ml_statistics(table2))
           val join =
             table1.toString + SQL.join_outer + table2 + " ON " +
             Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " +
             Data.session_name(table1) + " = " + Data.session_name(table2)
           (columns, SQL.enclose(join))
         }
         else (columns1, table1.ident)
 
       val sessions =
         db.using_statement(SQL.select(columns) + from + " " + where)(stmt =>
         {
           stmt.execute_query().iterator(res =>
           {
             val session_name = res.string(Data.session_name)
             val session_entry =
               Session_Entry(
                 chapter = res.string(Data.chapter),
                 groups = split_lines(res.string(Data.groups)),
                 threads = res.get_int(Data.threads),
                 timing = res.timing(Data.timing_elapsed, Data.timing_cpu, Data.timing_gc),
                 ml_timing =
                   res.timing(Data.ml_timing_elapsed, Data.ml_timing_cpu, Data.ml_timing_gc),
                 sources = res.get_string(Data.sources),
                 heap_size = res.get_long(Data.heap_size),
                 status = res.get_string(Data.status).map(Session_Status.withName),
                 errors = uncompress_errors(res.bytes(Data.errors), cache = cache),
                 ml_statistics =
                   if (ml_statistics) {
                     Properties.uncompress(res.bytes(Data.ml_statistics), cache = cache)
                   }
                   else Nil)
             session_name -> session_entry
           }).toMap
         })
       Build_Info(sessions)
     }
   }
 }
diff --git a/src/Pure/PIDE/markup.scala b/src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala
+++ b/src/Pure/PIDE/markup.scala
@@ -1,791 +1,768 @@
 /*  Title:      Pure/PIDE/markup.scala
     Author:     Makarius
 
 Quasi-abstract markup elements.
 */
 
 package isabelle
 
 
 object Markup
 {
   /* elements */
 
   object Elements
   {
     def apply(elems: Set[String]): Elements = new Elements(elems)
     def apply(elems: String*): Elements = apply(Set(elems: _*))
     val empty: Elements = apply()
     val full: Elements =
       new Elements(Set.empty)
       {
         override def apply(elem: String): Boolean = true
         override def toString: String = "Elements.full"
       }
   }
 
   sealed class Elements private[Markup](private val rep: Set[String])
   {
     def apply(elem: String): Boolean = rep.contains(elem)
     def + (elem: String): Elements = new Elements(rep + elem)
     def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
     def - (elem: String): Elements = new Elements(rep - elem)
     def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
     override def toString: String = rep.mkString("Elements(", ",", ")")
   }
 
 
   /* properties */
 
   val NAME = "name"
   val Name = new Properties.String(NAME)
 
   val XNAME = "xname"
   val XName = new Properties.String(XNAME)
 
   val KIND = "kind"
   val Kind = new Properties.String(KIND)
 
   val CONTENT = "content"
   val Content = new Properties.String(CONTENT)
 
   val SERIAL = "serial"
   val Serial = new Properties.Long(SERIAL)
 
   val INSTANCE = "instance"
   val Instance = new Properties.String(INSTANCE)
 
 
   /* basic markup */
 
   val Empty: Markup = Markup("", Nil)
   val Broken: Markup = Markup("broken", Nil)
 
   class Markup_String(val name: String, prop: String)
   {
-    private val Prop = new Properties.String(prop)
+    val Prop: Properties.String = new Properties.String(prop)
 
     def apply(s: String): Markup = Markup(name, Prop(s))
     def unapply(markup: Markup): Option[String] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
+    def get(markup: Markup): String = unapply(markup).getOrElse("")
   }
 
   class Markup_Int(val name: String, prop: String)
   {
-    private val Prop = new Properties.Int(prop)
+    val Prop: Properties.Int = new Properties.Int(prop)
 
     def apply(i: Int): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
+    def get(markup: Markup): Int = unapply(markup).getOrElse(0)
   }
 
   class Markup_Long(val name: String, prop: String)
   {
-    private val Prop = new Properties.Long(prop)
+    val Prop: Properties.Long = new Properties.Long(prop)
 
     def apply(i: Long): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Long] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
+    def get(markup: Markup): Long = unapply(markup).getOrElse(0)
   }
 
 
   /* meta data */
 
   val META_TITLE = "meta_title"
   val META_CREATOR = "meta_creator"
   val META_CONTRIBUTOR = "meta_contributor"
   val META_DATE = "meta_date"
   val META_LICENSE = "meta_license"
   val META_DESCRIPTION = "meta_description"
 
 
   /* formal entities */
 
   val BINDING = "binding"
   val ENTITY = "entity"
 
-  val Def = new Properties.Long("def")
-  val Ref = new Properties.Long("ref")
-
   object Entity
   {
-    object Def
-    {
-      def unapply(markup: Markup): Option[Long] =
-        if (markup.name == ENTITY) Markup.Def.unapply(markup.properties) else None
-    }
-    object Ref
-    {
-      def unapply(markup: Markup): Option[Long] =
-        if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None
-    }
+    val Def = new Markup_Long(ENTITY, "def")
+    val Ref = new Markup_Long(ENTITY, "ref")
+
     object Occ
     {
       def unapply(markup: Markup): Option[Long] =
         Def.unapply(markup) orElse Ref.unapply(markup)
     }
 
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
-        case Markup(ENTITY, props) =>
-          val kind = Kind.unapply(props).getOrElse("")
-          val name = Name.unapply(props).getOrElse("")
-          Some((kind, name))
+        case Markup(ENTITY, props) => Some((Kind.get(props), Name.get(props)))
         case _ => None
       }
   }
 
 
   /* completion */
 
   val COMPLETION = "completion"
   val NO_COMPLETION = "no_completion"
 
   val UPDATE = "update"
 
 
   /* position */
 
   val LINE = "line"
   val END_LINE = "line"
   val OFFSET = "offset"
   val END_OFFSET = "end_offset"
   val FILE = "file"
   val ID = "id"
 
   val DEF_LINE = "def_line"
   val DEF_OFFSET = "def_offset"
   val DEF_END_OFFSET = "def_end_offset"
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
   val DEF_THEORY = "def_theory"
 
   val POSITION = "position"
 
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
 
 
   /* position "def" name */
 
   private val def_names: Map[String, String] =
     Map(LINE -> DEF_LINE, OFFSET -> DEF_OFFSET, END_OFFSET -> DEF_END_OFFSET,
       FILE -> DEF_FILE, ID -> DEF_ID)
 
   def def_name(a: String): String = def_names.getOrElse(a, a + "def_")
 
 
   /* expression */
 
   val EXPRESSION = "expression"
   object Expression
   {
     def unapply(markup: Markup): Option[String] =
       markup match {
-        case Markup(EXPRESSION, Kind(kind)) => Some(kind)
-        case Markup(EXPRESSION, _) => Some("")
+        case Markup(EXPRESSION, props) => Some(Kind.get(props))
         case _ => None
       }
   }
 
 
   /* citation */
 
   val CITATION = "citation"
   val Citation = new Markup_String(CITATION, NAME)
 
 
   /* embedded languages */
 
   val Symbols = new Properties.Boolean("symbols")
   val Antiquotes = new Properties.Boolean("antiquotes")
   val Delimited = new Properties.Boolean("delimited")
 
   val LANGUAGE = "language"
   object Language
   {
     val DOCUMENT = "document"
     val ML = "ML"
     val SML = "SML"
     val PATH = "path"
     val UNKNOWN = "unknown"
 
     def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
       markup match {
         case Markup(LANGUAGE, props) =>
           (props, props, props, props) match {
             case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
               Some((name, symbols, antiquotes, delimited))
             case _ => None
           }
         case _ => None
       }
 
     object Path
     {
       def unapply(markup: Markup): Option[Boolean] =
         markup match {
           case Language(PATH, _, _, delimited) => Some(delimited)
           case _ => None
         }
     }
   }
 
 
   /* external resources */
 
   val PATH = "path"
   val Path = new Markup_String(PATH, NAME)
 
   val EXPORT_PATH = "export_path"
   val Export_Path = new Markup_String(EXPORT_PATH, NAME)
 
   val URL = "url"
   val Url = new Markup_String(URL, NAME)
 
   val DOC = "doc"
   val Doc = new Markup_String(DOC, NAME)
 
 
   /* pretty printing */
 
   val Consistent = new Properties.Boolean("consistent")
   val Indent = new Properties.Int("indent")
   val Width = new Properties.Int("width")
 
   object Block
   {
     val name = "block"
     def apply(c: Boolean, i: Int): Markup =
       Markup(name,
         (if (c) Consistent(c) else Nil) :::
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Boolean, Int)] =
       if (markup.name == name) {
-        val c = Consistent.unapply(markup.properties).getOrElse(false)
-        val i = Indent.unapply(markup.properties).getOrElse(0)
+        val c = Consistent.get(markup.properties)
+        val i = Indent.get(markup.properties)
         Some((c, i))
       }
       else None
   }
 
   object Break
   {
     val name = "break"
     def apply(w: Int, i: Int): Markup =
       Markup(name,
         (if (w != 0) Width(w) else Nil) :::
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Int, Int)] =
       if (markup.name == name) {
-        val w = Width.unapply(markup.properties).getOrElse(0)
-        val i = Indent.unapply(markup.properties).getOrElse(0)
+        val w = Width.get(markup.properties)
+        val i = Indent.get(markup.properties)
         Some((w, i))
       }
       else None
   }
 
   val ITEM = "item"
   val BULLET = "bullet"
 
   val SEPARATOR = "separator"
 
 
   /* text properties */
 
   val WORDS = "words"
 
   val HIDDEN = "hidden"
 
   val DELETE = "delete"
 
 
   /* misc entities */
 
   val SESSION = "session"
 
   val THEORY = "theory"
   val CLASS = "class"
   val LOCALE = "locale"
   val BUNDLE = "bundle"
   val TYPE_NAME = "type_name"
   val CONSTANT = "constant"
   val AXIOM = "axiom"
   val FACT = "fact"
   val ORACLE = "oracle"
 
   val FIXED = "fixed"
   val CASE = "case"
   val DYNAMIC_FACT = "dynamic_fact"
   val LITERAL_FACT = "literal_fact"
 
   val ATTRIBUTE = "attribute"
   val METHOD = "method"
   val METHOD_MODIFIER = "method_modifier"
 
 
   /* inner syntax */
 
   val TFREE = "tfree"
   val TVAR = "tvar"
   val FREE = "free"
   val SKOLEM = "skolem"
   val BOUND = "bound"
   val VAR = "var"
   val NUMERAL = "numeral"
   val LITERAL = "literal"
   val DELIMITER = "delimiter"
   val INNER_STRING = "inner_string"
   val INNER_CARTOUCHE = "inner_cartouche"
 
   val TOKEN_RANGE = "token_range"
 
   val SORTING = "sorting"
   val TYPING = "typing"
   val CLASS_PARAMETER = "class_parameter"
 
 
   /* antiquotations */
 
   val ANTIQUOTED = "antiquoted"
   val ANTIQUOTE = "antiquote"
 
   val ML_ANTIQUOTATION = "ML_antiquotation"
   val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
   val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
 
 
   /* document text */
 
   val RAW_TEXT = "raw_text"
   val PLAIN_TEXT = "plain_text"
 
   val PARAGRAPH = "paragraph"
   val TEXT_FOLD = "text_fold"
 
-  object Document_Tag
+  object Document_Tag extends Markup_String("document_tag", NAME)
   {
-    val ELEMENT = "document_tag"
     val IMPORTANT = "important"
     val UNIMPORTANT = "unimportant"
-
-    def unapply(markup: Markup): Option[String] =
-      markup match {
-        case Markup(ELEMENT, Name(name)) => Some(name)
-        case _ => None
-      }
   }
 
   val DOCUMENT_LATEX = "document_latex"
 
 
   /* Markdown document structure */
 
   val MARKDOWN_PARAGRAPH = "markdown_paragraph"
   val MARKDOWN_ITEM = "markdown_item"
   val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
   val Markdown_List = new Markup_String("markdown_list", "kind")
 
   val ITEMIZE = "itemize"
   val ENUMERATE = "enumerate"
   val DESCRIPTION = "description"
 
 
   /* ML */
 
   val ML_KEYWORD1 = "ML_keyword1"
   val ML_KEYWORD2 = "ML_keyword2"
   val ML_KEYWORD3 = "ML_keyword3"
   val ML_DELIMITER = "ML_delimiter"
   val ML_TVAR = "ML_tvar"
   val ML_NUMERAL = "ML_numeral"
   val ML_CHAR = "ML_char"
   val ML_STRING = "ML_string"
   val ML_COMMENT = "ML_comment"
 
   val ML_DEF = "ML_def"
   val ML_OPEN = "ML_open"
   val ML_STRUCTURE = "ML_structure"
   val ML_TYPING = "ML_typing"
 
   val ML_BREAKPOINT = "ML_breakpoint"
 
 
   /* outer syntax */
 
   val COMMAND_SPAN = "command_span"
   val Command_Span = new Markup_String(COMMAND_SPAN, NAME)
 
   val COMMAND = "command"
   val KEYWORD = "keyword"
   val KEYWORD1 = "keyword1"
   val KEYWORD2 = "keyword2"
   val KEYWORD3 = "keyword3"
   val QUASI_KEYWORD = "quasi_keyword"
   val IMPROPER = "improper"
   val OPERATOR = "operator"
   val STRING = "string"
   val ALT_STRING = "alt_string"
   val VERBATIM = "verbatim"
   val CARTOUCHE = "cartouche"
   val COMMENT = "comment"
 
   val LOAD_COMMAND = "load_command"
 
 
   /* comments */
 
   val COMMENT1 = "comment1"
   val COMMENT2 = "comment2"
   val COMMENT3 = "comment3"
 
 
   /* timing */
 
   val Elapsed = new Properties.Double("elapsed")
   val CPU = new Properties.Double("cpu")
   val GC = new Properties.Double("gc")
 
   object Timing_Properties
   {
     def apply(timing: isabelle.Timing): Properties.T =
       Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
 
     def unapply(props: Properties.T): Option[isabelle.Timing] =
       (props, props, props) match {
         case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
           Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
         case _ => None
       }
 
-    def parse(props: Properties.T): isabelle.Timing =
-      unapply(props) getOrElse isabelle.Timing.zero
+    def get(props: Properties.T): isabelle.Timing =
+      unapply(props).getOrElse(isabelle.Timing.zero)
   }
 
   val TIMING = "timing"
 
   object Timing
   {
     def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
 
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
         case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
         case _ => None
       }
   }
 
 
   /* process result */
 
   val Return_Code = new Properties.Int("return_code")
 
   object Process_Result
   {
     def apply(result: Process_Result): Properties.T =
       Return_Code(result.rc) :::
         (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
 
     def unapply(props: Properties.T): Option[Process_Result] =
       props match {
         case Return_Code(rc) =>
           val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
           Some(isabelle.Process_Result(rc, timing = timing))
         case _ => None
       }
   }
 
 
   /* command indentation */
 
-  object Command_Indent
-  {
-    val name = "command_indent"
-    def unapply(markup: Markup): Option[Int] =
-      if (markup.name == name) Indent.unapply(markup.properties) else None
-  }
+  val Command_Indent = new Markup_Int("command_indent", Indent.name)
 
 
   /* goals */
 
   val GOAL = "goal"
   val SUBGOAL = "subgoal"
 
 
   /* command status */
 
   val TASK = "task"
 
   val ACCEPTED = "accepted"
   val FORKED = "forked"
   val JOINED = "joined"
   val RUNNING = "running"
   val FINISHED = "finished"
   val FAILED = "failed"
   val CANCELED = "canceled"
   val INITIALIZED = "initialized"
   val FINALIZED = "finalized"
   val CONSOLIDATING = "consolidating"
   val CONSOLIDATED = "consolidated"
 
 
   /* interactive documents */
 
   val VERSION = "version"
   val ASSIGN = "assign"
 
 
   /* prover process */
 
   val PROVER_COMMAND = "prover_command"
   val PROVER_ARG = "prover_arg"
 
 
   /* messages */
 
   val INIT = "init"
   val STATUS = "status"
   val REPORT = "report"
   val RESULT = "result"
   val WRITELN = "writeln"
   val STATE = "state"
   val INFORMATION = "information"
   val TRACING = "tracing"
   val WARNING = "warning"
   val LEGACY = "legacy"
   val ERROR = "error"
   val NODES_STATUS = "nodes_status"
   val PROTOCOL = "protocol"
   val SYSTEM = "system"
   val STDOUT = "stdout"
   val STDERR = "stderr"
   val EXIT = "exit"
 
   val WRITELN_MESSAGE = "writeln_message"
   val STATE_MESSAGE = "state_message"
   val INFORMATION_MESSAGE = "information_message"
   val TRACING_MESSAGE = "tracing_message"
   val WARNING_MESSAGE = "warning_message"
   val LEGACY_MESSAGE = "legacy_message"
   val ERROR_MESSAGE = "error_message"
 
   val messages = Map(
     WRITELN -> WRITELN_MESSAGE,
     STATE -> STATE_MESSAGE,
     INFORMATION -> INFORMATION_MESSAGE,
     TRACING -> TRACING_MESSAGE,
     WARNING -> WARNING_MESSAGE,
     LEGACY -> LEGACY_MESSAGE,
     ERROR -> ERROR_MESSAGE)
 
   val message: String => String = messages.withDefault((s: String) => s)
 
   val NO_REPORT = "no_report"
 
   val BAD = "bad"
 
   val INTENSIFY = "intensify"
 
 
   /* ML profiling */
 
   val COUNT = "count"
   val ML_PROFILING_ENTRY = "ML_profiling_entry"
   val ML_PROFILING = "ML_profiling"
 
   object ML_Profiling
   {
     def unapply_entry(tree: XML.Tree): Option[isabelle.ML_Profiling.Entry] =
       tree match {
         case XML.Elem(Markup(ML_PROFILING_ENTRY, List((NAME, name), (COUNT, Value.Long(count)))), _) =>
           Some(isabelle.ML_Profiling.Entry(name, count))
         case _ => None
       }
 
     def unapply_report(tree: XML.Tree): Option[isabelle.ML_Profiling.Report] =
       tree match {
         case XML.Elem(Markup(ML_PROFILING, List((KIND, kind))), body) =>
           Some(isabelle.ML_Profiling.Report(kind, body.flatMap(unapply_entry)))
         case _ => None
       }
   }
 
 
   /* active areas */
 
   val BROWSER = "browser"
   val GRAPHVIEW = "graphview"
   val THEORY_EXPORTS = "theory_exports"
 
   val SENDBACK = "sendback"
   val PADDING = "padding"
   val PADDING_LINE = (PADDING, "line")
   val PADDING_COMMAND = (PADDING, "command")
 
   val DIALOG = "dialog"
   val Result = new Properties.String(RESULT)
 
   val JEDIT_ACTION = "jedit_action"
 
 
   /* protocol message functions */
 
   val FUNCTION = "function"
 
   class Function(val name: String)
   {
     val PROPERTY: Properties.Entry = (FUNCTION, name)
   }
 
   class Properties_Function(name: String) extends Function(name)
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
         case PROPERTY :: args => Some(args)
         case _ => None
       }
   }
 
   class Name_Function(name: String) extends Function(name)
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (NAME, a)) => Some(a)
         case _ => None
       }
   }
 
   object ML_Statistics extends Function("ML_statistics")
   {
     def unapply(props: Properties.T): Option[(Long, String)] =
       props match {
         case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
           Some((pid, stats_dir))
         case _ => None
       }
   }
 
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
   def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing")
   {
     val Threads = new Properties.Int("threads")
   }
   object Task_Statistics extends Properties_Function("task_statistics")
 
   object Loading_Theory extends Properties_Function("loading_theory")
   object Build_Session_Finished extends Function("build_session_finished")
 
   object Commands_Accepted extends Function("commands_accepted")
   object Assign_Update extends Function("assign_update")
   object Removed_Versions extends Function("removed_versions")
 
   object Invoke_Scala extends Function("invoke_scala")
   {
     def unapply(props: Properties.T): Option[(String, String)] =
       props match {
         case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
         case _ => None
       }
   }
 
   object Cancel_Scala extends Function("cancel_scala")
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (ID, id)) => Some(id)
         case _ => None
       }
   }
 
   val PRINT_OPERATIONS = "print_operations"
 
 
   /* export */
 
   val EXPORT = "export"
   val THEORY_NAME = "theory_name"
   val EXECUTABLE = "executable"
   val COMPRESS = "compress"
   val STRICT = "strict"
 
 
   /* debugger output */
 
   val DEBUGGER_STATE = "debugger_state"
   object Debugger_State
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
   val DEBUGGER_OUTPUT = "debugger_output"
   object Debugger_Output
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
 
   /* simplifier trace */
 
   val SIMP_TRACE_PANEL = "simp_trace_panel"
 
   val SIMP_TRACE_LOG = "simp_trace_log"
   val SIMP_TRACE_STEP = "simp_trace_step"
   val SIMP_TRACE_RECURSE = "simp_trace_recurse"
   val SIMP_TRACE_HINT = "simp_trace_hint"
   val SIMP_TRACE_IGNORE = "simp_trace_ignore"
 
   val SIMP_TRACE_CANCEL = "simp_trace_cancel"
   object Simp_Trace_Cancel
   {
     def unapply(props: Properties.T): Option[Long] =
       props match {
         case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
         case _ => None
       }
   }
 
 
   /* XML data representation */
 
   def encode: XML.Encode.T[Markup] = (markup: Markup) =>
   {
     import XML.Encode._
     pair(string, properties)((markup.name, markup.properties))
   }
 
   def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
   {
     import XML.Decode._
     val (name, props) = pair(string, properties)(body)
     Markup(name, props)
   }
 }
 
 
 sealed case class Markup(name: String, properties: Properties.T)
 {
   def is_empty: Boolean = name.isEmpty
 
   def markup(s: String): String =
     YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
 
   def update_properties(more_props: Properties.T): Markup =
     if (more_props.isEmpty) this
     else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) })
 
   def + (entry: Properties.Entry): Markup =
     Markup(name, Properties.put(properties, entry))
 }
diff --git a/src/Pure/PIDE/rendering.scala b/src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala
+++ b/src/Pure/PIDE/rendering.scala
@@ -1,792 +1,792 @@
 /*  Title:      Pure/PIDE/rendering.scala
     Author:     Makarius
 
 Isabelle-specific implementation of quasi-abstract rendering and
 markup interpretation.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 import java.nio.file.FileSystems
 
 import scala.collection.immutable.SortedMap
 
 
 
 object Rendering
 {
   /* color */
 
   object Color extends Enumeration
   {
     // background
     val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result,
       markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value
     val background_colors: ValueSet = values
 
     // foreground
     val quoted, antiquoted = Value
     val foreground_colors: ValueSet = values -- background_colors
 
     // message underline
     val writeln, information, warning, legacy, error = Value
     val message_underline_colors: ValueSet = values -- background_colors -- foreground_colors
 
     // message background
     val writeln_message, information_message, tracing_message,
       warning_message, legacy_message, error_message = Value
     val message_background_colors: ValueSet =
       values -- background_colors -- foreground_colors -- message_underline_colors
 
     // text
     val main, keyword1, keyword2, keyword3, quasi_keyword, improper, operator,
       tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted,
       inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter,
       antiquote, raw_text, plain_text = Value
     val text_colors: ValueSet =
       values -- background_colors -- foreground_colors -- message_underline_colors --
       message_background_colors
 
     // text overview
     val unprocessed, running = Value
     val text_overview_colors = Set(unprocessed, running, error, warning)
   }
 
 
   /* output messages */
 
   val state_pri = 1
   val writeln_pri = 2
   val information_pri = 3
   val tracing_pri = 4
   val warning_pri = 5
   val legacy_pri = 6
   val error_pri = 7
 
   val message_pri = Map(
     Markup.STATE -> state_pri,
     Markup.STATE_MESSAGE -> state_pri,
     Markup.WRITELN -> writeln_pri,
     Markup.WRITELN_MESSAGE -> writeln_pri,
     Markup.INFORMATION -> information_pri,
     Markup.INFORMATION_MESSAGE -> information_pri,
     Markup.TRACING -> tracing_pri,
     Markup.TRACING_MESSAGE -> tracing_pri,
     Markup.WARNING -> warning_pri,
     Markup.WARNING_MESSAGE -> warning_pri,
     Markup.LEGACY -> legacy_pri,
     Markup.LEGACY_MESSAGE -> legacy_pri,
     Markup.ERROR -> error_pri,
     Markup.ERROR_MESSAGE -> error_pri
   ).withDefaultValue(0)
 
   val message_underline_color = Map(
     writeln_pri -> Color.writeln,
     information_pri -> Color.information,
     warning_pri -> Color.warning,
     legacy_pri -> Color.legacy,
     error_pri -> Color.error)
 
   val message_background_color = Map(
     writeln_pri -> Color.writeln_message,
     information_pri -> Color.information_message,
     tracing_pri -> Color.tracing_message,
     warning_pri -> Color.warning_message,
     legacy_pri -> Color.legacy_message,
     error_pri -> Color.error_message)
 
   def output_messages(results: Command.Results): List[XML.Elem] =
   {
     val (states, other) =
       results.iterator.map(_._2).filterNot(Protocol.is_result).toList
         .partition(Protocol.is_state)
     states ::: other
   }
 
 
   /* text color */
 
   val text_color = Map(
     Markup.KEYWORD1 -> Color.keyword1,
     Markup.KEYWORD2 -> Color.keyword2,
     Markup.KEYWORD3 -> Color.keyword3,
     Markup.QUASI_KEYWORD -> Color.quasi_keyword,
     Markup.IMPROPER -> Color.improper,
     Markup.OPERATOR -> Color.operator,
     Markup.STRING -> Color.main,
     Markup.ALT_STRING -> Color.main,
     Markup.VERBATIM -> Color.main,
     Markup.CARTOUCHE -> Color.main,
     Markup.LITERAL -> Color.keyword1,
     Markup.DELIMITER -> Color.main,
     Markup.TFREE -> Color.tfree,
     Markup.TVAR -> Color.tvar,
     Markup.FREE -> Color.free,
     Markup.SKOLEM -> Color.skolem,
     Markup.BOUND -> Color.bound,
     Markup.VAR -> Color.`var`,
     Markup.INNER_STRING -> Color.inner_quoted,
     Markup.INNER_CARTOUCHE -> Color.inner_cartouche,
     Markup.DYNAMIC_FACT -> Color.dynamic,
     Markup.CLASS_PARAMETER -> Color.class_parameter,
     Markup.ANTIQUOTE -> Color.antiquote,
     Markup.RAW_TEXT -> Color.raw_text,
     Markup.PLAIN_TEXT -> Color.plain_text,
     Markup.ML_KEYWORD1 -> Color.keyword1,
     Markup.ML_KEYWORD2 -> Color.keyword2,
     Markup.ML_KEYWORD3 -> Color.keyword3,
     Markup.ML_DELIMITER -> Color.main,
     Markup.ML_NUMERAL -> Color.inner_numeral,
     Markup.ML_CHAR -> Color.inner_quoted,
     Markup.ML_STRING -> Color.inner_quoted,
     Markup.ML_COMMENT -> Color.comment1,
     Markup.COMMENT -> Color.comment1,
     Markup.COMMENT1 -> Color.comment1,
     Markup.COMMENT2 -> Color.comment2,
     Markup.COMMENT3 -> Color.comment3)
 
   val foreground =
     Map(
       Markup.STRING -> Color.quoted,
       Markup.ALT_STRING -> Color.quoted,
       Markup.VERBATIM -> Color.quoted,
       Markup.CARTOUCHE -> Color.quoted,
       Markup.ANTIQUOTED -> Color.antiquoted)
 
 
   /* tooltips */
 
   val tooltip_descriptions =
     Map(
       Markup.CITATION -> "citation",
       Markup.TOKEN_RANGE -> "inner syntax token",
       Markup.FREE -> "free variable",
       Markup.SKOLEM -> "skolem variable",
       Markup.BOUND -> "bound variable",
       Markup.VAR -> "schematic variable",
       Markup.TFREE -> "free type variable",
       Markup.TVAR -> "schematic type variable")
 
 
   /* entity focus */
 
   object Focus
   {
     def apply(ids: Set[Long]): Focus = new Focus(ids)
     val empty: Focus = apply(Set.empty)
     def make(args: List[Text.Info[Focus]]): Focus =
       args.foldLeft(empty) { case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 }
 
     val full: Focus =
       new Focus(Set.empty)
       {
         override def apply(id: Long): Boolean = true
         override def toString: String = "Focus.full"
       }
   }
 
   sealed class Focus private[Rendering](protected val rep: Set[Long])
   {
     def defined: Boolean = rep.nonEmpty
     def apply(id: Long): Boolean = rep.contains(id)
     def + (id: Long): Focus = if (rep.contains(id)) this else new Focus(rep + id)
     def ++ (other: Focus): Focus =
       if (this eq other) this
       else if (rep.isEmpty) other
       else other.rep.iterator.foldLeft(this)(_ + _)
     override def toString: String = rep.mkString("Focus(", ",", ")")
   }
 
 
   /* markup elements */
 
   val position_elements =
     Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   val semantic_completion_elements =
     Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
 
   val language_context_elements =
     Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
       Markup.ML_STRING, Markup.ML_COMMENT)
 
   val language_elements = Markup.Elements(Markup.LANGUAGE)
 
   val citation_elements = Markup.Elements(Markup.CITATION)
 
   val active_elements =
     Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.THEORY_EXPORTS,
       Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
 
   val background_elements =
     Document_Status.Command_Status.proper_elements + Markup.WRITELN_MESSAGE +
       Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
       Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
       Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
       Markup.Markdown_Bullet.name ++ active_elements
 
   val foreground_elements = Markup.Elements(foreground.keySet)
 
   val text_color_elements = Markup.Elements(text_color.keySet)
 
   val tooltip_elements =
     Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
       Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
       Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL,
       Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++
       Markup.Elements(tooltip_descriptions.keySet)
 
   val tooltip_message_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
       Markup.BAD)
 
   val message_elements = Markup.Elements(message_pri.keySet)
   val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY)
   val error_elements = Markup.Elements(Markup.ERROR)
 
   val entity_elements = Markup.Elements(Markup.ENTITY)
 
   val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
 
   val meta_data_elements =
     Markup.Elements(Markup.META_TITLE, Markup.META_CREATOR, Markup.META_CONTRIBUTOR,
       Markup.META_DATE, Markup.META_DESCRIPTION, Markup.META_LICENSE)
 
   val document_tag_elements =
-    Markup.Elements(Markup.Document_Tag.ELEMENT)
+    Markup.Elements(Markup.Document_Tag.name)
 
   val markdown_elements =
     Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
       Markup.Markdown_Bullet.name)
 }
 
 class Rendering(
   val snapshot: Document.Snapshot,
   val options: Options,
   val session: Session)
 {
   override def toString: String = "Rendering(" + snapshot.toString + ")"
 
   def get_text(range: Text.Range): Option[String] = None
 
 
   /* caret */
 
   def before_caret_range(caret: Text.Offset): Text.Range =
   {
     val former_caret = snapshot.revert(caret)
     snapshot.convert(Text.Range(former_caret - 1, former_caret))
   }
 
 
   /* completion */
 
   def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range)
       : Option[Text.Info[Completion.Semantic]] =
     if (snapshot.is_outdated) None
     else {
       snapshot.select(caret_range, Rendering.semantic_completion_elements, _ =>
         {
           case Completion.Semantic.Info(info) =>
             completed_range match {
               case Some(range0) if range0.contains(info.range) && range0 != info.range => None
               case _ => Some(info)
             }
           case _ => None
         }).headOption.map(_.info)
     }
 
   def semantic_completion_result(
     history: Completion.History,
     unicode: Boolean,
     completed_range: Option[Text.Range],
     caret_range: Text.Range): (Boolean, Option[Completion.Result]) =
   {
     semantic_completion(completed_range, caret_range) match {
       case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
       case Some(Text.Info(range, names: Completion.Names)) =>
         get_text(range) match {
           case Some(original) => (false, names.complete(range, history, unicode, original))
           case None => (false, None)
         }
       case None => (false, None)
     }
   }
 
   def language_context(range: Text.Range): Option[Completion.Language_Context] =
     snapshot.select(range, Rendering.language_context_elements, _ =>
       {
         case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
           if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
           else None
         case Text.Info(_, elem)
         if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
           Some(Completion.Language_Context.ML_inner)
         case Text.Info(_, _) =>
           Some(Completion.Language_Context.inner)
       }).headOption.map(_.info)
 
   def citations(range: Text.Range): List[Text.Info[String]] =
     snapshot.select(range, Rendering.citation_elements, _ =>
       {
         case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
           Some(Text.Info(snapshot.convert(info_range), name))
         case _ => None
       }).map(_.info)
 
 
   /* file-system path completion */
 
   def language_path(range: Text.Range): Option[Text.Info[Boolean]] =
     snapshot.select(range, Rendering.language_elements, _ =>
       {
         case Text.Info(info_range, XML.Elem(Markup.Language.Path(delimited), _)) =>
           Some((delimited, snapshot.convert(info_range)))
         case _ => None
       }).headOption.map({ case Text.Info(_, (delimited, range)) => Text.Info(range, delimited) })
 
   def path_completion(caret: Text.Offset): Option[Completion.Result] =
   {
     def complete(text: String): List[(String, List[String])] =
     {
       try {
         val path = Path.explode(text)
         val (dir, base_name) =
           if (text == "" || text.endsWith("/")) (path, "")
           else (path.dir, path.file_name)
 
         val directory = new JFile(session.resources.append(snapshot.node_name, dir))
         val files = directory.listFiles
         if (files == null) Nil
         else {
           val ignore =
             space_explode(':', options.string("completion_path_ignore")).
               map(s => FileSystems.getDefault.getPathMatcher("glob:" + s))
           (for {
             file <- files.iterator
 
             name = file.getName
             if name.startsWith(base_name)
             path_name = new JFile(name).toPath
             if !ignore.exists(matcher => matcher.matches(path_name))
 
             text1 = (dir + Path.basic(name)).implode_short
             if text != text1
 
             is_dir = new JFile(directory, name).isDirectory
             replacement = text1 + (if (is_dir) "/" else "")
             descr = List(text1, if (is_dir) "(directory)" else "(file)")
           } yield (replacement, descr)).take(options.int("completion_limit")).toList
         }
       }
       catch { case ERROR(_) => Nil }
     }
 
     def is_wrapped(s: String): Boolean =
       s.startsWith("\"") && s.endsWith("\"") ||
       s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
 
     for {
       Text.Info(r1, delimited) <- language_path(before_caret_range(caret))
       s1 <- get_text(r1)
       (r2, s2) <-
         if (is_wrapped(s1)) {
           Some((Text.Range(r1.start + 1, r1.stop - 1), s1.substring(1, s1.length - 1)))
         }
         else if (delimited) Some((r1, s1))
         else None
       if Path.is_valid(s2)
       paths = complete(s2)
       if paths.nonEmpty
       items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
     } yield Completion.Result(r2, s2, false, items)
   }
 
 
   /* spell checker */
 
   private lazy val spell_checker_include =
     Markup.Elements(space_explode(',', options.string("spell_checker_include")): _*)
 
   private lazy val spell_checker_elements =
     spell_checker_include ++
       Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
 
   def spell_checker(range: Text.Range): List[Text.Info[Text.Range]] =
   {
     val result =
       snapshot.select(range, spell_checker_elements, _ =>
         {
           case info =>
             Some(
               if (spell_checker_include(info.info.name))
                 Some(snapshot.convert(info.range))
               else None)
         })
     for (Text.Info(range, Some(range1)) <- result)
       yield Text.Info(range, range1)
   }
 
   def spell_checker_point(range: Text.Range): Option[Text.Range] =
     spell_checker(range).headOption.map(_.info)
 
 
   /* text background */
 
   def background(elements: Markup.Elements, range: Text.Range, focus: Rendering.Focus)
     : List[Text.Info[Rendering.Color.Value]] =
   {
     for {
       Text.Info(r, result) <-
         snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
           range, (List(Markup.Empty), None), elements,
           command_states =>
             {
               case ((markups, color), Text.Info(_, XML.Elem(markup, _)))
               if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) =>
                 Some((markup :: markups, color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
                 Some((Nil, Some(Rendering.Color.bad)))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                 Some((Nil, Some(Rendering.Color.intensify)))
               case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) =>
                 Some((Nil, Some(Rendering.Color.entity)))
               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
                 val color =
                   depth % 4 match {
                     case 1 => Rendering.Color.markdown_bullet1
                     case 2 => Rendering.Color.markdown_bullet2
                     case 3 => Rendering.Color.markdown_bullet3
                     case _ => Rendering.Color.markdown_bullet4
                   }
                 Some((Nil, Some(color)))
               case (_, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
                 command_states.collectFirst(
                   { case st if st.results.defined(serial) => st.results.get(serial).get }) match
                 {
                   case Some(Protocol.Dialog_Result(res)) if res == result =>
                     Some((Nil, Some(Rendering.Color.active_result)))
                   case _ =>
                     Some((Nil, Some(Rendering.Color.active)))
                 }
               case (_, Text.Info(_, elem)) =>
                 if (Rendering.active_elements(elem.name))
                   Some((Nil, Some(Rendering.Color.active)))
                 else None
             })
       color <-
         result match {
           case (markups, opt_color) if markups.nonEmpty =>
             val status = Document_Status.Command_Status.make(markups.iterator)
             if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
             else if (status.is_running) Some(Rendering.Color.running1)
             else if (status.is_canceled) Some(Rendering.Color.canceled)
             else opt_color
           case (_, opt_color) => opt_color
         }
     } yield Text.Info(r, color)
   }
 
 
   /* text foreground */
 
   def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
     snapshot.select(range, Rendering.foreground_elements, _ =>
       {
         case info => Some(Rendering.foreground(info.info.name))
       })
 
 
   /* entity focus */
 
   def entity_focus_defs(range: Text.Range): Rendering.Focus =
     Rendering.Focus.make(
       snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ =>
         {
           case (focus, Text.Info(_, XML.Elem(Markup.Entity.Def(i), _))) => Some(focus + i)
           case _ => None
         }))
 
   def entity_focus(range: Text.Range, defs_focus: Rendering.Focus): Rendering.Focus =
     Rendering.Focus.make(
       snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ =>
         {
           case (focus, Text.Info(_, XML.Elem(Markup.Entity.Ref(i), _)))
           if defs_focus(i) => Some(focus + i)
           case _ => None
         }))
 
 
   /* caret focus */
 
   def caret_focus(caret_range: Text.Range, defs_range: Text.Range): Rendering.Focus =
   {
     val focus = entity_focus_defs(caret_range)
     if (focus.defined) focus
     else if (defs_range == Text.Range.offside) Rendering.Focus.empty
     else {
       val defs_focus =
         if (defs_range == Text.Range.full) Rendering.Focus.full
         else entity_focus_defs(defs_range)
       entity_focus(caret_range, defs_focus)
     }
   }
 
   def caret_focus_ranges(caret_range: Text.Range, defs_range: Text.Range): List[Text.Range] =
   {
     val focus = caret_focus(caret_range, defs_range)
     if (focus.defined) {
       snapshot.cumulate[Boolean](defs_range, false, Rendering.entity_elements, _ =>
         {
           case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) => Some(true)
           case _ => None
         }).flatMap(info => if (info.info) Some(info.range) else None)
     }
     else Nil
   }
 
 
   /* messages */
 
   def message_underline_color(elements: Markup.Elements, range: Text.Range)
     : List[Text.Info[Rendering.Color.Value]] =
   {
     val results =
       snapshot.cumulate[Int](range, 0, elements, _ =>
         {
           case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
         })
     for {
       Text.Info(r, pri) <- results
       color <- Rendering.message_underline_color.get(pri)
     } yield Text.Info(r, color)
   }
 
   def text_messages(range: Text.Range): List[Text.Info[XML.Elem]] =
   {
     val results =
       snapshot.cumulate[Vector[Command.Results.Entry]](
         range, Vector.empty, Rendering.message_elements, command_states =>
           {
             case (res, Text.Info(_, elem)) =>
               Command.State.get_result_proper(command_states, elem.markup.properties)
                 .map(res :+ _)
             case _ => None
           })
 
     var seen_serials = Set.empty[Long]
     def seen(i: Long): Boolean =
     {
       val b = seen_serials(i)
       seen_serials += i
       b
     }
     for {
       Text.Info(range, entries) <- results
       (i, elem) <- entries if !seen(i)
     } yield Text.Info(range, elem)
   }
 
 
   /* tooltips */
 
   def timing_threshold: Double = 0.0
 
   private sealed case class Tooltip_Info(
     range: Text.Range,
     timing: Timing = Timing.zero,
     messages: List[(Long, XML.Tree)] = Nil,
     rev_infos: List[(Boolean, XML.Tree)] = Nil)
   {
     def + (t: Timing): Tooltip_Info = copy(timing = timing + t)
     def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info =
     {
       val r = snapshot.convert(r0)
       if (range == r) copy(messages = (serial -> tree) :: messages)
       else copy(range = r, messages = List(serial -> tree))
     }
     def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info =
     {
       val r = snapshot.convert(r0)
       if (range == r) copy(rev_infos = (important -> tree) :: rev_infos)
       else copy (range = r, rev_infos = List(important -> tree))
     }
 
     def timing_info(tree: XML.Tree): Option[XML.Tree] =
       tree match {
         case XML.Elem(Markup(Markup.TIMING, _), _) =>
           if (timing.elapsed.seconds >= timing_threshold) Some(XML.Text(timing.message)) else None
         case _ => Some(tree)
       }
     def infos(important: Boolean): List[XML.Tree] =
       for {
         (is_important, tree) <- rev_infos.reverse if is_important == important
         tree1 <- timing_info(tree)
       } yield tree1
   }
 
   def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
     if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name
 
   def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   {
     val results =
       snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states =>
         {
           case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t)
 
           case (info, Text.Info(r0, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body)))
           if body.nonEmpty => Some(info + (r0, i, msg))
 
           case (info, Text.Info(r0, XML.Elem(Markup(name, props), _)))
           if Rendering.tooltip_message_elements(name) =>
             for ((i, tree) <- Command.State.get_result_proper(command_states, props))
             yield (info + (r0, i, tree))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
           if kind != "" && kind != Markup.ML_DEF =>
             val kind1 = Word.implode(Word.explode('_', kind))
             val txt1 =
               if (name == "") kind1
               else if (kind1 == "") quote(name)
               else kind1 + " " + quote(name)
             val info1 = info + (r0, true, XML.Text(txt1))
             Some(if (kind == Markup.COMMAND) info1 + (r0, true, XML.elem(Markup.TIMING)) else info1)
 
           case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
             val file = perhaps_append_file(snapshot.node_name, name)
             val text =
               if (name == file) "file " + quote(file)
               else "path " + quote(name) + "\nfile " + quote(file)
             Some(info + (r0, true, XML.Text(text)))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
             val text = "doc " + quote(name)
             Some(info + (r0, true, XML.Text(text)))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
             Some(info + (r0, true, XML.Text("URL " + quote(name))))
 
           case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
           if name == Markup.SORTING || name == Markup.TYPING =>
             Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body)))
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
             Some(info + (r0, true, Pretty.block(0, body)))
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
             Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body)))
 
           case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) =>
               val text =
                 if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
                 else "breakpoint (disabled)"
               Some(info + (r0, true, XML.Text(text)))
           case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
             val lang = Word.implode(Word.explode('_', language))
             Some(info + (r0, true, XML.Text("language: " + lang)))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
             val descr = if (kind == "") "expression" else "expression: " + kind
             Some(info + (r0, true, XML.Text(descr)))
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
             Some(info + (r0, true, XML.Text("Markdown: paragraph")))
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), _))) =>
             Some(info + (r0, true, XML.Text("Markdown: item")))
           case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
             Some(info + (r0, true, XML.Text("Markdown: " + kind)))
 
           case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) =>
             Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc)))
         }).map(_.info)
 
     if (results.isEmpty) None
     else {
       val r = Text.Range(results.head.range.start, results.last.range.stop)
       val all_tips =
         results.flatMap(_.messages).foldLeft(SortedMap.empty[Long, XML.Tree])(_ + _)
           .iterator.map(_._2).toList :::
         results.flatMap(res => res.infos(true)) :::
         results.flatMap(res => res.infos(false)).lastOption.toList
       if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))
     }
   }
 
 
   /* messages */
 
   def warnings(range: Text.Range): List[Text.Markup] =
     snapshot.select(range, Rendering.warning_elements, _ => Some(_)).map(_.info)
 
   def errors(range: Text.Range): List[Text.Markup] =
     snapshot.select(range, Rendering.error_elements, _ => Some(_)).map(_.info)
 
 
   /* command status overview */
 
   def overview_color(range: Text.Range): Option[Rendering.Color.Value] =
   {
     if (snapshot.is_outdated) None
     else {
       val results =
         snapshot.cumulate[List[Markup]](range, Nil, Document_Status.Command_Status.liberal_elements,
           _ =>
             {
               case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
             }, status = true)
       if (results.isEmpty) None
       else {
         val status = Document_Status.Command_Status.make(results.iterator.flatMap(_.info))
 
         if (status.is_running) Some(Rendering.Color.running)
         else if (status.is_failed) Some(Rendering.Color.error)
         else if (status.is_warned) Some(Rendering.Color.warning)
         else if (status.is_unprocessed) Some(Rendering.Color.unprocessed)
         else None
       }
     }
   }
 
 
   /* antiquoted text */
 
   def antiquoted(range: Text.Range): Option[Text.Range] =
     snapshot.cumulate[Option[Text.Range]](range, None, Rendering.antiquoted_elements, _ =>
       {
         case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None
       }).headOption.flatMap(_.info)
 
 
   /* meta data */
 
   def meta_data(range: Text.Range): Properties.T =
   {
     val results =
       snapshot.cumulate[Properties.T](range, Nil, Rendering.meta_data_elements, _ =>
         {
           case (res, Text.Info(_, elem)) =>
             val plain_text = XML.content(elem)
             Some((elem.name -> plain_text) :: res)
         })
     Library.distinct(results.flatMap(_.info.reverse))
   }
 
 
   /* document tags */
 
   def document_tags(range: Text.Range): List[String] =
   {
     val results =
       snapshot.cumulate[List[String]](range, Nil, Rendering.document_tag_elements, _ =>
         {
           case (res, Text.Info(_, XML.Elem(Markup.Document_Tag(name), _))) => Some(name :: res)
           case _ => None
         })
     Library.distinct(results.flatMap(_.info.reverse))
   }
 }
diff --git a/src/Pure/Thy/presentation.scala b/src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala
+++ b/src/Pure/Thy/presentation.scala
@@ -1,667 +1,668 @@
 /*  Title:      Pure/Thy/presentation.scala
     Author:     Makarius
 
 HTML presentation of PIDE document content.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.collection.immutable.SortedMap
 import scala.collection.mutable
 
 
 object Presentation
 {
   /** HTML documents **/
 
   /* HTML context */
 
   sealed case class HTML_Document(title: String, content: String)
 
   abstract class HTML_Context
   {
     /* directory structure */
 
     def root_dir: Path
     def theory_session(name: Document.Node.Name): Sessions.Info
 
     def session_dir(info: Sessions.Info): Path =
       root_dir + Path.explode(info.chapter_session)
     def theory_path(name: Document.Node.Name): Path =
       session_dir(theory_session(name)) + Path.explode(name.theory_base_name).html
     def files_path(name: Document.Node.Name, path: Path): Path =
       theory_path(name).dir + Path.explode("files") + path.squash.html
 
 
     /* cached theory exports */
 
     val cache: Term.Cache = Term.Cache.make()
 
     private val already_presented = Synchronized(Set.empty[String])
     def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] =
       already_presented.change_result(presented =>
         (nodes.filterNot(name => presented.contains(name.theory)),
           presented ++ nodes.iterator.map(_.theory)))
 
     private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory])
     def cache_theory(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory =
     {
       theory_cache.change_result(thys =>
       {
         thys.get(thy_name) match {
           case Some(thy) => (thy, thys)
           case None =>
             val thy = make_thy
             (thy, thys + (thy_name -> thy))
         }
       })
     }
 
 
     /* HTML content */
 
     def head(title: String, rest: XML.Body = Nil): XML.Tree =
       HTML.div("head", HTML.chapter(title) :: rest)
 
     def source(body: XML.Body): XML.Tree = HTML.pre("source", body)
 
     def contents(heading: String, items: List[XML.Body], css_class: String = "contents")
       : List[XML.Elem] =
     {
       if (items.isEmpty) Nil
       else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items))))
     }
 
     val isabelle_css: String = File.read(HTML.isabelle_css)
 
     def html_document(title: String, body: XML.Body, fonts_css: String): HTML_Document =
     {
       val content =
         HTML.output_document(
           List(
             HTML.style(fonts_css + "\n\n" + isabelle_css),
             HTML.title(title)),
           List(HTML.source(body)), css = "", structural = false)
       HTML_Document(title, content)
     }
   }
 
 
   /* presentation elements */
 
   sealed case class Elements(
     html: Markup.Elements = Markup.Elements.empty,
     entity: Markup.Elements = Markup.Elements.empty,
     language: Markup.Elements = Markup.Elements.empty)
 
   val elements1: Elements =
     Elements(
       html = Rendering.foreground_elements ++ Rendering.text_color_elements +
         Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
       entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
         Markup.CLASS, Markup.LOCALE, Markup.FREE))
 
   val elements2: Elements =
     Elements(
       html = elements1.html ++ Rendering.markdown_elements,
       language = Markup.Elements(Markup.Language.DOCUMENT))
 
 
   /* formal entities */
 
   type Entity = Export_Theory.Entity[Export_Theory.No_Content]
 
   object Entity_Context
   {
     object Theory_Ref
     {
       def unapply(props: Properties.T): Option[Document.Node.Name] =
         (props, props, props) match {
           case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) =>
             Some(Resources.file_node(Path.explode(thy_file), theory = theory))
           case _ => None
         }
     }
 
     object Entity_Ref
     {
       def unapply(props: Properties.T): Option[(Path, Option[String], String, String)] =
         (props, props, props, props) match {
-          case (Markup.Ref(_), Position.Def_File(def_file), Markup.Kind(kind), Markup.Name(name)) =>
+          case (Markup.Entity.Ref.Prop(_), Position.Def_File(def_file),
+              Markup.Kind(kind), Markup.Name(name)) =>
             val def_theory = Position.Def_Theory.unapply(props)
             Some((Path.explode(def_file), def_theory, kind, name))
           case _ => None
         }
     }
 
     val empty: Entity_Context = new Entity_Context
 
     def make(
         session: String,
         deps: Sessions.Deps,
         node: Document.Node.Name,
         theory_exports: Map[String, Export_Theory.Theory]): Entity_Context =
       new Entity_Context {
         private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
 
         override def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] =
         {
           body match {
             case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
             case _ =>
               Some {
                 val entities =
                   theory_exports.get(node.theory).flatMap(_.entity_by_range.get(range))
                     .getOrElse(Nil)
                 val body1 =
                   if (seen_ranges.contains(range)) {
                     HTML.entity_def(HTML.span(HTML.id(offset_id(range)), body))
                   }
                   else HTML.span(body)
                 entities.map(_.kname).foldLeft(body1) {
                   case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
                 }
               }
           }
         }
 
         private def offset_id(range: Text.Range): String =
           "offset_" + range.start + ".." + range.stop
 
         private def physical_ref(thy_name: String, props: Properties.T): Option[String] =
         {
           for {
             range <- Position.Def_Range.unapply(props)
             if thy_name == node.theory
           } yield {
             seen_ranges += range
             offset_id(range)
           }
         }
 
         private def logical_ref(thy_name: String, kind: String, name: String): Option[String] =
           for {
             thy <- theory_exports.get(thy_name)
             entity <- thy.entity_by_kind_name.get((kind, name))
           } yield entity.kname
 
         override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
         {
           props match {
             case Theory_Ref(node_name) =>
               node_relative(deps, session, node_name).map(html_dir =>
                 HTML.link(html_dir + html_name(node_name), body))
             case Entity_Ref(file_path, def_theory, kind, name) =>
               for {
                 thy_name <-
                   def_theory orElse (if (File.eq(node.path, file_path)) Some(node.theory) else None)
                 node_name = Resources.file_node(file_path, theory = thy_name)
                 html_dir <- node_relative(deps, session, node_name)
                 html_file = node_file(node_name)
                 html_ref <-
                   logical_ref(thy_name, kind, name) orElse physical_ref(thy_name, props)
               } yield {
                 HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
               }
             case _ => None
           }
         }
       }
   }
 
   class Entity_Context
   {
     def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = None
     def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = None
   }
 
 
   /* HTML output */
 
   private val div_elements =
     Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
       HTML.descr.name)
 
   def make_html(
     entity_context: Entity_Context,
     elements: Elements,
     xml: XML.Body): XML.Body =
   {
     def html_div(html: XML.Body): Boolean =
       html exists {
         case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
         case XML.Text(_) => false
       }
 
     def html_class(c: String, html: XML.Body): XML.Body =
       if (c == "") html
       else if (html_div(html)) List(HTML.div(c, html))
       else List(HTML.span(c, html))
 
     def html_body(xml_body: XML.Body, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
       xml_body.foldRight((List.empty[XML.Tree], end_offset)) { case (tree, (res, end_offset1)) =>
         val (res1, offset) = html_body_single(tree, end_offset1)
         (res1 ++ res, offset)
       }
 
     @tailrec
     def html_body_single(xml_tree: XML.Tree, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
       xml_tree match {
         case XML.Wrapped_Elem(markup, _, body) => html_body_single(XML.Elem(markup, body), end_offset)
         case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
           val (body1, offset) = html_body(body, end_offset)
           if (elements.entity(kind)) {
             entity_context.make_ref(props, body1) match {
               case Some(link) => (List(link), offset)
               case None => (body1, offset)
             }
           }
           else (body1, offset)
         case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) =>
           val (body1, offset) = html_body(body, end_offset)
           (html_class(if (elements.language(name)) name else "", body1), offset)
         case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) =>
           val (body1, offset) = html_body(body, end_offset)
           (List(HTML.par(body1)), offset)
         case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) =>
           val (body1, offset) = html_body(body, end_offset)
           (List(HTML.item(body1)), offset)
         case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), text) =>
           (Nil, end_offset - XML.symbol_length(text))
         case XML.Elem(Markup.Markdown_List(kind), body) =>
           val (body1, offset) = html_body(body, end_offset)
           if (kind == Markup.ENUMERATE) (List(HTML.enum(body1)), offset)
           else (List(HTML.list(body1)), offset)
         case XML.Elem(markup, body) =>
           val name = markup.name
           val (body1, offset) = html_body(body, end_offset)
           val html =
             markup.properties match {
               case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
                 html_class(kind, body1)
               case _ =>
                 body1
             }
           Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
             case Some(c) => (html_class(c.toString, html), offset)
             case None => (html_class(name, html), offset)
           }
         case XML.Text(text) =>
           val offset = end_offset - Symbol.length(text)
           val body = HTML.text(Symbol.decode(text))
           entity_context.make_def(Text.Range(offset, end_offset), body) match {
             case Some(body1) => (List(body1), offset)
             case None => (body, offset)
           }
       }
 
     html_body(xml, XML.symbol_length(xml) + 1)._1
   }
 
 
   /* PIDE HTML document */
 
   def html_document(
     snapshot: Document.Snapshot,
     html_context: HTML_Context,
     elements: Elements,
     plain_text: Boolean = false,
     fonts_css: String = HTML.fonts_css()): HTML_Document =
   {
     require(!snapshot.is_outdated, "document snapshot outdated")
 
     val name = snapshot.node_name
     if (plain_text) {
       val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
       val body = HTML.text(snapshot.node.source)
       html_context.html_document(title, body, fonts_css)
     }
     else {
       Resources.html_document(snapshot) getOrElse {
         val title =
           if (name.is_theory) "Theory " + quote(name.theory_base_name)
           else "File " + Symbol.cartouche_decoded(name.path.file_name)
         val xml = snapshot.xml_markup(elements = elements.html)
         val body = make_html(Entity_Context.empty, elements, xml)
         html_context.html_document(title, body, fonts_css)
       }
     }
   }
 
 
 
   /** HTML presentation **/
 
   /* presentation context */
 
   object Context
   {
     val none: Context = new Context { def enabled: Boolean = false }
     val standard: Context = new Context { def enabled: Boolean = true }
 
     def dir(path: Path): Context =
       new Context {
         def enabled: Boolean = true
         override def dir(store: Sessions.Store): Path = path
       }
 
     def make(s: String): Context =
       if (s == ":") standard else dir(Path.explode(s))
   }
 
   abstract class Context private
   {
     def enabled: Boolean
     def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info
     def dir(store: Sessions.Store): Path = store.presentation_dir
     def dir(store: Sessions.Store, info: Sessions.Info): Path =
       dir(store) + Path.explode(info.chapter_session)
   }
 
 
   /* maintain chapter index */
 
   private val sessions_path = Path.basic(".sessions")
 
   private def read_sessions(dir: Path): List[(String, String)] =
   {
     val path = dir + sessions_path
     if (path.is_file) {
       import XML.Decode._
       list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
     }
     else Nil
   }
 
   def update_chapter(
     presentation_dir: Path, chapter: String, new_sessions: List[(String, String)]): Unit =
   {
     val dir = Isabelle_System.make_directory(presentation_dir + Path.basic(chapter))
 
     val sessions0 =
       try { read_sessions(dir) }
       catch { case _: XML.Error => Nil }
 
     val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
     File.write(dir + sessions_path,
       {
         import XML.Encode._
         YXML.string_of_body(list(pair(string, string))(sessions))
       })
 
     val title = "Isabelle/" + chapter + " sessions"
     HTML.write_document(dir, "index.html",
       List(HTML.title(title + Isabelle_System.isabelle_heading())),
       HTML.chapter(title) ::
        (if (sessions.isEmpty) Nil
         else
           List(HTML.div("sessions",
             List(HTML.description(
               sessions.map({ case (name, description) =>
                 val descr = Symbol.trim_blank_lines(description)
                 (List(HTML.link(name + "/index.html", HTML.text(name))),
                   if (descr == "") Nil
                   else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))),
       base = Some(presentation_dir))
   }
 
   def update_root(presentation_dir: Path): Unit =
   {
     Isabelle_System.make_directory(presentation_dir)
     HTML.init_fonts(presentation_dir)
     Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
       presentation_dir + Path.explode("isabelle.gif"))
     val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library"
     File.write(presentation_dir + Path.explode("index.html"),
       HTML.header +
 """
 <head>
   """ + HTML.head_meta + """
   <title>""" + title + """</title>
 </head>
 
 <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
   <center>
     <table width="100%" border="0" cellspacing="10" cellpadding="0">
       <tr>
         <td width="20%" valign="middle" align="center"><a href="https://isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></td>
 
         <td width="80%" valign="middle" align="center">
           <table width="90%" border="0" cellspacing="0" cellpadding="20">
             <tr>
               <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">""" + title + """</font></td>
             </tr>
           </table>
         </td>
       </tr>
     </table>
   </center>
   <hr />
 """ + File.read(Path.explode("~~/lib/html/library_index_content.template")) +
 """
 </body>
 """ + HTML.footer)
   }
 
 
   /* present session */
 
   val session_graph_path = Path.explode("session_graph.pdf")
   val readme_path = Path.explode("README.html")
 
   def html_name(name: Document.Node.Name): String = Path.explode(name.theory_base_name).html.implode
   def files_path(src_path: Path): String = (Path.explode("files") + src_path.squash.html).implode
 
   private def node_file(name: Document.Node.Name): String =
     if (name.node.endsWith(".thy")) html_name(name) else files_path(name.path)
 
   private def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] =
   {
     for {
       info0 <- deps.sessions_structure.get(session0)
       info1 <- deps.sessions_structure.get(session1)
     } yield info0.relative_path(info1)
   }
 
   def node_relative(
     deps: Sessions.Deps,
     session0: String,
     node_name: Document.Node.Name): Option[String] =
   {
     val session1 = deps(session0).theory_qualifier(node_name)
     session_relative(deps, session0, session1)
   }
 
   def theory_link(deps: Sessions.Deps, session0: String,
     name: Document.Node.Name, body: XML.Body, anchor: Option[String] = None): Option[XML.Tree] =
   {
     val session1 = deps(session0).theory_qualifier(name)
     val info0 = deps.sessions_structure.get(session0)
     val info1 = deps.sessions_structure.get(session1)
     val fragment = if (anchor.isDefined) "#" + anchor.get else ""
     if (info0.isDefined && info1.isDefined) {
       Some(HTML.link(info0.get.relative_path(info1.get) + html_name(name) + fragment, body))
     }
     else None
   }
 
   def session_html(
     session: String,
     deps: Sessions.Deps,
     db_context: Sessions.Database_Context,
     progress: Progress = new Progress,
     verbose: Boolean = false,
     html_context: HTML_Context,
     session_elements: Elements): Unit =
   {
     val hierarchy = deps.sessions_structure.hierarchy(session)
     val info = deps.sessions_structure(session)
     val options = info.options
     val base = deps(session)
 
     val session_dir = Isabelle_System.make_directory(html_context.session_dir(info))
 
     Bytes.write(session_dir + session_graph_path,
       graphview.Graph_File.make_pdf(options, base.session_graph_display))
 
     val documents =
       for {
         doc <- info.document_variants
         document <- db_context.input_database(session)(Document_Build.read_document(_, _, doc.name))
       } yield {
         val doc_path = (session_dir + doc.path.pdf).expand
         if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
         if (options.bool("document_echo")) progress.echo("Document at " + doc_path)
         Bytes.write(doc_path, document.pdf)
         doc
       }
 
     val view_links =
     {
       val deps_link =
         HTML.link(session_graph_path, HTML.text("theory dependencies"))
 
       val readme_links =
         if ((info.dir + readme_path).is_file) {
           Isabelle_System.copy_file(info.dir + readme_path, session_dir + readme_path)
           List(HTML.link(readme_path, HTML.text("README")))
         }
         else Nil
 
       val document_links =
         documents.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name)))
 
       Library.separate(HTML.break ::: HTML.nl,
         (deps_link :: readme_links ::: document_links).
           map(link => HTML.text("View ") ::: List(link))).flatten
     }
 
     val all_used_theories = hierarchy.reverse.flatMap(a => deps(a).used_theories.map(_._1))
     val present_theories = html_context.register_presented(all_used_theories)
 
     val theory_exports: Map[String, Export_Theory.Theory] =
       (for (node <- all_used_theories.iterator) yield {
         val thy_name = node.theory
         val theory =
           if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
           else {
             html_context.cache_theory(thy_name,
               {
                 val provider = Export.Provider.database_context(db_context, hierarchy, thy_name)
                 if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
                   Export_Theory.read_theory(
                     provider, session, thy_name, cache = html_context.cache)
                 }
                 else Export_Theory.no_theory
               })
         }
         thy_name -> theory
       }).toMap
 
     def entity_context(name: Document.Node.Name): Entity_Context =
       Entity_Context.make(session, deps, name, theory_exports)
 
     val theories: List[XML.Body] =
     {
       sealed case class Seen_File(
         src_path: Path, thy_name: Document.Node.Name, thy_session: String)
       {
         val files_path: Path = html_context.files_path(thy_name, src_path)
 
         def check(src_path1: Path, thy_name1: Document.Node.Name, thy_session1: String): Boolean =
         {
           val files_path1 = html_context.files_path(thy_name1, src_path1)
           (src_path == src_path1 || files_path == files_path1) && thy_session == thy_session1
         }
       }
       var seen_files = List.empty[Seen_File]
 
       sealed case class Theory(
         name: Document.Node.Name,
         command: Command,
         files_html: List[(Path, XML.Tree)],
         html: XML.Tree)
 
       def read_theory(name: Document.Node.Name): Option[Theory] =
       {
         progress.expose_interrupt()
 
         for (command <- Build_Job.read_theory(db_context, hierarchy, name.theory))
         yield {
           if (verbose) progress.echo("Presenting theory " + name)
           val snapshot = Document.State.init.snippet(command)
 
           val thy_elements =
             session_elements.copy(entity =
               theory_exports(name.theory).others.keySet.foldLeft(session_elements.entity)(_ + _))
 
           val files_html =
             for {
               (src_path, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html)
               if xml.nonEmpty
             }
             yield {
               progress.expose_interrupt()
               if (verbose) progress.echo("Presenting file " + src_path)
 
               (src_path, html_context.source(
                 make_html(entity_context(name), thy_elements, xml)))
             }
 
           val html =
             html_context.source(
               make_html(entity_context(name), thy_elements,
                 snapshot.xml_markup(elements = thy_elements.html)))
 
           Theory(name, command, files_html, html)
         }
       }
 
       (for (thy <- Par_List.map(read_theory, present_theories).flatten) yield {
         val thy_session = html_context.theory_session(thy.name)
         val thy_dir = Isabelle_System.make_directory(html_context.session_dir(thy_session))
         val files =
           for { (src_path, file_html) <- thy.files_html }
           yield {
             seen_files.find(_.check(src_path, thy.name, thy_session.name)) match {
               case None => seen_files ::= Seen_File(src_path, thy.name, thy_session.name)
               case Some(seen_file) =>
                 error("Incoherent use of file name " + src_path + " as " + files_path(src_path) +
                   " in theory " + seen_file.thy_name + " vs. " + thy.name)
             }
 
             val file_path = html_context.files_path(thy.name, src_path)
             val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
             HTML.write_document(file_path.dir, file_path.file_name,
               List(HTML.title(file_title)), List(html_context.head(file_title), file_html),
               base = Some(html_context.root_dir))
 
             List(HTML.link(files_path(src_path), HTML.text(file_title)))
           }
 
         val thy_title = "Theory " + thy.name.theory_base_name
 
         HTML.write_document(thy_dir, html_name(thy.name),
           List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html),
           base = Some(html_context.root_dir))
 
         if (thy_session.name == session) {
           Some(
             List(HTML.link(html_name(thy.name),
               HTML.text(thy.name.theory_base_name) :::
                 (if (files.isEmpty) Nil else List(HTML.itemize(files))))))
         }
         else None
       }).flatten
     }
 
     val title = "Session " + session
     HTML.write_document(session_dir, "index.html",
       List(HTML.title(title + Isabelle_System.isabelle_heading())),
       html_context.head(title, List(HTML.par(view_links))) ::
         html_context.contents("Theories", theories),
       base = Some(html_context.root_dir))
   }
 }
diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala
+++ b/src/Pure/Tools/build.scala
@@ -1,690 +1,690 @@
 /*  Title:      Pure/Tools/build.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 Build and manage Isabelle sessions.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.SortedSet
 import scala.annotation.tailrec
 
 
 object Build
 {
   /** auxiliary **/
 
   /* persistent build info */
 
   sealed case class Session_Info(
     sources: String,
     input_heaps: List[String],
     output_heap: Option[String],
     return_code: Int)
   {
     def ok: Boolean = return_code == 0
   }
 
 
   /* queue with scheduling information */
 
   private object Queue
   {
     type Timings = (List[Properties.T], Double)
 
     def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings =
     {
       val no_timings: Timings = (Nil, 0.0)
 
       store.try_open_database(session_name) match {
         case None => no_timings
         case Some(db) =>
           def ignore_error(msg: String) =
           {
             progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
             no_timings
           }
           try {
             val command_timings = store.read_command_timings(db, session_name)
             val session_timing =
               store.read_session_timing(db, session_name) match {
                 case Markup.Elapsed(t) => t
                 case _ => 0.0
               }
             (command_timings, session_timing)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
             case exn: java.lang.Error => ignore_error(Exn.message(exn))
             case _: XML.Error => ignore_error("")
           }
           finally { db.close() }
       }
     }
 
     def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
       : Map[String, Double] =
     {
       val maximals = sessions_structure.build_graph.maximals.toSet
       def desc_timing(session_name: String): Double =
       {
         if (maximals.contains(session_name)) timing(session_name)
         else {
           val descendants = sessions_structure.build_descendants(List(session_name)).toSet
           val g = sessions_structure.build_graph.restrict(descendants)
           (0.0 :: g.maximals.flatMap(desc => {
             val ps = g.all_preds(List(desc))
             if (ps.exists(p => !timing.isDefinedAt(p))) None
             else Some(ps.map(timing(_)).sum)
           })).max
         }
       }
       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
     }
 
     def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
       : Queue =
     {
       val graph = sessions_structure.build_graph
       val names = graph.keys
 
       val timings = names.map(name => (name, load_timings(progress, store, name)))
       val command_timings =
         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
       val session_timing =
         make_session_timing(sessions_structure,
           timings.map({ case (name, (_, t)) => (name, t) }).toMap)
 
       object Ordering extends scala.math.Ordering[String]
       {
         def compare(name1: String, name2: String): Int =
           session_timing(name2) compare session_timing(name1) match {
             case 0 =>
               sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
                 case 0 => name1 compare name2
                 case ord => ord
               }
             case ord => ord
           }
       }
 
       new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
     }
   }
 
   private class Queue(
     graph: Graph[String, Sessions.Info],
     order: SortedSet[String],
     val command_timings: String => List[Properties.T])
   {
     def is_inner(name: String): Boolean = !graph.is_maximal(name)
 
     def is_empty: Boolean = graph.is_empty
 
     def - (name: String): Queue =
       new Queue(graph.del_node(name), order - name, command_timings)
 
     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
     {
       val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
       if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
       else None
     }
   }
 
 
 
   /** build with results **/
 
   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   {
     def sessions: Set[String] = results.keySet
     def infos: List[Sessions.Info] = results.values.map(_._2).toList
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
     def get_info(name: String): Option[Sessions.Info] = results.get(name).map(_._2)
     def info(name: String): Sessions.Info = get_info(name).get
     val rc: Int =
       results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
         foldLeft(Process_Result.RC.ok)(_ max _)
     def ok: Boolean = rc == Process_Result.RC.ok
 
     override def toString: String = rc.toString
   }
 
   def session_finished(session_name: String, process_result: Process_Result): String =
     "Finished " + session_name + " (" + process_result.timing.message_resources + ")"
 
   def session_timing(session_name: String, build_log: Build_Log.Session_Info): String =
   {
     val props = build_log.session_timing
     val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
-    val timing = Markup.Timing_Properties.parse(props)
+    val timing = Markup.Timing_Properties.get(props)
     "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
   }
 
   def build(
     options: Options,
     selection: Sessions.Selection = Sessions.Selection.empty,
     presentation: Presentation.Context = Presentation.Context.none,
     progress: Progress = new Progress,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     infos: List[Sessions.Info] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     soft_build: Boolean = false,
     verbose: Boolean = false,
     export_files: Boolean = false,
     session_setup: (String, Session) => Unit = (_, _) => ()): Results =
   {
     val build_options =
       options +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
         "kodkod_scala=false" +
         ("pide_reports=" + options.bool("build_pide_reports"))
 
     val store = Sessions.store(build_options)
 
     Isabelle_Fonts.init()
 
 
     /* session selection and dependencies */
 
     val full_sessions =
       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
 
     val full_sessions_selection = full_sessions.imports_selection(selection)
 
     def sources_stamp(deps: Sessions.Deps, session_name: String): String =
     {
       val digests =
         full_sessions(session_name).meta_digest ::
         deps.sources(session_name) :::
         deps.imported_sources(session_name)
       SHA1.digest_set(digests).toString
     }
 
     val deps =
     {
       val deps0 =
         Sessions.deps(full_sessions.selection(selection),
           progress = progress, inlined_files = true, verbose = verbose,
           list_files = list_files, check_keywords = check_keywords).check_errors
 
       if (soft_build && !fresh_build) {
         val outdated =
           deps0.sessions_structure.build_topological_order.flatMap(name =>
             store.try_open_database(name) match {
               case Some(db) =>
                 using(db)(store.read_build(_, name)) match {
                   case Some(build)
                   if build.ok && build.sources == sources_stamp(deps0, name) => None
                   case _ => Some(name)
                 }
               case None => Some(name)
             })
 
         Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
           progress = progress, inlined_files = true).check_errors
       }
       else deps0
     }
 
 
     /* check unknown files */
 
     if (check_unknown_files) {
       val source_files =
         (for {
           (_, base) <- deps.session_bases.iterator
           (path, _) <- base.sources.iterator
         } yield path).toList
       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
       val unknown_files =
         Mercurial.check_files(source_files)._2.
           filterNot(path => exclude_files.contains(path.canonical_file))
       if (unknown_files.nonEmpty) {
         progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
       }
     }
 
 
     /* main build process */
 
     val queue = Queue(progress, deps.sessions_structure, store)
 
     store.prepare_output_dir()
 
     if (clean_build) {
       for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
         val (relevant, ok) = store.clean_output(name)
         if (relevant) {
           if (ok) progress.echo("Cleaned " + name)
           else progress.echo(name + " FAILED to clean")
         }
       }
     }
 
     // scheduler loop
     case class Result(
       current: Boolean,
       heap_digest: Option[String],
       process: Option[Process_Result],
       info: Sessions.Info)
     {
       def ok: Boolean =
         process match {
           case None => false
           case Some(res) => res.ok
         }
     }
 
     def sleep(): Unit =
       Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep() }
 
     val log =
       build_options.string("system_log") match {
         case "" => No_Logger
         case "true" => Logger.make(progress)
         case log_file => Logger.make(Some(Path.explode(log_file)))
       }
 
     val numa_nodes = new NUMA.Nodes(numa_shuffling)
 
     @tailrec def loop(
       pending: Queue,
       running: Map[String, (List[String], Build_Job)],
       results: Map[String, Result]): Map[String, Result] =
     {
       def used_node(i: Int): Boolean =
         running.iterator.exists(
           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
 
       if (pending.is_empty) results
       else {
         if (progress.stopped) {
           for ((_, (_, job)) <- running) job.terminate()
         }
 
         running.find({ case (_, (_, job)) => job.is_finished }) match {
           case Some((session_name, (input_heaps, job))) =>
             //{{{ finish job
 
             val (process_result, heap_digest) = job.join
 
             val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
             val process_result_tail =
             {
               val tail = job.info.options.int("process_output_tail")
               process_result.copy(
                 out_lines =
                   "(see also " + store.output_log(session_name).file.toString + ")" ::
                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
             }
 
             val build_log =
               Build_Log.Log_File(session_name, process_result.out_lines).
                 parse_session_info(
                   command_timings = true,
                   theory_timings = true,
                   ml_statistics = true,
                   task_statistics = true)
 
             // write log file
             if (process_result.ok) {
               File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
             }
             else File.write(store.output_log(session_name), terminate_lines(log_lines))
 
             // write database
             using(store.open_database(session_name, output = true))(db =>
               store.write_session_info(db, session_name,
                 build_log =
                   if (process_result.timeout) build_log.error("Timeout") else build_log,
                 build =
                   Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
                     process_result.rc)))
 
             // messages
             process_result.err_lines.foreach(progress.echo)
 
             if (process_result.ok) {
               if (verbose) progress.echo(session_timing(session_name, build_log))
               progress.echo(session_finished(session_name, process_result))
             }
             else {
               progress.echo(session_name + " FAILED")
               if (!process_result.interrupted) progress.echo(process_result_tail.out)
             }
 
             loop(pending - session_name, running - session_name,
               results +
                 (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job
             pending.dequeue(running.isDefinedAt) match {
               case Some((session_name, info)) =>
                 val ancestor_results =
                   deps.sessions_structure.build_requirements(List(session_name)).
                     filterNot(_ == session_name).map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
 
                 val do_store =
                   build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
 
                 val (current, heap_digest) =
                 {
                   store.try_open_database(session_name) match {
                     case Some(db) =>
                       using(db)(store.read_build(_, session_name)) match {
                         case Some(build) =>
                           val heap_digest = store.find_heap_digest(session_name)
                           val current =
                             !fresh_build &&
                             build.ok &&
                             build.sources == sources_stamp(deps, session_name) &&
                             build.input_heaps == ancestor_heaps &&
                             build.output_heap == heap_digest &&
                             !(do_store && heap_digest.isEmpty)
                           (current, heap_digest)
                         case None => (false, None)
                       }
                     case None => (false, None)
                   }
                 }
                 val all_current = current && ancestor_results.forall(_.current)
 
                 if (all_current)
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
                 else if (no_build) {
                   progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
 
                   store.clean_output(session_name)
                   using(store.open_database(session_name, output = true))(
                     store.init_session_info(_, session_name))
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
                     new Build_Job(progress, session_name, info, deps, store, do_store,
                       log, session_setup, numa_node, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
                 else {
                   progress.echo(session_name + " CANCELLED")
                   loop(pending - session_name, running,
                     results + (session_name -> Result(false, heap_digest, None, info)))
                 }
               case None => sleep(); loop(pending, running, results)
             }
             ///}}}
           case None => sleep(); loop(pending, running, results)
         }
       }
     }
 
 
     /* build results */
 
     val results =
     {
       val results0 =
         if (deps.is_empty) {
           progress.echo_warning("Nothing to build")
           Map.empty[String, Result]
         }
         else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
 
       new Results(
         (for ((name, result) <- results0.iterator)
           yield (name, (result.process, result.info))).toMap)
     }
 
     if (export_files) {
       for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
         val info = results.info(name)
         if (info.export_files.nonEmpty) {
           progress.echo("Exporting " + info.name + " ...")
           for ((dir, prune, pats) <- info.export_files) {
             Export.export_files(store, name, info.dir + dir,
               progress = if (verbose) progress else new Progress,
               export_prune = prune,
               export_patterns = pats)
           }
         }
       }
     }
 
     if (results.rc != Process_Result.RC.ok && (verbose || !no_build)) {
       val unfinished =
         (for {
           name <- results.sessions.iterator
           if !results(name).ok
          } yield name).toList.sorted
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }
 
 
     /* PDF/HTML presentation */
 
     if (!no_build && !progress.stopped && results.ok) {
       val selected = full_sessions_selection.toSet
       val presentation_sessions =
         (for {
           session_name <- deps.sessions_structure.imports_topological_order.iterator
           info <- results.get_info(session_name)
           if selected(session_name) && presentation.enabled(info) && results(session_name).ok }
         yield info).toList
 
       if (presentation_sessions.nonEmpty) {
         val presentation_dir = presentation.dir(store)
         progress.echo("Presentation in " + presentation_dir.absolute)
         Presentation.update_root(presentation_dir)
 
         for ((chapter, infos) <- presentation_sessions.groupBy(_.chapter).iterator) {
           val entries = infos.map(info => (info.name, info.description))
           Presentation.update_chapter(presentation_dir, chapter, entries)
         }
 
         using(store.open_database_context())(db_context =>
           for (session <- presentation_sessions.map(_.name)) {
             progress.expose_interrupt()
             progress.echo("Presenting " + session + " ...")
 
             val html_context =
               new Presentation.HTML_Context {
                 override val cache: Term.Cache = store.cache
                 override def root_dir: Path = presentation_dir
                 override def theory_session(name: Document.Node.Name): Sessions.Info =
                   deps.sessions_structure(deps(session).theory_qualifier(name))
               }
             Presentation.session_html(
               session, deps, db_context, progress = progress,
               verbose = verbose, html_context = html_context,
               Presentation.elements1)
           })
       }
     }
 
     results
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions",
     Scala_Project.here, args =>
   {
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
     var numa_shuffling = false
     var presentation = Presentation.Context.none
     var requirements = false
     var soft_build = false
     var exclude_session_groups: List[String] = Nil
     var all_sessions = false
     var build_heap = false
     var clean_build = false
     var dirs: List[Path] = Nil
     var export_files = false
     var fresh_build = false
     var session_groups: List[String] = Nil
     var max_jobs = 1
     var check_keywords: Set[String] = Set.empty
     var list_files = false
     var no_build = false
     var options = Options.init(opts = build_options)
     var verbose = false
     var exclude_sessions: List[String] = Nil
 
     val getopts = Getopts("""
 Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -R           refer to requirements of selected sessions
     -S           soft build: only observe changes of sources, not heap images
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -b           build heap images
     -c           clean build
     -d DIR       include session directory
     -e           export files from session specification into file-system
     -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -k KEYWORD   check theory sources for conflicts with proposed keywords
     -l           list session source files
     -n           no build -- test dependencies only
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
   Build and manage Isabelle sessions, depending on implicit settings:
 
 """ + Library.indent_lines(2,  Build_Log.Settings.show()) + "\n",
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "N" -> (_ => numa_shuffling = true),
       "P:" -> (arg => presentation = Presentation.Context.make(arg)),
       "R" -> (_ => requirements = true),
       "S" -> (_ => soft_build = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
       "b" -> (_ => build_heap = true),
       "c" -> (_ => clean_build = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "e" -> (_ => export_files = true),
       "f" -> (_ => fresh_build = true),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
       "k:" -> (arg => check_keywords = check_keywords + arg),
       "l" -> (_ => list_files = true),
       "n" -> (_ => no_build = true),
       "o:" -> (arg => options = options + arg),
       "v" -> (_ => verbose = true),
       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
     val sessions = getopts(args)
 
     val progress = new Console_Progress(verbose = verbose)
 
     val start_date = Date.now()
 
     if (verbose) {
       progress.echo(
         "Started at " + Build_Log.print_date(start_date) +
           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
       progress.echo(Build_Log.Settings.show() + "\n")
     }
 
     val results =
       progress.interrupt_handler {
         build(options,
           selection = Sessions.Selection(
             requirements = requirements,
             all_sessions = all_sessions,
             base_sessions = base_sessions,
             exclude_session_groups = exclude_session_groups,
             exclude_sessions = exclude_sessions,
             session_groups = session_groups,
             sessions = sessions),
           presentation = presentation,
           progress = progress,
           check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
           build_heap = build_heap,
           clean_build = clean_build,
           dirs = dirs,
           select_dirs = select_dirs,
           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
           max_jobs = max_jobs,
           list_files = list_files,
           check_keywords = check_keywords,
           fresh_build = fresh_build,
           no_build = no_build,
           soft_build = soft_build,
           verbose = verbose,
           export_files = export_files)
       }
     val end_date = Date.now()
     val elapsed_time = end_date.time - start_date.time
 
     if (verbose) {
       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
     }
 
     val total_timing =
       results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
         copy(elapsed = elapsed_time)
     progress.echo(total_timing.message_resources)
 
     sys.exit(results.rc)
   })
 
 
   /* build logic image */
 
   def build_logic(options: Options, logic: String,
     progress: Progress = new Progress,
     build_heap: Boolean = false,
     dirs: List[Path] = Nil,
     fresh: Boolean = false,
     strict: Boolean = false): Int =
   {
     val selection = Sessions.Selection.session(logic)
     val rc =
       if (!fresh && build(options, selection = selection,
             build_heap = build_heap, no_build = true, dirs = dirs).ok) Process_Result.RC.ok
       else {
         progress.echo("Build started for Isabelle/" + logic + " ...")
         Build.build(options, selection = selection, progress = progress,
           build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
       }
     if (strict && rc != Process_Result.RC.ok) error("Failed to build Isabelle/" + logic) else rc
   }
 }
diff --git a/src/Tools/jEdit/src/jedit_rendering.scala b/src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala
+++ b/src/Tools/jEdit/src/jedit_rendering.scala
@@ -1,429 +1,429 @@
 /*  Title:      Tools/jEdit/src/jedit_rendering.scala
     Author:     Makarius
 
 Isabelle/jEdit-specific implementation of quasi-abstract rendering and
 markup interpretation.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.Color
 import javax.swing.Icon
 
 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
 import org.gjt.sp.jedit.jEdit
 
 import scala.collection.immutable.SortedMap
 
 
 object JEdit_Rendering
 {
   /* make rendering */
 
   def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
     new JEdit_Rendering(snapshot, model, options)
 
   def text(snapshot: Document.Snapshot, formatted_body: XML.Body,
     results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) =
   {
     val command = Command.rich_text(Document_ID.make(), results, formatted_body)
     val snippet = snapshot.snippet(command)
     val model = File_Model.empty(PIDE.session)
     val rendering = apply(snippet, model, PIDE.options.value)
     (command.source, rendering)
   }
 
 
   /* popup window bounds */
 
   def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
 
 
   /* Isabelle/Isar token markup */
 
   private val command_style: Map[String, Byte] =
   {
     import JEditToken._
     Map[String, Byte](
       Keyword.THY_END -> KEYWORD2,
       Keyword.PRF_ASM -> KEYWORD3,
       Keyword.PRF_ASM_GOAL -> KEYWORD3
     ).withDefaultValue(KEYWORD1)
   }
 
   private val token_style: Map[Token.Kind.Value, Byte] =
   {
     import JEditToken._
     Map[Token.Kind.Value, Byte](
       Token.Kind.KEYWORD -> KEYWORD2,
       Token.Kind.IDENT -> NULL,
       Token.Kind.LONG_IDENT -> NULL,
       Token.Kind.SYM_IDENT -> NULL,
       Token.Kind.VAR -> NULL,
       Token.Kind.TYPE_IDENT -> NULL,
       Token.Kind.TYPE_VAR -> NULL,
       Token.Kind.NAT -> NULL,
       Token.Kind.FLOAT -> NULL,
       Token.Kind.SPACE -> NULL,
       Token.Kind.STRING -> LITERAL1,
       Token.Kind.ALT_STRING -> LITERAL2,
       Token.Kind.VERBATIM -> COMMENT3,
       Token.Kind.CARTOUCHE -> COMMENT3,
       Token.Kind.CONTROL -> COMMENT3,
       Token.Kind.INFORMAL_COMMENT -> COMMENT1,
       Token.Kind.FORMAL_COMMENT -> COMMENT1,
       Token.Kind.ERROR -> INVALID
     ).withDefaultValue(NULL)
   }
 
   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
     if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
     else if (token.is_delimiter) JEditToken.OPERATOR
     else token_style(token.kind)
 
 
   /* Isabelle/ML token markup */
 
   private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
   {
     import JEditToken._
     Map[ML_Lex.Kind.Value, Byte](
       ML_Lex.Kind.KEYWORD -> NULL,
       ML_Lex.Kind.IDENT -> NULL,
       ML_Lex.Kind.LONG_IDENT -> NULL,
       ML_Lex.Kind.TYPE_VAR -> NULL,
       ML_Lex.Kind.WORD -> DIGIT,
       ML_Lex.Kind.INT -> DIGIT,
       ML_Lex.Kind.REAL -> DIGIT,
       ML_Lex.Kind.CHAR -> LITERAL2,
       ML_Lex.Kind.STRING -> LITERAL1,
       ML_Lex.Kind.SPACE -> NULL,
       ML_Lex.Kind.INFORMAL_COMMENT -> COMMENT1,
       ML_Lex.Kind.FORMAL_COMMENT -> COMMENT1,
       ML_Lex.Kind.ANTIQ -> NULL,
       ML_Lex.Kind.ANTIQ_START -> LITERAL4,
       ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
       ML_Lex.Kind.ANTIQ_OTHER -> NULL,
       ML_Lex.Kind.ANTIQ_STRING -> NULL,
       ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL,
       ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL,
       ML_Lex.Kind.ERROR -> INVALID
     ).withDefaultValue(NULL)
   }
 
   def ml_token_markup(token: ML_Lex.Token): Byte =
     if (!token.is_keyword) ml_token_style(token.kind)
     else if (token.is_delimiter) JEditToken.OPERATOR
     else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
     else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
     else JEditToken.KEYWORD1
 
 
   /* markup elements */
 
   private val indentation_elements =
     Markup.Elements(Markup.Command_Indent.name)
 
   private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
 
   private val highlight_elements =
     Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL,
       Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM,
       Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
       Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
 
   private val hyperlink_elements =
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.EXPORT_PATH, Markup.DOC, Markup.URL,
       Markup.POSITION, Markup.CITATION)
 
   private val gutter_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
 
   private val squiggly_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
 
   private val line_background_elements =
     Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE,
       Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE,
       Markup.ERROR_MESSAGE)
 
   private val separator_elements =
     Markup.Elements(Markup.SEPARATOR)
 
   private val bullet_elements =
     Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT)
 
   private val fold_depth_elements =
     Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
 }
 
 
 class JEdit_Rendering(snapshot: Document.Snapshot, model: Document_Model, options: Options)
   extends Rendering(snapshot, options, PIDE.session)
 {
   override def get_text(range: Text.Range): Option[String] = model.get_text(range)
 
 
   /* colors */
 
   def color(s: String): Color =
     if (s == "main_color") main_color
     else Color_Value(options.string(s))
 
   def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
 
   lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
     Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap
 
   val main_color = jEdit.getColorProperty("view.fgColor")
 
   val outdated_color = color("outdated_color")
   val bullet_color = color("bullet_color")
   val tooltip_color = color("tooltip_color")
   val spell_checker_color = color("spell_checker_color")
   val entity_ref_color = color("entity_ref_color")
   val breakpoint_disabled_color = color("breakpoint_disabled_color")
   val breakpoint_enabled_color = color("breakpoint_enabled_color")
   val caret_debugger_color = color("caret_debugger_color")
   val highlight_color = color("highlight_color")
   val hyperlink_color = color("hyperlink_color")
   val active_hover_color = color("active_hover_color")
   val caret_invisible_color = color("caret_invisible_color")
   val completion_color = color("completion_color")
   val search_color = color("search_color")
 
 
   /* indentation */
 
   def indentation(range: Text.Range): Int =
     snapshot.select(range, JEdit_Rendering.indentation_elements, _ =>
       {
         case Text.Info(_, XML.Elem(Markup.Command_Indent(i), _)) => Some(i)
         case _ => None
       }).headOption.map(_.info).getOrElse(0)
 
 
   /* breakpoints */
 
   def breakpoint(range: Text.Range): Option[(Command, Long)] =
     if (snapshot.is_outdated) None
     else
       snapshot.select(range, JEdit_Rendering.breakpoint_elements, command_states =>
         {
           case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
             command_states match {
               case st :: _ => Some((st.command, breakpoint))
               case _ => None
             }
           case _ => None
         }).headOption.map(_.info)
 
 
   /* caret focus */
 
   def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
     snapshot.select(range, Rendering.entity_elements, _ =>
       {
-        case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Ref(i)), _))
-        if focus(i) => Some(entity_ref_color)
+        case Text.Info(_, XML.Elem(Markup.Entity.Ref(i), _)) if focus(i) =>
+          Some(entity_ref_color)
         case _ => None
       })
 
 
   /* highlighted area */
 
   def highlight(range: Text.Range): Option[Text.Info[Color]] =
     snapshot.select(range, JEdit_Rendering.highlight_elements, _ =>
       {
         case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
       }).headOption.map(_.info)
 
 
   /* hyperlinks */
 
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
     snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
       range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
             val file = perhaps_append_file(snapshot.node_name, name)
             val link = PIDE.editor.hyperlink_file(true, file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Export_Path(name), _))) =>
             val link = PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
             PIDE.editor.hyperlink_doc(name).map(link =>
               (links :+ Text.Info(snapshot.convert(info_range), link)))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
             val link = PIDE.editor.hyperlink_url(name)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
             val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
             val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
             val opt_link =
               Document_Model.bibtex_entries_iterator().collectFirst(
                 { case Text.Info(entry_range, (entry, model)) if entry == name =>
                     PIDE.editor.hyperlink_model(true, model, entry_range.start) })
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
           case _ => None
         }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
   }
 
   def hyperlink_entity(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
     snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
       range, Vector.empty, Rendering.entity_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
             val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
           case _ => None
         }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
   }
 
 
   /* active elements */
 
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
     snapshot.select(range, Rendering.active_elements, command_states =>
       {
         case Text.Info(info_range, elem) =>
           if (elem.name == Markup.DIALOG) {
             elem match {
               case Protocol.Dialog(_, serial, _)
               if !command_states.exists(st => st.results.defined(serial)) =>
                 Some(Text.Info(snapshot.convert(info_range), elem))
               case _ => None
             }
           }
           else Some(Text.Info(snapshot.convert(info_range), elem))
       }).headOption.map(_.info)
 
 
   /* tooltips */
 
   def tooltip_margin: Int = options.int("jedit_tooltip_margin")
   override def timing_threshold: Double = options.real("jedit_timing_threshold")
 
   def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[XML.Body]] =
   {
     val elements = if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements
     tooltips(elements, range).map(info => info.map(Pretty.fbreaks))
   }
 
   lazy val tooltip_close_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   lazy val tooltip_detach_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
 
 
   /* gutter */
 
   private def gutter_message_pri(msg: XML.Tree): Int =
     if (Protocol.is_error(msg)) Rendering.error_pri
     else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
     else if (Protocol.is_warning(msg)) Rendering.warning_pri
     else if (Protocol.is_information(msg)) Rendering.information_pri
     else 0
 
   private lazy val gutter_message_content = Map(
     Rendering.information_pri ->
       (JEdit_Lib.load_icon(options.string("gutter_information_icon")),
         color(Rendering.Color.information_message)),
     Rendering.warning_pri ->
       (JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
         color(Rendering.Color.warning_message)),
     Rendering.legacy_pri ->
       (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
         color(Rendering.Color.legacy_message)),
     Rendering.error_pri ->
       (JEdit_Lib.load_icon(options.string("gutter_error_icon")),
         color(Rendering.Color.error_message)))
 
   def gutter_content(range: Text.Range): Option[(Icon, Color)] =
   {
     val pris =
       snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ =>
         {
           case (pri, Text.Info(_, elem)) => Some(pri max gutter_message_pri(elem))
           case _ => None
         }).map(_.info)
 
     gutter_message_content.get(pris.foldLeft(0)(_ max _))
   }
 
 
   /* message output */
 
   def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
     message_underline_color(JEdit_Rendering.squiggly_elements, range)
 
   def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] =
   {
     val results =
       snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ =>
         {
           case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
         })
     val pri = results.foldLeft(0) { case (p1, Text.Info(_, p2)) => p1 max p2 }
 
     Rendering.message_background_color.get(pri).map(message_color =>
       {
         val is_separator =
           snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ =>
             {
               case _ => Some(true)
             }).exists(_.info)
         (message_color, is_separator)
       })
   }
 
 
   /* text color */
 
   def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] =
   {
     if (current_color == Syntax_Style.hidden_color) List(Text.Info(range, current_color))
     else
       snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ =>
         {
           case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color)
         })
   }
 
 
   /* virtual bullets */
 
   def bullet(range: Text.Range): List[Text.Info[Color]] =
     snapshot.select(range, JEdit_Rendering.bullet_elements, _ =>
       {
         case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
           PIDE.session.debugger.active_breakpoint_state(breakpoint).map(b =>
             if (b) breakpoint_enabled_color else breakpoint_disabled_color)
         case _ => Some(bullet_color)
       })
 
 
   /* text folds */
 
   def fold_depth(range: Text.Range): List[Text.Info[Int]] =
     snapshot.cumulate[Int](range, 0, JEdit_Rendering.fold_depth_elements, _ =>
       {
         case (depth, _) => Some(depth + 1)
       })
 }