diff --git a/src/Pure/General/bytes.scala b/src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala
+++ b/src/Pure/General/bytes.scala
@@ -1,206 +1,212 @@
 /*  Title:      Pure/General/bytes.scala
     Author:     Makarius
 
 Immutable byte vectors versus UTF8 strings.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
   OutputStream, InputStream, FileInputStream, FileOutputStream}
 import java.net.URL
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
 
 object Bytes {
   val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
 
   def apply(s: CharSequence): Bytes = {
     val str = s.toString
     if (str.isEmpty) empty
     else {
       val b = UTF8.bytes(str)
       new Bytes(b, 0, b.length)
     }
   }
 
   def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length)
 
   def apply(a: Array[Byte], offset: Int, length: Int): Bytes =
     if (length == 0) empty
     else {
       val b = new Array[Byte](length)
       System.arraycopy(a, offset, b, 0, length)
       new Bytes(b, 0, b.length)
     }
 
   val newline: Bytes = apply("\n")
 
 
   /* base64 */
 
   def decode_base64(s: String): Bytes = {
     val a = Base64.decode(s)
     new Bytes(a, 0, a.length)
   }
 
 
   /* read */
 
   def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
     if (limit == 0) empty
     else {
       val out_size = (if (limit == Integer.MAX_VALUE) hint else limit) max 1024
       val out = new ByteArrayOutputStream(out_size)
       val buf = new Array[Byte](8192)
       var m = 0
 
       while ({
         m = stream.read(buf, 0, buf.length min (limit - out.size))
         if (m != -1) out.write(buf, 0, m)
         m != -1 && limit > out.size
       }) ()
 
       new Bytes(out.toByteArray, 0, out.size)
     }
 
   def read(file: JFile): Bytes = {
     val length = file.length
     val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
     using(new FileInputStream(file))(read_stream(_, limit = limit))
   }
 
   def read(path: Path): Bytes = read(path.file)
 
   def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
 
 
   /* write */
 
   def write(file: JFile, bytes: Bytes): Unit =
     using(new FileOutputStream(file))(bytes.write_stream(_))
 
   def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
 }
 
 final class Bytes private(
   protected val bytes: Array[Byte],
   protected val offset: Int,
   val length: Int) extends CharSequence {
   /* equality */
 
   override def equals(that: Any): Boolean = {
     that match {
       case other: Bytes =>
         if (this eq other) true
         else if (length != other.length) false
         else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
       case _ => false
     }
   }
 
   private lazy val hash: Int = {
     var h = 0
     for (i <- offset until offset + length) {
       val b = bytes(i).asInstanceOf[Int] & 0xFF
       h = 31 * h + b
     }
     h
   }
 
   override def hashCode(): Int = hash
 
 
   /* content */
 
   lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
   def is_empty: Boolean = length == 0
 
   def iterator: Iterator[Byte] =
     for (i <- (offset until (offset + length)).iterator)
       yield bytes(i)
 
   def array: Array[Byte] = {
     val a = new Array[Byte](length)
     System.arraycopy(bytes, offset, a, 0, length)
     a
   }
 
   def text: String = UTF8.decode_permissive(this)
 
+  def wellformed_text: Option[String] = {
+    val s = text
+    if (this == Bytes(s)) Some(s) else None
+  }
+
   def encode_base64: String = {
     val b =
       if (offset == 0 && length == bytes.length) bytes
       else Bytes(bytes, offset, length).bytes
     Base64.encode(b)
   }
 
-  def maybe_encode_base64: (Boolean, String) = {
-    val s = text
-    if (this == Bytes(s)) (false, s) else (true, encode_base64)
-  }
+  def maybe_encode_base64: (Boolean, String) =
+    wellformed_text match {
+      case Some(s) => (false, s)
+      case None => (true, encode_base64)
+    }
 
   override def toString: String = "Bytes(" + length + ")"
 
   def proper: Option[Bytes] = if (is_empty) None else Some(this)
   def proper_text: Option[String] = if (is_empty) None else Some(text)
 
   def +(other: Bytes): Bytes =
     if (other.is_empty) this
     else if (is_empty) other
     else {
       val new_bytes = new Array[Byte](length + other.length)
       System.arraycopy(bytes, offset, new_bytes, 0, length)
       System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
       new Bytes(new_bytes, 0, new_bytes.length)
     }
 
 
   /* CharSequence operations */
 
   def charAt(i: Int): Char =
     if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
     else throw new IndexOutOfBoundsException
 
   def subSequence(i: Int, j: Int): Bytes = {
     if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i)
     else throw new IndexOutOfBoundsException
   }
 
   def trim_line: Bytes =
     if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10)
       subSequence(0, length - 2)
     else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10))
       subSequence(0, length - 1)
     else this
 
 
   /* streams */
 
   def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length)
 
   def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length)
 
 
   /* XZ data compression */
 
   def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes =
     using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length))
 
   def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes = {
     val result = new ByteArrayOutputStream(length)
     using(new XZOutputStream(result, options, cache))(write_stream(_))
     new Bytes(result.toByteArray, 0, result.size)
   }
 
   def maybe_compress(
     options: XZ.Options = XZ.options(),
     cache: XZ.Cache = XZ.Cache()
   ) : (Boolean, Bytes) = {
     val compressed = compress(options = options, cache = cache)
     if (compressed.length < length) (true, compressed) else (false, this)
   }
 }
diff --git a/src/Pure/General/symbol.scala b/src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala
+++ b/src/Pure/General/symbol.scala
@@ -1,669 +1,669 @@
 /*  Title:      Pure/General/symbol.scala
     Author:     Makarius
 
 Isabelle text symbols.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 import scala.util.matching.Regex
 import scala.annotation.tailrec
 
 
 object Symbol {
   type Symbol = String
 
   // counting Isabelle symbols, starting from 1
   type Offset = Text.Offset
   type Range = Text.Range
 
 
   /* spaces */
 
   val space_char = ' '
   val space = " "
 
   private val static_spaces = space * 4000
 
   def spaces(n: Int): String = {
     require(n >= 0, "negative spaces")
     if (n < static_spaces.length) static_spaces.substring(0, n)
     else space * n
   }
 
 
   /* char symbols */
 
   private val char_symbols: Array[Symbol] =
     (0 until 0x500).iterator.map(i => new String(Array(i.toChar))).toArray
 
   def char_symbol(c: Char): String =
     if (c < char_symbols.length) char_symbols(c)
     else c.toString
 
 
   /* ASCII characters */
 
   def is_ascii_printable(c: Char): Boolean = space_char <= c && c <= '~'
 
   def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
 
   def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
 
   def is_ascii_hex(c: Char): Boolean =
     '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
 
   def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''
 
   def is_ascii_blank(c: Char): Boolean = " \t\n\u000b\f\r".contains(c)
 
   def is_ascii_line_terminator(c: Char): Boolean = "\r\n".contains(c)
 
   def is_ascii_letdig(c: Char): Boolean =
     is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)
 
   def is_ascii_identifier(s: String): Boolean =
     s.nonEmpty && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig)
 
   def ascii(c: Char): Symbol = {
     if (c > 127) error("Non-ASCII character: " + quote(c.toString))
     else char_symbol(c)
   }
 
   def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128
 
 
   /* symbol matching */
 
   def is_malformed(s: Symbol): Boolean =
     s.length match {
       case 1 =>
         val c = s(0)
         Character.isHighSurrogate(c) || Character.isLowSurrogate(c) || c == '\ufffd'
       case 2 =>
         val c1 = s(0)
         val c2 = s(1)
         !(c1 == '\r' && c2 == '\n' || Character.isSurrogatePair(c1, c2))
       case _ => !s.endsWith(">") || s == "\\<>" || s == "\\<^>"
     }
 
   def is_newline(s: Symbol): Boolean =
     s == "\n" || s == "\r" || s == "\r\n"
 
   class Matcher(text: CharSequence) {
     private def ok(i: Int): Boolean = 0 <= i && i < text.length
     private def char(i: Int): Char = if (ok(i)) text.charAt(i) else 0
     private def maybe_char(c: Char, i: Int): Int = if (char(i) == c) i + 1 else i
 
     @tailrec private def many_ascii_letdig(i: Int): Int =
       if (is_ascii_letdig(char(i))) many_ascii_letdig(i + 1) else i
     private def maybe_ascii_id(i: Int): Int =
       if (is_ascii_letter(char(i))) many_ascii_letdig(i + 1) else i
 
     def match_length(i: Int): Int = {
       val a = char(i)
       val b = char(i + 1)
 
       if (Character.isHighSurrogate(a) && Character.isLowSurrogate(b) || a == '\r' && b == '\n') 2
       else if (a == '\\' && b == '<') maybe_char('>', maybe_ascii_id(maybe_char('^', i + 2))) - i
       else if (ok(i)) 1
       else 0
     }
 
     def match_symbol(i: Int): String =
       match_length(i) match {
         case 0 => ""
         case 1 => char_symbol(text.charAt(i))
         case n => text.subSequence(i, i + n).toString
       }
   }
 
 
   /* iterator */
 
   def iterator(text: CharSequence): Iterator[Symbol] =
     new Iterator[Symbol] {
       private val matcher = new Matcher(text)
       private var i = 0
       def hasNext: Boolean = i < text.length
       def next(): Symbol = {
         val s = matcher.match_symbol(i)
         i += s.length
         s
       }
     }
 
   def explode(text: CharSequence): List[Symbol] = iterator(text).toList
 
   def length(text: CharSequence): Int = iterator(text).length
 
   def trim_blanks(text: CharSequence): String =
     Library.trim(is_blank, explode(text)).mkString
 
   def all_blank(str: String): Boolean =
     iterator(str).forall(is_blank)
 
   def trim_blank_lines(text: String): String =
     cat_lines(split_lines(text).dropWhile(all_blank).reverse.dropWhile(all_blank).reverse)
 
 
   /* decoding offsets */
 
   object Index {
     private sealed case class Entry(chr: Int, sym: Int)
 
     val empty: Index = new Index(Nil)
 
     def apply(text: CharSequence): Index = {
       val matcher = new Matcher(text)
       val buf = new mutable.ListBuffer[Entry]
       var chr = 0
       var sym = 0
       while (chr < text.length) {
         val n = matcher.match_length(chr)
         chr += n
         sym += 1
         if (n > 1) buf += Entry(chr, sym)
       }
       if (buf.isEmpty) empty else new Index(buf.toList)
     }
   }
 
   final class Index private(entries: List[Index.Entry]) {
     private val hash: Int = entries.hashCode
     private val index: Array[Index.Entry] = entries.toArray
 
     def decode(symbol_offset: Offset): Text.Offset = {
       val sym = symbol_offset - 1
       val end = index.length
       @tailrec def bisect(a: Int, b: Int): Int = {
         if (a < b) {
           val c = (a + b) / 2
           if (sym < index(c).sym) bisect(a, c)
           else if (c + 1 == end || sym < index(c + 1).sym) c
           else bisect(c + 1, b)
         }
         else -1
       }
       val i = bisect(0, end)
       if (i < 0) sym
       else index(i).chr + sym - index(i).sym
     }
     def decode(symbol_range: Range): Text.Range = symbol_range.map(decode)
 
     override def hashCode: Int = hash
     override def equals(that: Any): Boolean =
       that match {
         case other: Index => index.sameElements(other.index)
         case _ => false
       }
   }
 
 
   /* symbolic text chunks -- without actual text */
 
   object Text_Chunk {
     sealed abstract class Name
     case object Default extends Name
     case class Id(id: Document_ID.Generic) extends Name
     case class File(name: String) extends Name
 
     def apply(text: CharSequence): Text_Chunk =
-      new Text_Chunk(Text.Range(0, text.length), Index(text))
+      new Text_Chunk(Text.Range.length(text), Index(text))
   }
 
   final class Text_Chunk private(val range: Text.Range, private val index: Index) {
     override def hashCode: Int = (range, index).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Text_Chunk =>
           range == other.range &&
           index == other.index
         case _ => false
       }
 
     override def toString: String = "Text_Chunk" + range.toString
 
     def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset)
     def decode(symbol_range: Range): Text.Range = index.decode(symbol_range)
     def incorporate(symbol_range: Range): Option[Text.Range] = {
       def in(r: Range): Option[Text.Range] = {
         range.try_restrict(decode(r)) match {
           case Some(r1) if !r1.is_singularity => Some(r1)
           case _ => None
         }
       }
       in(symbol_range) orElse in(symbol_range - 1)
     }
   }
 
 
   /* recoding text */
 
   private class Recoder(list: List[(String, String)]) {
     private val (min, max) = {
       var min = '\uffff'
       var max = '\u0000'
       for ((x, _) <- list) {
         val c = x(0)
         if (c < min) min = c
         if (c > max) max = c
       }
       (min, max)
     }
     private val table = {
       var tab = Map[String, String]()
       for ((x, y) <- list) {
         tab.get(x) match {
           case None => tab += (x -> y)
           case Some(z) =>
             error("Duplicate symbol mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z))
         }
       }
       tab
     }
     def recode(text: String): String = {
       val len = text.length
       val matcher = new Symbol.Matcher(text)
       val result = new StringBuilder(len)
       var i = 0
       while (i < len) {
         val c = text(i)
         if (min <= c && c <= max) {
           val s = matcher.match_symbol(i)
           result.append(table.getOrElse(s, s))
           i += s.length
         }
         else { result.append(c); i += 1 }
       }
       result.toString
     }
   }
 
 
 
   /** defined symbols **/
 
   object Argument extends Enumeration {
     val none, cartouche, space_cartouche = Value
 
     def unapply(s: String): Option[Value] =
       try { Some(withName(s)) }
       catch { case _: NoSuchElementException => None}
   }
 
   object Entry {
     private val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
     private val Argument = new Properties.String("argument")
     private val Abbrev = new Properties.String("abbrev")
     private val Code = new Properties.String("code")
     private val Font = new Properties.String("font")
     private val Group = new Properties.String("group")
 
     def apply(symbol: Symbol, props: Properties.T): Entry = {
       def err(msg: String): Nothing = error(msg + " for symbol " + quote(symbol))
 
       val name =
         symbol match { case Name(a) => a case _ => err("Cannot determine name") }
 
       val argument =
         props match {
           case Argument(arg) =>
             Symbol.Argument.unapply(arg) getOrElse
               error("Bad argument: " + quote(arg) + " for symbol " + quote(symbol))
           case _ => Symbol.Argument.none
         }
 
       val code =
         props match {
           case Code(s) =>
             try {
               val code = Integer.decode(s).intValue
               if (code >= 128) Some(code) else err("Illegal ASCII code")
             }
             catch { case _: NumberFormatException => err("Bad code") }
           case _ => None
         }
 
       val groups = proper_list(for ((Group.name, a) <- props) yield a).getOrElse(List("unsorted"))
 
       val abbrevs = for ((Abbrev.name, a) <- props) yield a
 
       new Entry(symbol, name, argument, code, Font.unapply(props), groups, abbrevs)
     }
   }
 
   class Entry private(
     val symbol: Symbol,
     val name: String,
     val argument: Symbol.Argument.Value,
     val code: Option[Int],
     val font: Option[String],
     val groups: List[String],
     val abbrevs: List[String]
   ) {
     override def toString: String = symbol
 
     val decode: Option[String] =
       code.map(c => new String(Character.toChars(c)))
   }
 
   lazy val symbols: Symbols = Symbols.load()
 
   object Symbols {
     def load(static: Boolean = false): Symbols = {
       val paths =
         if (static) List(Path.explode("~~/etc/symbols"))
         else Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS"))
       make(cat_lines(for (path <- paths if path.is_file) yield File.read(path)))
     }
 
     def make(symbols_spec: String): Symbols = {
       val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
       val Key = new Regex("""(?xs) (.+): """)
 
       def read_decl(decl: String): (Symbol, Properties.T) = {
         def err() = error("Bad symbol declaration: " + decl)
 
         def read_props(props: List[String]): Properties.T = {
           props match {
             case Nil => Nil
             case _ :: Nil => err()
             case Key(x) :: y :: rest => (x -> y.replace('\u2423', ' ')) :: read_props(rest)
             case _ => err()
           }
         }
         decl.split("\\s+").toList match {
           case sym :: props if sym.length > 1 && !is_malformed(sym) =>
             (sym, read_props(props))
           case _ => err()
         }
       }
 
       new Symbols(
         split_lines(symbols_spec).reverse.
           foldLeft((List.empty[Entry], Set.empty[Symbol])) {
             case (res, No_Decl()) => res
             case ((list, known), decl) =>
               val (sym, props) = read_decl(decl)
               if (known(sym)) (list, known)
               else (Entry(sym, props) :: list, known + sym)
           }._1)
     }
   }
 
   class Symbols(val entries: List[Entry]) {
     override def toString: String = entries.mkString("Symbols(", ", ", ")")
 
 
     /* basic properties */
 
     private val entries_map: Map[Symbol, Entry] =
       (for (entry <- entries.iterator) yield entry.symbol -> entry).toMap
 
     def get(sym: Symbol): Option[Entry] = entries_map.get(sym)
     def defined(sym: Symbol): Boolean = entries_map.isDefinedAt(sym)
 
     def defined_code(sym: Symbol): Boolean =
       get(sym) match { case Some(entry) => entry.code.isDefined case _ => false }
 
     val code_defined: Int => Boolean =
       (for (entry <- entries.iterator; code <- entry.code) yield code).toSet
 
     val groups_code: List[(String, List[Symbol])] =
       (for {
         entry <- entries.iterator if entry.code.isDefined
         group <- entry.groups.iterator
       } yield entry.symbol -> group)
         .toList.groupBy(_._2).toList.map({ case (g, list) => (g, list.map(_._1)) }).sortBy(_._1)
 
     def get_abbrevs(sym: Symbol): List[String] =
       get(sym) match { case Some(entry) => entry.abbrevs case _ => Nil }
 
 
     /* recoding */
 
     private val (decoder, encoder) = {
       val mapping =
         for (entry <- entries; s <- entry.decode) yield entry.symbol -> s
       (new Recoder(mapping), new Recoder(for ((x, y) <- mapping) yield (y, x)))
     }
 
     def decode(text: String): String = decoder.recode(text)
     def encode(text: String): String = encoder.recode(text)
 
     private def recode_set(elems: Iterable[String]): Set[String] =
       (elems.iterator ++ elems.iterator.map(decode)).toSet
 
     private def recode_map[A](elems: Iterable[(String, A)]): Map[String, A] =
       (elems.iterator ++ elems.iterator.map({ case (sym, a) => (decode(sym), a) })).toMap
 
 
     /* user fonts */
 
     val fonts: Map[Symbol, String] =
       recode_map(for (entry <- entries; font <- entry.font) yield entry.symbol -> font)
 
     val font_names: List[String] = fonts.iterator.map(_._2).toSet.toList
     val font_index: Map[String, Int] = (font_names zip font_names.indices.toList).toMap
 
     def lookup_font(sym: Symbol): Option[Int] = fonts.get(sym).map(font_index(_))
 
 
     /* classification */
 
     val letters: Set[String] = recode_set(List(
       "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
       "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
       "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
       "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z",
 
       "\\<A>", "\\<B>", "\\<C>", "\\<D>", "\\<E>", "\\<F>", "\\<G>",
       "\\<H>", "\\<I>", "\\<J>", "\\<K>", "\\<L>", "\\<M>", "\\<N>",
       "\\<O>", "\\<P>", "\\<Q>", "\\<R>", "\\<S>", "\\<T>", "\\<U>",
       "\\<V>", "\\<W>", "\\<X>", "\\<Y>", "\\<Z>", "\\<a>", "\\<b>",
       "\\<c>", "\\<d>", "\\<e>", "\\<f>", "\\<g>", "\\<h>", "\\<i>",
       "\\<j>", "\\<k>", "\\<l>", "\\<m>", "\\<n>", "\\<o>", "\\<p>",
       "\\<q>", "\\<r>", "\\<s>", "\\<t>", "\\<u>", "\\<v>", "\\<w>",
       "\\<x>", "\\<y>", "\\<z>",
 
       "\\<AA>", "\\<BB>", "\\<CC>", "\\<DD>", "\\<EE>", "\\<FF>",
       "\\<GG>", "\\<HH>", "\\<II>", "\\<JJ>", "\\<KK>", "\\<LL>",
       "\\<MM>", "\\<NN>", "\\<OO>", "\\<PP>", "\\<QQ>", "\\<RR>",
       "\\<SS>", "\\<TT>", "\\<UU>", "\\<VV>", "\\<WW>", "\\<XX>",
       "\\<YY>", "\\<ZZ>", "\\<aa>", "\\<bb>", "\\<cc>", "\\<dd>",
       "\\<ee>", "\\<ff>", "\\<gg>", "\\<hh>", "\\<ii>", "\\<jj>",
       "\\<kk>", "\\<ll>", "\\<mm>", "\\<nn>", "\\<oo>", "\\<pp>",
       "\\<qq>", "\\<rr>", "\\<ss>", "\\<tt>", "\\<uu>", "\\<vv>",
       "\\<ww>", "\\<xx>", "\\<yy>", "\\<zz>",
 
       "\\<alpha>", "\\<beta>", "\\<gamma>", "\\<delta>", "\\<epsilon>",
       "\\<zeta>", "\\<eta>", "\\<theta>", "\\<iota>", "\\<kappa>",
       "\\<mu>", "\\<nu>", "\\<xi>", "\\<pi>", "\\<rho>", "\\<sigma>",
       "\\<tau>", "\\<upsilon>", "\\<phi>", "\\<chi>", "\\<psi>",
       "\\<omega>", "\\<Gamma>", "\\<Delta>", "\\<Theta>", "\\<Lambda>",
       "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
       "\\<Psi>", "\\<Omega>"))
 
     val blanks: Set[String] = recode_set(List(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n"))
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
 
     val symbolic: Set[String] =
       recode_set(for (entry <- entries if raw_symbolic(entry.symbol)) yield entry.symbol)
 
 
     /* misc symbols */
 
     val newline_decoded: Symbol = decode(newline)
     val comment_decoded: Symbol = decode(comment)
     val cancel_decoded: Symbol = decode(cancel)
     val latex_decoded: Symbol = decode(latex)
     val marker_decoded: Symbol = decode(marker)
     val open_decoded: Symbol = decode(open)
     val close_decoded: Symbol = decode(close)
 
 
     /* control symbols */
 
     val control_decoded: Set[Symbol] =
       (for (entry <- entries.iterator if entry.symbol.startsWith("\\<^"); s <- entry.decode)
         yield s).toSet
 
     val sub_decoded: Symbol = decode(sub)
     val sup_decoded: Symbol = decode(sup)
     val bold_decoded: Symbol = decode(bold)
     val emph_decoded: Symbol = decode(emph)
     val bsub_decoded: Symbol = decode(bsub)
     val esub_decoded: Symbol = decode(esub)
     val bsup_decoded: Symbol = decode(bsup)
     val esup_decoded: Symbol = decode(esup)
   }
 
 
   /* tables */
 
   def decode(text: String): String = symbols.decode(text)
   def encode(text: String): String = symbols.encode(text)
 
   def decode_yxml(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
     YXML.parse_body(decode(text), cache = cache)
 
   def decode_yxml_failsafe(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
     YXML.parse_body_failsafe(decode(text), cache = cache)
 
   def encode_yxml(body: XML.Body): String = encode(YXML.string_of_body(body))
 
   def decode_strict(text: String): String = {
     val decoded = decode(text)
     if (encode(decoded) == text) decoded
     else {
       val bad = new mutable.ListBuffer[Symbol]
       for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s))
         bad += s
       error("Bad Unicode symbols in text: " + commas_quote(bad))
     }
   }
 
   def output(unicode_symbols: Boolean, text: String): String =
     if (unicode_symbols) Symbol.decode(text) else Symbol.encode(text)
 
 
   /* classification */
 
   def is_letter(sym: Symbol): Boolean = symbols.letters.contains(sym)
   def is_digit(sym: Symbol): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
   def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'"
   def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
   def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
 
 
   /* symbolic newline */
 
   val newline: Symbol = "\\<newline>"
   def newline_decoded: Symbol = symbols.newline_decoded
 
   def print_newlines(str: String): String =
     if (str.contains('\n'))
       (for (s <- iterator(str)) yield { if (s == "\n") newline_decoded else s }).mkString
     else str
 
 
   /* formal comments */
 
   val comment: Symbol = "\\<comment>"
   val cancel: Symbol = "\\<^cancel>"
   val latex: Symbol = "\\<^latex>"
   val marker: Symbol = "\\<^marker>"
 
   def comment_decoded: Symbol = symbols.comment_decoded
   def cancel_decoded: Symbol = symbols.cancel_decoded
   def latex_decoded: Symbol = symbols.latex_decoded
   def marker_decoded: Symbol = symbols.marker_decoded
 
 
   /* cartouches */
 
   val open: Symbol = "\\<open>"
   val close: Symbol = "\\<close>"
 
   def open_decoded: Symbol = symbols.open_decoded
   def close_decoded: Symbol = symbols.close_decoded
 
   def is_open(sym: Symbol): Boolean = sym == open_decoded || sym == open
   def is_close(sym: Symbol): Boolean = sym == close_decoded || sym == close
 
   def cartouche(s: String): String = open + s + close
   def cartouche_decoded(s: String): String = open_decoded + s + close_decoded
 
 
   /* symbols for symbolic identifiers */
 
   private def raw_symbolic(sym: Symbol): Boolean =
     sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
 
   def is_symbolic(sym: Symbol): Boolean =
     !is_open(sym) && !is_close(sym) && (raw_symbolic(sym) || symbols.symbolic.contains(sym))
 
   def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
 
 
   /* control symbols */
 
   val control_prefix = "\\<^"
   val control_suffix = ">"
 
   def control_name(sym: Symbol): Option[String] =
     if (is_control_encoded(sym))
       Some(sym.substring(control_prefix.length, sym.length - control_suffix.length))
     else None
 
   def is_control_encoded(sym: Symbol): Boolean =
     sym.startsWith(control_prefix) && sym.endsWith(control_suffix)
 
   def is_control(sym: Symbol): Boolean =
     is_control_encoded(sym) || symbols.control_decoded.contains(sym)
 
   def is_controllable(sym: Symbol): Boolean =
     !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) &&
     !is_malformed(sym) && sym != "\""
 
   val sub: Symbol = "\\<^sub>"
   val sup: Symbol = "\\<^sup>"
   val bold: Symbol = "\\<^bold>"
   val emph: Symbol = "\\<^emph>"
   val bsub: Symbol = "\\<^bsub>"
   val esub: Symbol = "\\<^esub>"
   val bsup: Symbol = "\\<^bsup>"
   val esup: Symbol = "\\<^esup>"
 
   def sub_decoded: Symbol = symbols.sub_decoded
   def sup_decoded: Symbol = symbols.sup_decoded
   def bold_decoded: Symbol = symbols.bold_decoded
   def emph_decoded: Symbol = symbols.emph_decoded
   def bsub_decoded: Symbol = symbols.bsub_decoded
   def esub_decoded: Symbol = symbols.esub_decoded
   def bsup_decoded: Symbol = symbols.bsup_decoded
   def esup_decoded: Symbol = symbols.esup_decoded
 
 
   /* metric */
 
   def is_printable(sym: Symbol): Boolean =
     if (is_ascii(sym)) is_ascii_printable(sym(0))
     else !is_control(sym)
 
   object Metric extends Pretty.Metric {
     val unit = 1.0
     def apply(str: String): Double =
       (for (s <- iterator(str)) yield {
         val sym = encode(s)
         if (sym.startsWith("\\<long") || sym.startsWith("\\<Long")) 2
         else if (is_printable(sym)) 1
         else 0
       }).sum
   }
 }
diff --git a/src/Pure/PIDE/command.scala b/src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala
+++ b/src/Pure/PIDE/command.scala
@@ -1,642 +1,642 @@
 /*  Title:      Pure/PIDE/command.scala
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
 Prover commands with accumulated results from execution.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.SortedMap
 
 
 object Command {
   /* blobs */
 
   object Blob {
     def read_file(name: Document.Node.Name, src_path: Path): Blob = {
       val bytes = Bytes.read(name.path)
       val chunk = Symbol.Text_Chunk(bytes.text)
       Blob(name, src_path, Some((bytes.sha1_digest, chunk)))
     }
   }
 
   sealed case class Blob(
     name: Document.Node.Name,
     src_path: Path,
     content: Option[(SHA1.Digest, Symbol.Text_Chunk)]
   ) {
     def read_file: Bytes = Bytes.read(name.path)
 
     def chunk_file: Symbol.Text_Chunk.File =
       Symbol.Text_Chunk.File(name.node)
   }
 
   object Blobs_Info {
     val none: Blobs_Info = Blobs_Info(Nil)
 
     def errors(msgs: List[String]): Blobs_Info =
       Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg))))
   }
 
   sealed case class Blobs_Info(blobs: List[Exn.Result[Blob]], index: Int = -1)
 
 
 
   /** accumulated results from prover **/
 
   /* results */
 
   object Results {
     type Entry = (Long, XML.Elem)
     val empty: Results = new Results(SortedMap.empty)
     def make(args: IterableOnce[Results.Entry]): Results =
       args.iterator.foldLeft(empty)(_ + _)
     def merge(args: IterableOnce[Results]): Results =
       args.iterator.foldLeft(empty)(_ ++ _)
   }
 
   final class Results private(private val rep: SortedMap[Long, XML.Elem]) {
     def is_empty: Boolean = rep.isEmpty
     def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
     def get(serial: Long): Option[XML.Elem] = rep.get(serial)
     def iterator: Iterator[Results.Entry] = rep.iterator
 
     def + (entry: Results.Entry): Results =
       if (defined(entry._1)) this
       else new Results(rep + entry)
 
     def ++ (other: Results): Results =
       if (this eq other) this
       else if (rep.isEmpty) other
       else other.iterator.foldLeft(this)(_ + _)
 
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Results => rep == other.rep
         case _ => false
       }
     override def toString: String = iterator.mkString("Results(", ", ", ")")
   }
 
 
   /* exports */
 
   object Exports {
     type Entry = (Long, Export.Entry)
     val empty: Exports = new Exports(SortedMap.empty)
     def merge(args: IterableOnce[Exports]): Exports =
       args.iterator.foldLeft(empty)(_ ++ _)
   }
 
   final class Exports private(private val rep: SortedMap[Long, Export.Entry]) {
     def is_empty: Boolean = rep.isEmpty
     def iterator: Iterator[Exports.Entry] = rep.iterator
 
     def + (entry: Exports.Entry): Exports =
       if (rep.isDefinedAt(entry._1)) this
       else new Exports(rep + entry)
 
     def ++ (other: Exports): Exports =
       if (this eq other) this
       else if (rep.isEmpty) other
       else other.iterator.foldLeft(this)(_ + _)
 
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Exports => rep == other.rep
         case _ => false
       }
     override def toString: String = iterator.mkString("Exports(", ", ", ")")
   }
 
 
   /* markups */
 
   object Markup_Index {
     val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default)
     def blob(blob: Blob): Markup_Index = Markup_Index(false, blob.chunk_file)
   }
 
   sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name)
 
   object Markups {
     type Entry = (Markup_Index, Markup_Tree)
     val empty: Markups = new Markups(Map.empty)
     def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
     def make(args: IterableOnce[Entry]): Markups =
       args.iterator.foldLeft(empty)(_ + _)
     def merge(args: IterableOnce[Markups]): Markups =
       args.iterator.foldLeft(empty)(_ ++ _)
   }
 
   final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) {
     def is_empty: Boolean = rep.isEmpty
 
     def apply(index: Markup_Index): Markup_Tree =
       rep.getOrElse(index, Markup_Tree.empty)
 
     def add(index: Markup_Index, markup: Text.Markup): Markups =
       new Markups(rep + (index -> (this(index) + markup)))
 
     def + (entry: Markups.Entry): Markups = {
       val (index, tree) = entry
       new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full))))
     }
 
     def ++ (other: Markups): Markups =
       if (this eq other) this
       else if (rep.isEmpty) other
       else other.rep.iterator.foldLeft(this)(_ + _)
 
     def redirection_iterator: Iterator[Document_ID.Generic] =
       for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
         yield id
 
     def redirect(other_id: Document_ID.Generic): Markups = {
       val rep1 =
         (for {
           (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator
           if other_id == id
         } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap
       if (rep1.isEmpty) Markups.empty else new Markups(rep1)
     }
 
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Markups => rep == other.rep
         case _ => false
       }
     override def toString: String = rep.iterator.mkString("Markups(", ", ", ")")
   }
 
 
   /* state */
 
   object State {
     def get_result(states: List[State], serial: Long): Option[XML.Elem] =
       states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get)
 
     def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] =
       for {
         serial <- Markup.Serial.unapply(props)
         elem <- get_result(states, serial)
         if elem.body.nonEmpty
       } yield serial -> elem
 
     def merge_results(states: List[State]): Results =
       Results.merge(states.map(_.results))
 
     def merge_exports(states: List[State]): Exports =
       Exports.merge(states.map(_.exports))
 
     def merge_markups(states: List[State]): Markups =
       Markups.merge(states.map(_.markups))
 
     def merge_markup(states: List[State], index: Markup_Index,
         range: Text.Range, elements: Markup.Elements): Markup_Tree =
       Markup_Tree.merge(states.map(_.markup(index)), range, elements)
 
     def merge(command: Command, states: List[State]): State =
       State(command, states.flatMap(_.status), merge_results(states),
         merge_exports(states), merge_markups(states))
   }
 
   sealed case class State(
     command: Command,
     status: List[Markup] = Nil,
     results: Results = Results.empty,
     exports: Exports = Exports.empty,
     markups: Markups = Markups.empty
   ) {
     def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
     def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING)
     def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
 
     lazy val maybe_consolidated: Boolean = {
       var touched = false
       var forks = 0
       var runs = 0
       for (markup <- status) {
         markup.name match {
           case Markup.FORKED => touched = true; forks += 1
           case Markup.JOINED => forks -= 1
           case Markup.RUNNING => touched = true; runs += 1
           case Markup.FINISHED => runs -= 1
           case _ =>
         }
       }
       touched && forks == 0 && runs == 0
     }
 
     lazy val document_status: Document_Status.Command_Status = {
       val warnings =
         if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2)))
           List(Markup(Markup.WARNING, Nil))
         else Nil
       val errors =
         if (results.iterator.exists(p => Protocol.is_error(p._2)))
           List(Markup(Markup.ERROR, Nil))
         else Nil
       Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator)
     }
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)
 
     def redirect(other_command: Command): Option[State] = {
       val markups1 = markups.redirect(other_command.id)
       if (markups1.is_empty) None
       else Some(new State(other_command, markups = markups1))
     }
 
     private def add_status(st: Markup): State =
       copy(status = st :: status)
 
     private def add_result(entry: Results.Entry): State =
       copy(results = results + entry)
 
     def add_export(entry: Exports.Entry): Option[State] =
       if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry))
       else None
 
     private def add_markup(
       status: Boolean,
       chunk_name: Symbol.Text_Chunk.Name,
       m: Text.Markup
     ): State = {
       val markups1 =
         if (status || Document_Status.Command_Status.liberal_elements(m.info.name))
           markups.add(Markup_Index(true, chunk_name), m)
         else markups
       copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
     }
 
     def accumulate(
         self_id: Document_ID.Generic => Boolean,
         other_id: (Document.Node.Name, Document_ID.Generic) =>
           Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
         message: XML.Elem,
         cache: XML.Cache): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           if (command.span.is_theory) this
           else {
             msgs.foldLeft(this) {
               case (state, msg) =>
                 msg match {
                   case elem @ XML.Elem(markup, Nil) =>
                     state.
                       add_status(markup).
                       add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
                   case _ =>
                     Output.warning("Ignored status message: " + msg)
                     state
                 }
             }
           }
 
         case XML.Elem(Markup(Markup.REPORT, atts0), msgs) =>
           msgs.foldLeft(this) {
             case (state, msg) =>
               def bad(): Unit = Output.warning("Ignored report message: " + msg)
 
               msg match {
                 case XML.Elem(Markup(name, atts), args) =>
                   command.reported_position(atts) orElse command.reported_position(atts0) match {
                     case Some((id, chunk_name, target_range)) =>
                       val target =
                         if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
                           Some((chunk_name, command.chunks(chunk_name)))
                         else if (chunk_name == Symbol.Text_Chunk.Default)
                           other_id(command.node_name, id)
                         else None
 
                       (target, target_range) match {
                         case (Some((target_name, target_chunk)), Some(symbol_range))
                         if !symbol_range.is_singularity =>
                           target_chunk.incorporate(symbol_range) match {
                             case Some(range) =>
                               val props = atts.filterNot(Markup.position_property)
                               val elem = cache.elem(XML.Elem(Markup(name, props), args))
                               state.add_markup(false, target_name, Text.Info(range, elem))
                             case None => bad(); state
                           }
                         case _ =>
                           // silently ignore excessive reports
                           state
                       }
 
                     case _ => bad(); state
                   }
                 case _ => bad(); state
               }
           }
 
         case XML.Elem(Markup(name, props), body) =>
           props match {
             case Markup.Serial(i) =>
               val markup_message =
                 cache.elem(Protocol.make_message(body, kind = name, props = props))
               val message_markup =
                 cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
 
               var st = add_result(i -> markup_message)
               if (Protocol.is_inlined(message)) {
                 for {
                   (chunk_name, chunk) <- command.chunks.iterator
                   range <- command.message_positions(self_id, chunk_name, chunk, message)
                 } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup))
               }
               st
 
             case _ =>
               Output.warning("Ignored message without serial number: " + message)
               this
           }
       }
   }
 
 
 
   /** static content **/
 
   /* make commands */
 
   def apply(
     id: Document_ID.Command,
     node_name: Document.Node.Name,
     blobs_info: Blobs_Info,
     span: Command_Span.Span
   ): Command = {
     val (source, span1) = span.compact_source
     new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty)
   }
 
   val empty: Command =
     Command(Document_ID.none, Document.Node.Name.empty, Blobs_Info.none, Command_Span.empty)
 
   def unparsed(
     source: String,
     theory: Boolean = false,
     id: Document_ID.Command = Document_ID.none,
     node_name: Document.Node.Name = Document.Node.Name.empty,
     blobs_info: Blobs_Info = Blobs_Info.none,
     results: Results = Results.empty,
     markups: Markups = Markups.empty
   ): Command = {
     val (source1, span1) = Command_Span.unparsed(source, theory).compact_source
     new Command(id, node_name, blobs_info, span1, source1, results, markups)
   }
 
   def text(source: String): Command = unparsed(source)
 
   def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
     unparsed(XML.content(body), id = id, results = results,
       markups = Markups.init(Markup_Tree.from_XML(body)))
 
 
   /* edits and perspective */
 
   type Edit = (Option[Command], Option[Command])
 
   object Perspective {
     val empty: Perspective = Perspective(Nil)
   }
 
   sealed case class Perspective(
     commands: List[Command]  // visible commands in canonical order
   ) {
     def is_empty: Boolean = commands.isEmpty
 
     def same(that: Perspective): Boolean = {
       val cmds1 = this.commands
       val cmds2 = that.commands
       require(!cmds1.exists(_.is_undefined), "cmds1 not defined")
       require(!cmds2.exists(_.is_undefined), "cmds2 not defined")
       cmds1.length == cmds2.length &&
         (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
     }
   }
 
 
   /* blobs: inlined errors and auxiliary files */
 
   def blobs_info(
     resources: Resources,
     syntax: Outer_Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
     can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
     span: Command_Span.Span
   ): Blobs_Info = {
     span.name match {
       // inlined errors
       case Thy_Header.THEORY =>
         val reader = span.content_reader
         val header = resources.check_thy(node_name, span.content_reader)
         val imports_pos = header.imports_pos
         val raw_imports =
           try {
             val read_imports = Thy_Header.read(node_name, reader).imports.map(_._1)
             if (imports_pos.length == read_imports.length) read_imports else error("")
           }
           catch { case _: Throwable => List.fill(header.imports.length)("") }
 
         val errors =
           for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
           yield {
             val completion =
               if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
             "Bad theory import " +
               Markup.Path(import_name.node).markup(quote(import_name.toString)) +
               Position.here(pos) + Completion.report_theories(pos, completion)
           }
         Blobs_Info.errors(errors)
 
       // auxiliary files
       case _ =>
         val loaded_files = span.loaded_files(syntax)
         val blobs =
           loaded_files.files.map(file =>
             (Exn.capture {
               val src_path = Path.explode(file)
               val name = Document.Node.Name(resources.append(node_name, src_path))
               val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
               Blob(name, src_path, content)
             }).user_error)
         Blobs_Info(blobs, index = loaded_files.index)
     }
   }
 
   def build_blobs_info(
     syntax: Outer_Syntax,
     node_name: Document.Node.Name,
     load_commands: List[Command_Span.Span]
   ): Blobs_Info = {
     val blobs =
       for {
         span <- load_commands
         file <- span.loaded_files(syntax).files
       } yield {
         (Exn.capture {
           val dir = node_name.master_dir_path
           val src_path = Path.explode(file)
           val name = Document.Node.Name((dir + src_path).expand.implode_symbolic)
           Blob.read_file(name, src_path)
         }).user_error
       }
     Blobs_Info(blobs)
   }
 }
 
 
 final class Command private(
   val id: Document_ID.Command,
   val node_name: Document.Node.Name,
   val blobs_info: Command.Blobs_Info,
   val span: Command_Span.Span,
   val source: String,
   val init_results: Command.Results,
   val init_markups: Command.Markups
 ) {
   override def toString: String = id.toString + "/" + span.kind.toString
 
 
   /* classification */
 
   def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span]
   def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span
 
   def is_undefined: Boolean = id == Document_ID.none
   val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
   val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
 
   def potentially_initialized: Boolean = span.name == Thy_Header.THEORY
 
 
   /* blobs */
 
   def blobs: List[Exn.Result[Command.Blob]] = blobs_info.blobs
   def blobs_index: Int = blobs_info.index
 
   def blobs_ok: Boolean =
     blobs.forall({ case Exn.Res(_) => true case _ => false })
 
   def blobs_names: List[Document.Node.Name] =
     for (Exn.Res(blob) <- blobs) yield blob.name
 
   def blobs_undefined: List[Document.Node.Name] =
     for (Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name
 
   def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] =
     for (Exn.Res(blob) <- blobs; (digest, _) <- blob.content) yield (blob.name, digest)
 
   def blobs_changed(doc_blobs: Document.Blobs): Boolean =
     blobs.exists({ case Exn.Res(blob) => doc_blobs.changed(blob.name) case _ => false })
 
 
   /* source chunks */
 
   val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source)
 
   val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
     ((Symbol.Text_Chunk.Default -> chunk) ::
       (for (Exn.Res(blob) <- blobs; (_, file) <- blob.content)
         yield blob.chunk_file -> file)).toMap
 
   def length: Int = source.length
   def range: Text.Range = chunk.range
 
   val core_range: Text.Range =
     Text.Range(0,
-      span.content.reverse.iterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length))
+      span.content.reverseIterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length))
 
   def source(range: Text.Range): String = range.substring(source)
 
 
   /* theory parents */
 
   def theory_parents(resources: Resources): List[Document.Node.Name] =
     if (span.name == Thy_Header.THEORY) {
       try {
         val header = Thy_Header.read(node_name, span.content_reader)
         for ((s, _) <- header.imports)
         yield {
           try { resources.import_name(node_name, s) }
           catch { case ERROR(_) => Document.Node.Name.empty }
         }
       }
       catch { case ERROR(_) => Nil }
     }
     else Nil
 
 
   /* reported positions */
 
   def reported_position(
     pos: Position.T
   ) : Option[(Document_ID.Generic, Symbol.Text_Chunk.Name, Option[Symbol.Range])] = {
     pos match {
       case Position.Id(id) =>
         val chunk_name =
           pos match {
             case Position.File(name) if name != node_name.node =>
               Symbol.Text_Chunk.File(name)
             case _ => Symbol.Text_Chunk.Default
           }
         Some((id, chunk_name, Position.Range.unapply(pos)))
       case _ => None
     }
   }
 
   def message_positions(
     self_id: Document_ID.Generic => Boolean,
     chunk_name: Symbol.Text_Chunk.Name,
     chunk: Symbol.Text_Chunk,
     message: XML.Elem
   ): Set[Text.Range] = {
     def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       reported_position(props) match {
         case Some((id, name, reported_range)) if self_id(id) && name == chunk_name =>
           val opt_range =
             reported_range orElse {
               if (name == Symbol.Text_Chunk.Default)
                 Position.Range.unapply(span.position)
               else None
             }
           opt_range match {
             case Some(symbol_range) =>
               chunk.incorporate(symbol_range) match {
                 case Some(range) => set + range
                 case _ => set
               }
             case None => set
           }
         case _ => set
       }
     def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
       t match {
         case XML.Wrapped_Elem(Markup(name, props), _, body) =>
           body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree)
         case XML.Elem(Markup(name, props), body) =>
           body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree)
         case XML.Text(_) => set
       }
 
     val set = tree(Set.empty, message)
     if (set.isEmpty) elem(message.markup.properties, set)
     else set
   }
 
 
   /* accumulated results */
 
   val init_state: Command.State =
     Command.State(this, results = init_results, markups = init_markups)
 
   val empty_state: Command.State = Command.State(this)
 }
diff --git a/src/Pure/PIDE/document.scala b/src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala
+++ b/src/Pure/PIDE/document.scala
@@ -1,1224 +1,1224 @@
 /*  Title:      Pure/PIDE/document.scala
     Author:     Makarius
 
 Document as collection of named nodes, each consisting of an editable
 list of commands, associated with asynchronous execution process.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 
 
 object Document {
   /** document structure **/
 
   /* overlays -- print functions with arguments */
 
   object Overlays {
     val empty = new Overlays(Map.empty)
   }
 
   final class Overlays private(rep: Map[Node.Name, Node.Overlays]) {
     def apply(name: Node.Name): Node.Overlays =
       rep.getOrElse(name, Node.Overlays.empty)
 
     private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays = {
       val node_overlays = f(apply(name))
       new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays))
     }
 
     def insert(command: Command, fn: String, args: List[String]): Overlays =
       update(command.node_name, _.insert(command, fn, args))
 
     def remove(command: Command, fn: String, args: List[String]): Overlays =
       update(command.node_name, _.remove(command, fn, args))
 
     override def toString: String = rep.mkString("Overlays(", ",", ")")
   }
 
 
   /* document blobs: auxiliary files */
 
   sealed case class Blob(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean) {
     def unchanged: Blob = copy(changed = false)
   }
 
   object Blobs {
     def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
     val empty: Blobs = apply(Map.empty)
   }
 
   final class Blobs private(blobs: Map[Node.Name, Blob]) {
     def get(name: Node.Name): Option[Blob] = blobs.get(name)
 
     def changed(name: Node.Name): Boolean =
       get(name) match {
         case Some(blob) => blob.changed
         case None => false
       }
 
     override def toString: String = blobs.mkString("Blobs(", ",", ")")
   }
 
 
   /* document nodes: theories and auxiliary files */
 
   type Edit[A, B] = (Node.Name, Node.Edit[A, B])
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
   object Node {
     /* header and name */
 
     sealed case class Header(
       imports_pos: List[(Name, Position.T)] = Nil,
       keywords: Thy_Header.Keywords = Nil,
       abbrevs: Thy_Header.Abbrevs = Nil,
       errors: List[String] = Nil
     ) {
       def imports: List[Name] = imports_pos.map(_._1)
 
       def append_errors(msgs: List[String]): Header =
         copy(errors = errors ::: msgs)
 
       def cat_errors(msg2: String): Header =
         copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
     }
 
     val no_header: Header = Header()
     def bad_header(msg: String): Header = Header(errors = List(msg))
 
     object Name {
       val empty: Name = Name("")
 
       object Ordering extends scala.math.Ordering[Name] {
         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
       }
 
       type Graph[A] = isabelle.Graph[Node.Name, A]
 
       def make_graph[A](entries: List[((Name, A), List[Name])]): Graph[A] =
         Graph.make(entries, symmetric = true)(Ordering)
     }
 
     sealed case class Name(node: String, master_dir: String = "", theory: String = "") {
       override def hashCode: Int = node.hashCode
       override def equals(that: Any): Boolean =
         that match {
           case other: Name => node == other.node
           case _ => false
         }
 
       def path: Path = Path.explode(File.standard_path(node))
       def master_dir_path: Path = Path.explode(File.standard_path(master_dir))
 
       def expand: Name =
         Name(path.expand.implode, master_dir_path.expand.implode, theory)
 
       def is_theory: Boolean = theory.nonEmpty
 
       def theory_base_name: String = Long_Name.base_name(theory)
 
       override def toString: String = if (is_theory) theory else node
 
       def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
       def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
 
       def json: JSON.Object.T =
         JSON.Object("node_name" -> node, "theory_name" -> theory)
     }
 
     sealed case class Entry(name: Node.Name, header: Node.Header) {
       def map(f: String => String): Entry = copy(name = name.map(f))
 
       override def toString: String = name.toString
     }
 
 
     /* node overlays */
 
     object Overlays {
       val empty = new Overlays(Multi_Map.empty)
     }
 
     final class Overlays private(rep: Multi_Map[Command, (String, List[String])]) {
       def commands: Set[Command] = rep.keySet
       def is_empty: Boolean = rep.isEmpty
       def dest: List[(Command, (String, List[String]))] = rep.iterator.toList
       def insert(cmd: Command, fn: String, args: List[String]): Overlays =
         new Overlays(rep.insert(cmd, (fn, args)))
       def remove(cmd: Command, fn: String, args: List[String]): Overlays =
         new Overlays(rep.remove(cmd, (fn, args)))
 
       override def toString: String = rep.mkString("Node.Overlays(", ",", ")")
     }
 
 
     /* edits */
 
     sealed abstract class Edit[A, B] {
       def foreach(f: A => Unit): Unit = {
         this match {
           case Edits(es) => es.foreach(f)
           case _ =>
         }
       }
 
       def is_void: Boolean =
         this match {
           case Edits(Nil) => true
           case _ => false
         }
     }
     case class Blob[A, B](blob: Document.Blob) extends Edit[A, B]
 
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
     case class Deps[A, B](header: Header) extends Edit[A, B]
     case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
 
 
     /* perspective */
 
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
     type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 
     val no_perspective_text: Perspective_Text =
       Perspective(false, Text.Perspective.empty, Overlays.empty)
 
     val no_perspective_command: Perspective_Command =
       Perspective(false, Command.Perspective.empty, Overlays.empty)
 
     def is_no_perspective_text(perspective: Perspective_Text): Boolean =
       !perspective.required &&
       perspective.visible.is_empty &&
       perspective.overlays.is_empty
 
     def is_no_perspective_command(perspective: Perspective_Command): Boolean =
       !perspective.required &&
       perspective.visible.is_empty &&
       perspective.overlays.is_empty
 
 
     /* commands */
 
     object Commands {
       def apply(commands: Linear_Set[Command]): Commands = new Commands(commands)
       val empty: Commands = apply(Linear_Set.empty)
 
       def starts(
         commands: Iterator[Command],
         offset: Text.Offset = 0
       ) : Iterator[(Command, Text.Offset)] = {
         var i = offset
         for (command <- commands) yield {
           val start = i
           i += command.length
           (command, start)
         }
       }
 
       def starts_pos(
         commands: Iterator[Command],
         pos: Token.Pos = Token.Pos.start
       ) : Iterator[(Command, Token.Pos)] = {
         var p = pos
         for (command <- commands) yield {
           val start = p
           p = command.span.content.foldLeft(p)(_.advance(_))
           (command, start)
         }
       }
 
       private val block_size = 256
     }
 
     final class Commands private(val commands: Linear_Set[Command]) {
       lazy val load_commands: List[Command] =
         commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList
 
       private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = {
         val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
         var next_block = 0
         var last_stop = 0
         for ((command, start) <- Commands.starts(commands.iterator)) {
           last_stop = start + command.length
           while (last_stop + 1 > next_block) {
             blocks += (command -> start)
             next_block += Commands.block_size
           }
         }
         (blocks.toArray, Text.Range(0, last_stop))
       }
 
       private def full_range: Text.Range = full_index._2
 
       def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = {
         if (commands.nonEmpty && full_range.contains(i)) {
           val (cmd0, start0) = full_index._1(i / Commands.block_size)
           Node.Commands.starts(commands.iterator(cmd0), start0) dropWhile {
             case (cmd, start) => start + cmd.length <= i }
         }
         else Iterator.empty
       }
     }
 
     val empty: Node = new Node()
   }
 
   final class Node private(
     val get_blob: Option[Document.Blob] = None,
     val header: Node.Header = Node.no_header,
     val syntax: Option[Outer_Syntax] = None,
     val text_perspective: Text.Perspective = Text.Perspective.empty,
     val perspective: Node.Perspective_Command = Node.no_perspective_command,
     _commands: Node.Commands = Node.Commands.empty
   ) {
     def is_empty: Boolean =
       get_blob.isEmpty &&
       header == Node.no_header &&
       text_perspective.is_empty &&
       Node.is_no_perspective_command(perspective) &&
       commands.isEmpty
 
     def has_header: Boolean = header != Node.no_header
 
     override def toString: String =
       if (is_empty) "empty"
       else if (get_blob.isDefined) "blob"
       else "node"
 
     def commands: Linear_Set[Command] = _commands.commands
     def load_commands: List[Command] = _commands.load_commands
     def load_commands_changed(doc_blobs: Blobs): Boolean =
       load_commands.exists(_.blobs_changed(doc_blobs))
 
     def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged))
 
     def update_header(new_header: Node.Header): Node =
       new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
 
     def update_syntax(new_syntax: Option[Outer_Syntax]): Node =
       new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
 
     def update_perspective(
         new_text_perspective: Text.Perspective,
         new_perspective: Node.Perspective_Command): Node =
       new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
 
     def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] =
       Node.Perspective(perspective.required, text_perspective, perspective.overlays)
 
     def same_perspective(
         other_text_perspective: Text.Perspective,
         other_perspective: Node.Perspective_Command): Boolean =
       text_perspective == other_text_perspective &&
       perspective.required == other_perspective.required &&
       perspective.visible.same(other_perspective.visible) &&
       perspective.overlays == other_perspective.overlays
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
       else
         new Node(get_blob, header, syntax, text_perspective, perspective,
           Node.Commands(new_commands))
 
     def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       _commands.iterator(i)
 
     def command_iterator(range: Text.Range): Iterator[(Command, Text.Offset)] =
       command_iterator(range.start) takeWhile { case (_, start) => start < range.stop }
 
     def command_start(cmd: Command): Option[Text.Offset] =
       Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
 
     lazy val source: String =
       get_blob match {
         case Some(blob) => blob.source
         case None => command_iterator().map({ case (cmd, _) => cmd.source }).mkString
       }
   }
 
 
   /* development graph */
 
   object Nodes {
     val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering))
   }
 
   final class Nodes private(graph: Graph[Node.Name, Node]) {
     def apply(name: Node.Name): Node =
       graph.default_node(name, Node.empty).get_node(name)
 
     def is_suppressed(name: Node.Name): Boolean = {
       val graph1 = graph.default_node(name, Node.empty)
       graph1.is_maximal(name) && graph1.get_node(name).is_empty
     }
 
     def purge_suppressed: Option[Nodes] =
       graph.keys_iterator.filter(is_suppressed).toList match {
         case Nil => None
         case del => Some(new Nodes(del.foldLeft(graph)(_.del_node(_))))
       }
 
     def + (entry: (Node.Name, Node)): Nodes = {
       val (name, node) = entry
       val imports = node.header.imports
       val graph1 =
         imports.foldLeft(graph.default_node(name, Node.empty)) {
           case (g, p) => g.default_node(p, Node.empty)
         }
       val graph2 =
         graph1.imm_preds(name).foldLeft(graph1) { case (g, dep) => g.del_edge(dep, name) }
       val graph3 = imports.foldLeft(graph2) { case (g, dep) => g.add_edge(dep, name) }
       new Nodes(graph3.map_node(name, _ => node))
     }
 
     def domain: Set[Node.Name] = graph.domain
 
     def iterator: Iterator[(Node.Name, Node)] =
       graph.iterator.map({ case (name, (node, _)) => (name, node) })
 
     def theory_name(theory: String): Option[Node.Name] =
       graph.keys_iterator.find(name => name.theory == theory)
 
     def commands_loading(file_name: Node.Name): List[Command] =
       (for {
         (_, node) <- iterator
         cmd <- node.load_commands.iterator
         name <- cmd.blobs_names.iterator
         if name == file_name
       } yield cmd).toList
 
     def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
     def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds_rev(names)
     def topological_order: List[Node.Name] = graph.topological_order
 
     override def toString: String = topological_order.mkString("Nodes(", ",", ")")
   }
 
 
 
   /** versioning **/
 
   /* particular document versions */
 
   object Version {
     val init: Version = new Version()
     def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes)
 
     def purge_future(
       versions: Map[Document_ID.Version, Version],
       future: Future[Version]
     ) : Future[Version] = {
       if (future.is_finished) {
         val version = future.join
         versions.get(version.id) match {
           case Some(version1) if !(version eq version1) => Future.value(version1)
           case _ => future
         }
       }
       else future
     }
 
     def purge_suppressed(
       versions: Map[Document_ID.Version, Version]
     ): Map[Document_ID.Version, Version] = {
       (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)).
         foldLeft(versions)(_ + _)
     }
   }
 
   final class Version private(
     val id: Document_ID.Version = Document_ID.none,
     val nodes: Nodes = Nodes.empty
   ) {
     override def toString: String = "Version(" + id + ")"
 
     def purge_suppressed: Option[Version] =
       nodes.purge_suppressed.map(new Version(id, _))
   }
 
 
   /* changes of plain text, eventually resulting in document edits */
 
   object Change {
     val init: Change = new Change()
 
     def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
       new Change(Some(previous), edits.reverse, version)
   }
 
   final class Change private(
     val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
     val rev_edits: List[Edit_Text] = Nil,
     val version: Future[Version] = Future.value(Version.init)
   ) {
     def is_finished: Boolean =
       (previous match { case None => true case Some(future) => future.is_finished }) &&
       version.is_finished
 
     def truncate: Change = new Change(None, Nil, version)
 
     def purge(versions: Map[Document_ID.Version, Version]): Option[Change] = {
       val previous1 = previous.map(Version.purge_future(versions, _))
       val version1 = Version.purge_future(versions, version)
       if ((previous eq previous1) && (version eq version1)) None
       else Some(new Change(previous1, rev_edits, version1))
     }
   }
 
 
   /* history navigation */
 
   object History {
     val init: History = new History()
   }
 
   final class History private(
     val undo_list: List[Change] = List(Change.init)  // non-empty list
   ) {
     override def toString: String = "History(" + undo_list.length + ")"
 
     def tip: Change = undo_list.head
     def + (change: Change): History = new History(change :: undo_list)
 
     def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] = {
       val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1
       val (retained, dropped) = undo_list.splitAt(n max retain)
 
       retained.splitAt(retained.length - 1) match {
         case (prefix, List(last)) => Some(dropped, new History(prefix ::: List(last.truncate)))
         case _ => None
       }
     }
 
     def purge(versions: Map[Document_ID.Version, Version]): History = {
       val undo_list1 = undo_list.map(_.purge(versions))
       if (undo_list1.forall(_.isEmpty)) this
       else new History(for ((a, b) <- undo_list1 zip undo_list) yield a.getOrElse(b))
     }
   }
 
 
   /* snapshot: persistent user-view of document state */
 
   object Snapshot {
     val init: Snapshot = State.init.snapshot()
   }
 
   class Snapshot private[Document](
     val state: State,
     val version: Version,
     val node_name: Node.Name,
     edits: List[Text.Edit],
     val snippet_command: Option[Command]
   ) {
     override def toString: String =
       "Snapshot(node = " + node_name.node + ", version = " + version.id +
         (if (is_outdated) ", outdated" else "") + ")"
 
 
     /* nodes */
 
     def get_node(name: Node.Name): Node = version.nodes(name)
 
     val node: Node = get_node(node_name)
 
     def node_files: List[Node.Name] =
       node_name :: node.load_commands.flatMap(_.blobs_names)
 
 
     /* source text */
 
     def source: String =
       snippet_command match {
         case Some(command) => command.source
         case None => node.source
       }
 
 
     /* edits */
 
     def is_outdated: Boolean = edits.nonEmpty
 
     private lazy val reverse_edits = edits.reverse
 
     def convert(offset: Text.Offset): Text.Offset =
       edits.foldLeft(offset) { case (i, edit) => edit.convert(i) }
     def revert(offset: Text.Offset): Text.Offset =
       reverse_edits.foldLeft(offset) { case (i, edit) => edit.revert(i) }
 
     def convert(range: Text.Range): Text.Range = range.map(convert)
     def revert(range: Text.Range): Text.Range = range.map(revert)
 
 
     /* theory load commands */
 
     val commands_loading: List[Command] =
       if (node_name.is_theory) Nil
       else version.nodes.commands_loading(node_name)
 
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] =
       (for {
         cmd <- node.load_commands.iterator
         blob_name <- cmd.blobs_names.iterator
         if pred(blob_name)
         start <- node.command_start(cmd)
       } yield convert(cmd.core_range + start)).toList
 
 
     /* command as add-on snippet */
 
     def snippet(command: Command): Snapshot = {
       val node_name = command.node_name
 
       val nodes0 = version.nodes
       val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
       val version1 = Document.Version.make(nodes1)
 
       val edits: List[Edit_Text] =
         List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source))))
 
       val state0 = state.define_command(command)
       val state1 =
         state0.continue_history(Future.value(version), edits, Future.value(version1))
           .define_version(version1, state0.the_assignment(version))
           .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
 
       state1.snapshot(node_name = node_name, snippet_command = Some(command))
     }
 
 
     /* XML markup */
 
     def xml_markup(
         range: Text.Range = Text.Range.full,
         elements: Markup.Elements = Markup.Elements.full): XML.Body =
       state.xml_markup(version, node_name, range = range, elements = elements)
 
     def xml_markup_blobs(
       elements: Markup.Elements = Markup.Elements.full
     ) : List[(Command.Blob, XML.Body)] = {
       snippet_command match {
         case None => Nil
         case Some(command) =>
           for (Exn.Res(blob) <- command.blobs)
           yield {
             val bytes = blob.read_file
             val text = bytes.text
             val xml =
               if (Bytes(text) == bytes) {
                 val markup = command.init_markups(Command.Markup_Index.blob(blob))
-                markup.to_XML(Text.Range(0, text.length), text, elements)
+                markup.to_XML(Text.Range.length(text), text, elements)
               }
               else Nil
             blob -> xml
           }
       }
     }
 
 
     /* messages */
 
     lazy val messages: List[(XML.Elem, Position.T)] =
       (for {
         (command, start) <-
           Document.Node.Commands.starts_pos(
             node.commands.iterator, Token.Pos.file(node_name.node))
         pos = command.span.keyword_pos(start).position(command.span.name)
         (_, elem) <- state.command_results(version, command).iterator
        } yield (elem, pos)).toList
 
 
     /* exports */
 
     lazy val exports: List[Export.Entry] =
       state.node_exports(version, node_name).iterator.map(_._2).toList
 
     lazy val all_exports: Map[Export.Entry_Name, Export.Entry] =
       (for {
         (name, _) <- version.nodes.iterator
         (_, entry) <- state.node_exports(version, name).iterator
         if entry.entry_name.session == Sessions.DRAFT
       } yield entry.entry_name -> entry).toMap
 
 
     /* find command */
 
     def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
       state.lookup_id(id) match {
         case None => None
         case Some(st) =>
           val command = st.command
           val command_node = get_node(command.node_name)
           if (command_node.commands.contains(command)) Some((command_node, command)) else None
       }
 
     def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
         : Option[Line.Node_Position] =
       for ((node, command) <- find_command(id))
       yield {
         val name = command.node_name.node
         val sources_iterator =
           node.commands.iterator.takeWhile(_ != command).map(_.source) ++
             (if (offset == 0) Iterator.empty
              else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
         val pos = sources_iterator.foldLeft(Line.Position.zero)(_.advance(_))
         Line.Node_Position(name, pos)
       }
 
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
       if (other_node_name.is_theory) {
         val other_node = get_node(other_node_name)
         val iterator = other_node.command_iterator(revert(offset) max 0)
         if (iterator.hasNext) {
           val (command0, _) = iterator.next()
           other_node.commands.reverse.iterator(command0).find(command => !command.is_ignored)
         }
         else other_node.commands.reverse.iterator.find(command => !command.is_ignored)
       }
       else version.nodes.commands_loading(other_node_name).headOption
 
 
     /* command results */
 
     def command_results(range: Text.Range): Command.Results =
       Command.State.merge_results(
         select[List[Command.State]](range, Markup.Elements.full,
           command_states => _ => Some(command_states)).flatMap(_.info))
 
     def command_results(command: Command): Command.Results =
       state.command_results(version, command)
 
 
     /* cumulate markup */
 
     def cumulate[A](
       range: Text.Range,
       info: A,
       elements: Markup.Elements,
       result: List[Command.State] => (A, Text.Markup) => Option[A],
       status: Boolean = false
     ): List[Text.Info[A]] = {
       val former_range = revert(range).inflate_singularity
       val (chunk_name, command_iterator) =
         commands_loading.headOption match {
           case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
           case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
         }
       val markup_index = Command.Markup_Index(status, chunk_name)
       (for {
         (command, command_start) <- command_iterator
         chunk <- command.chunks.get(chunk_name).iterator
         states = state.command_states(version, command)
         res = result(states)
         markup_range <- (former_range - command_start).try_restrict(chunk.range).iterator
         markup = Command.State.merge_markup(states, markup_index, markup_range, elements)
         Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements,
           {
             case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
           }).iterator
         r1 <- convert(r0 + command_start).try_restrict(range).iterator
       } yield Text.Info(r1, a)).toList
     }
 
     def select[A](
       range: Text.Range,
       elements: Markup.Elements,
       result: List[Command.State] => Text.Markup => Option[A],
       status: Boolean = false
     ): List[Text.Info[A]] = {
       def result1(states: List[Command.State]): (Option[A], Text.Markup) => Option[Option[A]] = {
         val res = result(states)
         (_: Option[A], x: Text.Markup) =>
           res(x) match {
             case None => None
             case some => Some(some)
           }
       }
       for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
         yield Text.Info(r, x)
     }
   }
 
 
   /* model */
 
   trait Session {
     def resources: Resources
   }
 
   trait Model {
     def session: Session
     def is_stable: Boolean
     def snapshot(): Snapshot
 
     def node_name: Node.Name
     def is_theory: Boolean = node_name.is_theory
     override def toString: String = node_name.toString
 
     def get_text(range: Text.Range): Option[String]
 
     def node_required: Boolean
     def get_blob: Option[Blob]
     def bibtex_entries: List[Text.Info[String]]
 
     def node_edits(
       node_header: Node.Header,
       text_edits: List[Text.Edit],
       perspective: Node.Perspective_Text
     ): List[Edit_Text] = {
       val edits: List[Node.Edit[Text.Edit, Text.Perspective]] =
         get_blob match {
           case None =>
             List(
               Node.Deps(
                 if (session.resources.session_base.loaded_theory(node_name)) {
                   node_header.append_errors(
                     List("Cannot update finished theory " + quote(node_name.theory)))
                 }
                 else node_header),
               Node.Edits(text_edits), perspective)
           case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits))
         }
       edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit))
     }
   }
 
 
   /** global state -- document structure, execution process, editing history **/
 
   type Assign_Update =
     List[(Document_ID.Command, List[Document_ID.Exec])]  // update of exec state assignment
 
   object State {
     class Fail(state: State) extends Exception
 
     object Assignment {
       val init: Assignment = new Assignment()
     }
 
     final class Assignment private(
       val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty,
       val is_finished: Boolean = false
     ) {
       override def toString: String = "Assignment(" + command_execs.size + "," + is_finished + ")"
 
       def check_finished: Assignment = { require(is_finished, "assignment not finished"); this }
       def unfinished: Assignment = new Assignment(command_execs, false)
 
       def assign(update: Assign_Update): Assignment = {
         require(!is_finished, "assignment already finished")
         val command_execs1 =
           update.foldLeft(command_execs) {
             case (res, (command_id, exec_ids)) =>
               if (exec_ids.isEmpty) res - command_id
               else res + (command_id -> exec_ids)
           }
         new Assignment(command_execs1, true)
       }
     }
 
     val init: State =
       State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2
   }
 
   final case class State private(
     /*reachable versions*/
     versions: Map[Document_ID.Version, Version] = Map.empty,
     /*inlined auxiliary files*/
     blobs: Set[SHA1.Digest] = Set.empty,
     /*loaded theories in batch builds*/
     theories: Map[Document_ID.Exec, Command.State] = Map.empty,
     /*static markup from define_command*/
     commands: Map[Document_ID.Command, Command.State] = Map.empty,
     /*dynamic markup from execution*/
     execs: Map[Document_ID.Exec, Command.State] = Map.empty,
     /*command-exec assignment for each version*/
     assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
     /*commands with markup produced by other commands (imm_succs)*/
     commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
     /*explicit (linear) history*/
     history: History = History.init,
     /*intermediate state between remove_versions/removed_versions*/
     removing_versions: Boolean = false
   ) {
     override def toString: String =
       "State(versions = " + versions.size +
       ", blobs = " + blobs.size +
       ", commands = " + commands.size +
       ", execs = " + execs.size +
       ", assignments = " + assignments.size +
       ", commands_redirection = " + commands_redirection.size +
       ", history = " + history.undo_list.size +
       ", removing_versions = " + removing_versions + ")"
 
     private def fail[A]: A = throw new State.Fail(this)
 
     def define_version(version: Version, assignment: State.Assignment): State = {
       val id = version.id
       copy(versions = versions + (id -> version),
         assignments = assignments + (id -> assignment.unfinished))
     }
 
     def define_blob(digest: SHA1.Digest): State = copy(blobs = blobs + digest)
     def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest)
 
     def define_command(command: Command): State = {
       val id = command.id
       if (commands.isDefinedAt(id)) fail
       else copy(commands = commands + (id -> command.init_state))
     }
 
     def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
 
     def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
     def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
     def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
 
     def lookup_id(id: Document_ID.Generic): Option[Command.State] =
       theories.get(id) orElse commands.get(id) orElse execs.get(id)
 
     private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
       id == st.command.id ||
       (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
 
     private def other_id(
       node_name: Node.Name,
       id: Document_ID.Generic
     ) : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = {
       for {
         st <- lookup_id(id)
         if st.command.node_name == node_name
       } yield (Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)
     }
 
     private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
       st.markups.redirection_iterator.foldLeft(commands_redirection) {
         case (graph, id) =>
           graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id)
       }
 
     def accumulate(
       id: Document_ID.Generic,
       message: XML.Elem,
       cache: XML.Cache
     ) : (Command.State, State) = {
       def update(st: Command.State): (Command.State, State) = {
         val st1 = st.accumulate(self_id(st), other_id, message, cache)
         (st1, copy(commands_redirection = redirection(st1)))
       }
       execs.get(id).map(update) match {
         case Some((st1, state1)) => (st1, state1.copy(execs = execs + (id -> st1)))
         case None =>
           commands.get(id).map(update) match {
             case Some((st1, state1)) => (st1, state1.copy(commands = commands + (id -> st1)))
             case None =>
               theories.get(id).map(update) match {
                 case Some((st1, state1)) => (st1, state1.copy(theories = theories + (id -> st1)))
                 case None => fail
               }
           }
       }
     }
 
     def add_export(
       id: Document_ID.Generic,
       entry: Command.Exports.Entry
     ): (Command.State, State) = {
       execs.get(id) match {
         case Some(st) =>
           st.add_export(entry) match {
             case Some(new_st) => (new_st, copy(execs = execs + (id -> new_st)))
             case None => fail
           }
         case None =>
           commands.get(id) match {
             case Some(st) =>
               st.add_export(entry) match {
                 case Some(new_st) => (new_st, copy(commands = commands + (id -> new_st)))
                 case None => fail
               }
             case None => fail
           }
       }
     }
 
     def node_exports(version: Version, node_name: Node.Name): Command.Exports =
       Command.Exports.merge(
         for {
           command <- version.nodes(node_name).commands.iterator
           st <- command_states(version, command).iterator
         } yield st.exports)
 
     def begin_theory(
       node_name: Node.Name,
       id: Document_ID.Exec,
       source: String,
       blobs_info: Command.Blobs_Info
     ): State = {
       if (theories.isDefinedAt(id)) fail
       else {
         val command =
           Command.unparsed(source, theory = true, id = id, node_name = node_name,
             blobs_info = blobs_info)
         copy(theories = theories + (id -> command.empty_state))
       }
     }
 
     def end_theory(id: Document_ID.Exec): (Snapshot, State) =
       theories.get(id) match {
         case None => fail
         case Some(st) =>
           val command = st.command
           val node_name = command.node_name
           val command1 =
             Command.unparsed(command.source, theory = true, id = id, node_name = node_name,
               blobs_info = command.blobs_info, results = st.results, markups = st.markups)
           val state1 = copy(theories = theories - id)
           (state1.snippet(command1), state1)
       }
 
     def assign(
       id: Document_ID.Version,
       edited: List[String],
       update: Assign_Update
     ) : ((List[Node.Name], List[Command]), State) = {
       val version = the_version(id)
 
       val edited_set = edited.toSet
       val edited_nodes =
         (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
 
       def upd(exec_id: Document_ID.Exec, st: Command.State)
           : Option[(Document_ID.Exec, Command.State)] =
         if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
 
       val (changed_commands, new_execs) =
         update.foldLeft((List.empty[Command], execs)) {
           case ((commands1, execs1), (command_id, exec)) =>
             val st = the_static_state(command_id)
             val command = st.command
             val commands2 = command :: commands1
             val execs2 =
               exec match {
                 case Nil => execs1
                 case eval_id :: print_ids =>
                   execs1 ++ upd(eval_id, st) ++
                     (for (id <- print_ids; up <- upd(id, command.empty_state)) yield up)
               }
             (commands2, execs2)
         }
       val new_assignment = the_assignment(version).assign(update)
       val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
 
       ((edited_nodes, changed_commands), new_state)
     }
 
     def is_assigned(version: Version): Boolean =
       assignments.get(version.id) match {
         case Some(assgn) => assgn.is_finished
         case None => false
       }
 
     def is_stable(change: Change): Boolean =
       change.is_finished && is_assigned(change.version.get_finished)
 
     def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail
     def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
     def stable_tip_version: Option[Version] =
       if (is_stable(history.tip)) Some(history.tip.version.get_finished) else None
 
     def continue_history(
       previous: Future[Version],
       edits: List[Edit_Text],
       version: Future[Version]
     ): State = {
       val change = Change.make(previous, edits, version)
       copy(history = history + change)
     }
 
     def remove_versions(retain: Int = 0): (List[Version], State) = {
       history.prune(is_stable, retain) match {
         case Some((dropped, history1)) =>
           val old_versions = dropped.map(change => change.version.get_finished)
           val removing = old_versions.nonEmpty
           val state1 = copy(history = history1, removing_versions = removing)
           (old_versions, state1)
         case None => fail
       }
     }
 
     def removed_versions(removed: List[Document_ID.Version]): State = {
       val versions1 = Version.purge_suppressed(versions -- removed)
 
       val assignments1 = assignments -- removed
       var blobs1_names = Set.empty[Node.Name]
       var blobs1 = Set.empty[SHA1.Digest]
       var commands1 = Map.empty[Document_ID.Command, Command.State]
       var execs1 = Map.empty[Document_ID.Exec, Command.State]
       for {
         (version_id, version) <- versions1.iterator
         command_execs = assignments1(version_id).command_execs
         (_, node) <- version.nodes.iterator
         command <- node.commands.iterator
       } {
         for ((name, digest) <- command.blobs_defined) {
           blobs1_names += name
           blobs1 += digest
         }
 
         if (!commands1.isDefinedAt(command.id))
           commands.get(command.id).foreach(st => commands1 += (command.id -> st))
 
         for (exec_id <- command_execs.getOrElse(command.id, Nil)) {
           if (!execs1.isDefinedAt(exec_id))
             execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
         }
       }
 
       copy(
         versions = versions1,
         blobs = blobs1,
         commands = commands1,
         execs = execs1,
         commands_redirection = commands_redirection.restrict(commands1.keySet),
         assignments = assignments1,
         history = history.purge(versions1),
         removing_versions = false)
     }
 
     def command_maybe_consolidated(version: Version, command: Command): Boolean = {
       require(is_assigned(version), "version not assigned (command_maybe_consolidated)")
       try {
         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match {
           case eval_id :: print_ids =>
             the_dynamic_state(eval_id).maybe_consolidated &&
             !print_ids.exists(print_id => the_dynamic_state(print_id).consolidating)
           case Nil => false
         }
       }
       catch { case _: State.Fail => false }
     }
 
     private def command_states_self(
       version: Version,
       command: Command
     ) : List[(Document_ID.Generic, Command.State)] = {
       require(is_assigned(version), "version not assigned (command_states_self)")
       try {
         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
           .map(id => id -> the_dynamic_state(id)) match {
             case Nil => fail
             case res => res
           }
       }
       catch {
         case _: State.Fail =>
           try { List(command.id -> the_static_state(command.id)) }
           catch { case _: State.Fail => List(command.id -> command.init_state) }
       }
     }
 
     def command_states(version: Version, command: Command): List[Command.State] = {
       val self = command_states_self(version, command)
       val others =
         if (commands_redirection.defined(command.id)) {
           (for {
             command_id <- commands_redirection.imm_succs(command.id).iterator
             (id, st) <- command_states_self(version, the_static_state(command_id).command)
             if !self.exists(_._1 == id)
           } yield (id, st)).toMap.valuesIterator.toList
         }
         else Nil
       self.map(_._2) ::: others.flatMap(_.redirect(command))
     }
 
     def command_results(version: Version, command: Command): Command.Results =
       Command.State.merge_results(command_states(version, command))
 
     def command_markup(version: Version, command: Command, index: Command.Markup_Index,
         range: Text.Range, elements: Markup.Elements): Markup_Tree =
       Command.State.merge_markup(command_states(version, command), index, range, elements)
 
     def xml_markup(
       version: Version,
       node_name: Node.Name,
       range: Text.Range = Text.Range.full,
       elements: Markup.Elements = Markup.Elements.full
     ): XML.Body = {
       val node = version.nodes(node_name)
       if (node_name.is_theory) {
         val markup_index = Command.Markup_Index.markup
         (for {
           command <- node.commands.iterator
           command_range <- command.range.try_restrict(range).iterator
           markup = command_markup(version, command, markup_index, command_range, elements)
           tree <- markup.to_XML(command_range, command.source, elements).iterator
         } yield tree).toList
       }
       else {
-        Text.Range(0, node.source.length).try_restrict(range) match {
+        Text.Range.length(node.source).try_restrict(range) match {
           case None => Nil
           case Some(node_range) =>
             val markup =
               version.nodes.commands_loading(node_name).headOption match {
                 case None => Markup_Tree.empty
                 case Some(command) =>
                   val chunk_name = Symbol.Text_Chunk.File(node_name.node)
                   val markup_index = Command.Markup_Index(false, chunk_name)
                   command_markup(version, command, markup_index, node_range, elements)
               }
             markup.to_XML(node_range, node.source, elements)
         }
       }
     }
 
     def node_initialized(version: Version, name: Node.Name): Boolean =
       name.is_theory &&
       (version.nodes(name).commands.iterator.find(_.potentially_initialized) match {
         case None => false
         case Some(command) => command_states(version, command).headOption.exists(_.initialized)
       })
 
     def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
       name.is_theory &&
       version.nodes(name).commands.reverse.iterator.forall(command_maybe_consolidated(version, _))
 
     def node_consolidated(version: Version, name: Node.Name): Boolean =
       !name.is_theory || {
         val it = version.nodes(name).commands.reverse.iterator
         it.hasNext && command_states(version, it.next()).exists(_.consolidated)
       }
 
     def snapshot(
       node_name: Node.Name = Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil,
       snippet_command: Option[Command] = None
     ): Snapshot = {
       val stable = recent_stable
       val version = stable.version.get_finished
 
       val rev_pending_changes =
         for {
           change <- history.undo_list.takeWhile(_ != stable)
           (name, edits) <- change.rev_edits
           if name == node_name
         } yield edits
 
       val edits =
         rev_pending_changes.foldLeft(pending_edits) {
           case (edits, Node.Edits(es)) => es ::: edits
           case (edits, _) => edits
         }
 
       new Snapshot(this, version, node_name, edits, snippet_command)
     }
 
     def snippet(command: Command): Snapshot =
       snapshot().snippet(command)
   }
 }
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,772 +1,774 @@
 /*  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, output_state: Boolean): List[XML.Elem] = {
     val (states, other) =
       results.iterator.map(_._2).filterNot(Protocol.is_result).toList
         .partition(Protocol.is_state)
     (if (output_state) states else Nil) ::: 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.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.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.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.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 =
+  lazy val spell_checker_include: Markup.Elements =
     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")): _*)
+  lazy val spell_checker_exclude: Markup.Elements =
+    Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
+
+  lazy val spell_checker_elements: Markup.Elements =
+    spell_checker_include ++ 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 :+ _)
           })
 
     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(body, indent = 0)))
 
           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/PIDE/text.scala b/src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala
+++ b/src/Pure/PIDE/text.scala
@@ -1,189 +1,191 @@
 /*  Title:      Pure/PIDE/text.scala
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
 Basic operations on plain text.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 import scala.util.Sorting
 
 
 object Text {
   /* offset */
 
   type Offset = Int
 
 
   /* range -- with total quasi-ordering */
 
   object Range {
     def apply(start: Offset): Range = Range(start, start)
+    def length(text: CharSequence): Range = Range(0, text.length)
 
+    val zero: Range = apply(0)
     val full: Range = apply(0, Integer.MAX_VALUE / 2)
     val offside: Range = apply(-1)
 
     object Ordering extends scala.math.Ordering[Range] {
       def compare(r1: Range, r2: Range): Int = r1 compare r2
     }
   }
 
   sealed case class Range(start: Offset, stop: Offset) {
     // denotation: {start} Un {i. start < i & i < stop}
     if (start > stop)
       error("Bad range: [" + start.toString + ".." + stop.toString + "]")
 
     override def toString: String = "[" + start.toString + ".." + stop.toString + "]"
 
     def length: Offset = stop - start
 
     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     def +(i: Offset): Range = if (i == 0) this else map(_ + i)
     def -(i: Offset): Range = if (i == 0) this else map(_ - i)
 
     def is_singularity: Boolean = start == stop
     def inflate_singularity: Range = if (is_singularity) Range(start, start + 1) else this
 
     def touches(i: Offset): Boolean = start <= i && i <= stop
 
     def contains(i: Offset): Boolean = start == i || start < i && i < stop
     def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
     def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
     def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
 
     def apart(that: Range): Boolean =
       (this.start max that.start) > (this.stop min that.stop)
 
     def restrict(that: Range): Range =
       Range(this.start max that.start, this.stop min that.stop)
 
     def try_restrict(that: Range): Option[Range] =
       if (this apart that) None
       else Some(restrict(that))
 
     def try_join(that: Range): Option[Range] =
       if (this apart that) None
       else Some(Range(this.start min that.start, this.stop max that.stop))
 
     def substring(text: String): String = text.substring(start, stop)
 
     def try_substring(text: String): Option[String] =
       try { Some(substring(text)) }
       catch { case _: IndexOutOfBoundsException => None }
   }
 
 
   /* perspective */
 
   object Perspective {
     val empty: Perspective = Perspective(Nil)
 
     def full: Perspective = Perspective(List(Range.full))
 
     def apply(ranges: List[Range]): Perspective = {
       val result = new mutable.ListBuffer[Range]
       var last: Option[Range] = None
       def ship(next: Option[Range]): Unit = { result ++= last; last = next }
 
       for (range <- ranges.sortBy(_.start)) {
         last match {
           case None => ship(Some(range))
           case Some(last_range) =>
             last_range.try_join(range) match {
               case None => ship(Some(range))
               case joined => last = joined
             }
         }
       }
       ship(None)
       new Perspective(result.toList)
     }
   }
 
   final class Perspective private(
     val ranges: List[Range]  // visible text partitioning in canonical order
   ) {
     def is_empty: Boolean = ranges.isEmpty
     def range: Range =
-      if (is_empty) Range(0)
+      if (is_empty) Range.zero
       else Range(ranges.head.start, ranges.last.stop)
 
     override def hashCode: Int = ranges.hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Perspective => ranges == other.ranges
         case _ => false
       }
     override def toString: String = ranges.toString
   }
 
 
   /* information associated with text range */
 
   sealed case class Info[A](range: Range, info: A) {
     def restrict(r: Range): Info[A] = Info(range.restrict(r), info)
     def try_restrict(r: Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))
 
     def map[B](f: A => B): Info[B] = Info(range, f(info))
   }
 
   type Markup = Info[XML.Elem]
 
 
   /* editing */
 
   object Edit {
     def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
     def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
     def inserts(start: Offset, text: String): List[Edit] =
       if (text == "") Nil else List(insert(start, text))
     def removes(start: Offset, text: String): List[Edit] =
       if (text == "") Nil else List(remove(start, text))
     def replace(start: Offset, old_text: String, new_text: String): List[Edit] =
       if (old_text == new_text) Nil
       else removes(start, old_text) ::: inserts(start, new_text)
   }
 
   final class Edit private(val is_insert: Boolean, val start: Offset, val text: String) {
     override def toString: String =
       (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
 
 
     /* transform offsets */
 
     private def transform(do_insert: Boolean, i: Offset): Offset =
       if (i < start) i
       else if (do_insert) i + text.length
       else (i - text.length) max start
 
     def convert(i: Offset): Offset = transform(is_insert, i)
     def revert(i: Offset): Offset = transform(!is_insert, i)
 
 
     /* edit strings */
 
     private def insert(i: Offset, string: String): String =
       string.substring(0, i) + text + string.substring(i)
 
     private def remove(i: Offset, count: Offset, string: String): String =
       string.substring(0, i) + string.substring(i + count)
 
     def can_edit(string: String, shift: Offset): Boolean =
       shift <= start && start < shift + string.length
 
     def edit(string: String, shift: Offset): (Option[Edit], String) =
       if (!can_edit(string, shift)) (Some(this), string)
       else if (is_insert) (None, insert(start - shift, string))
       else {
         val i = start - shift
         val count = text.length min (string.length - i)
         val rest =
           if (count == text.length) None
           else Some(Edit.remove(start, text.substring(count)))
         (rest, remove(i, count, string))
       }
   }
 }