diff --git a/src/Pure/Admin/build_jdk.scala b/src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala
+++ b/src/Pure/Admin/build_jdk.scala
@@ -1,235 +1,235 @@
 /*  Title:      Pure/Admin/build_jdk.scala
     Author:     Makarius
 
 Build Isabelle jdk component from original platform installations.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 import java.nio.file.Files
 import java.nio.file.attribute.PosixFilePermission
 
 import scala.util.matching.Regex
 
 
 object Build_JDK {
   /* platform and version information */
 
   sealed case class JDK_Platform(
     platform_name: String,
     platform_regex: Regex,
     exe: String = "java",
     macos_home: Boolean = false,
     jdk_version: String = ""
   ) {
     override def toString: String = platform_name
 
     def platform_path: Path = Path.explode(platform_name)
 
     def detect(jdk_dir: Path): Option[JDK_Platform] = {
       val major_version = {
         val Major_Version = """.*jdk(\d+).*$""".r
         val jdk_name = jdk_dir.file.getName
         jdk_name match {
           case Major_Version(s) => s
           case _ => error("Cannot determine major version from " + quote(jdk_name))
         }
       }
 
       val path = jdk_dir + Path.explode("bin") + Path.explode(exe)
       if (path.is_file) {
         val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out
         if (platform_regex.pattern.matcher(file_descr).matches) {
           val Version = ("^(" + major_version + """[0-9.+]+)(?:-LTS)?$""").r
           val version_lines =
             Isabelle_System.bash("strings " + File.bash_path(path)).check
               .out_lines.flatMap({ case Version(s) => Some(s) case _ => None })
           version_lines match {
             case List(jdk_version) => Some(copy(jdk_version = jdk_version))
             case _ => error("Expected unique version within executable " + path)
           }
         }
         else None
       }
       else None
     }
   }
 
   val templates: List[JDK_Platform] =
     List(
       JDK_Platform("arm64-darwin", """.*Mach-O 64-bit.*arm64.*""".r, macos_home = true),
       JDK_Platform("arm64-linux", """.*ELF 64-bit.*ARM aarch64.*""".r),
       JDK_Platform("x86_64-darwin", """.*Mach-O 64-bit.*x86[-_]64.*""".r, macos_home = true),
       JDK_Platform("x86_64-linux", """.*ELF 64-bit.*x86[-_]64.*""".r),
       JDK_Platform("x86_64-windows", """.*PE32\+ executable.*x86[-_]64.*""".r, exe = "java.exe"))
 
 
   /* README */
 
   def readme(jdk_version: String): String =
-"""This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also
+    """This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also
 https://www.azul.com/downloads/zulu-community/?package=jdk
 
 The main license is GPL2, but some modules are covered by other (more liberal)
 licenses, see legal/* for details.
 
 Linux, Windows, macOS all work uniformly, depending on platform-specific
 subdirectories.
 """
 
 
   /* settings */
 
   val settings: String =
-"""# -*- shell-script -*- :mode=shellscript:
+    """# -*- shell-script -*- :mode=shellscript:
 
 case "$ISABELLE_PLATFORM_FAMILY" in
   linux)
     ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
     ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
     ;;
   windows)
     ISABELLE_JAVA_PLATFORM="$ISABELLE_WINDOWS_PLATFORM64"
     ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
     ;;
   macos)
     if [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$COMPONENT/$ISABELLE_APPLE_PLATFORM64" ]
     then
       ISABELLE_JAVA_PLATFORM="$ISABELLE_APPLE_PLATFORM64"
     else
       ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
     fi
     ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
     ;;
 esac
 """
 
 
   /* extract archive */
 
   def extract_archive(dir: Path, archive: Path): JDK_Platform = {
     try {
       val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp"))
 
       if (archive.get_ext == "zip") {
         Isabelle_System.bash(
           "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check
       }
       else {
         Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
       }
 
       val dir_entry =
         File.read_dir(tmp_dir) match {
           case List(s) => s
           case _ => error("Archive contains multiple directories")
         }
 
       val jdk_dir = tmp_dir + Path.explode(dir_entry)
       val platform =
         templates.view.flatMap(_.detect(jdk_dir))
           .headOption.getOrElse(error("Failed to detect JDK platform"))
 
       val platform_dir = dir + platform.platform_path
       if (platform_dir.is_dir) error("Directory already exists: " + platform_dir)
 
       Isabelle_System.move_file(jdk_dir, platform_dir)
 
       platform
     }
     catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for " + archive) }
   }
 
 
   /* build jdk */
 
   def build_jdk(
     archives: List[Path],
     progress: Progress = new Progress,
     target_dir: Path = Path.current
   ): Unit = {
     if (Platform.is_windows) error("Cannot build jdk on Windows")
 
     Isabelle_System.with_tmp_dir("jdk") { dir =>
       progress.echo("Extracting ...")
       val platforms = archives.map(extract_archive(dir, _))
 
       val jdk_version =
         platforms.map(_.jdk_version).distinct match {
           case List(version) => version
           case Nil => error("No archives")
           case versions =>
             error("Archives contain multiple JDK versions: " + commas_quote(versions))
         }
 
       templates.filterNot(p1 => platforms.exists(p2 => p1.platform_name == p2.platform_name))
       match {
         case Nil =>
         case missing => error("Missing platforms: " + commas_quote(missing.map(_.platform_name)))
       }
 
       val jdk_name = "jdk-" + jdk_version
       val jdk_path = Path.explode(jdk_name)
       val component_dir = dir + jdk_path
 
       Isabelle_System.make_directory(component_dir + Path.explode("etc"))
       File.write(Components.settings(component_dir), settings)
       File.write(component_dir + Path.explode("README"), readme(jdk_version))
 
       for (platform <- platforms) {
         Isabelle_System.move_file(dir + platform.platform_path, component_dir)
       }
 
       for (file <- File.find_files(component_dir.file, include_dirs = true)) {
         val path = file.toPath
         val perms = Files.getPosixFilePermissions(path)
         perms.add(PosixFilePermission.OWNER_READ)
         perms.add(PosixFilePermission.GROUP_READ)
         perms.add(PosixFilePermission.OTHERS_READ)
         perms.add(PosixFilePermission.OWNER_WRITE)
         if (file.isDirectory) {
           perms.add(PosixFilePermission.OWNER_WRITE)
           perms.add(PosixFilePermission.OWNER_EXECUTE)
           perms.add(PosixFilePermission.GROUP_EXECUTE)
           perms.add(PosixFilePermission.OTHERS_EXECUTE)
         }
         Files.setPosixFilePermissions(path, perms)
       }
 
       progress.echo("Archiving ...")
       Isabelle_System.gnutar(
         "-czf " + File.bash_path(target_dir + jdk_path.tar.gz) + " " + jdk_name, dir = dir).check
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives",
       Scala_Project.here,
       { args =>
         var target_dir = Path.current
 
         val getopts = Getopts("""
 Usage: isabelle build_jdk [OPTIONS] ARCHIVES...
 
   Options are:
     -D DIR       target directory (default ".")
 
   Build jdk component from tar.gz archives, with original jdk archives
   for Linux, Windows, and macOS.
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)))
 
         val more_args = getopts(args)
         if (more_args.isEmpty) getopts.usage()
 
         val archives = more_args.map(Path.explode)
         val progress = new Console_Progress()
 
         build_jdk(archives = archives, progress = progress, target_dir = target_dir)
       })
 }
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,668 +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))
   }
 
   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] =
+      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)
+      }
+      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/markup_tree.scala b/src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala
+++ b/src/Pure/PIDE/markup_tree.scala
@@ -1,269 +1,269 @@
 /*  Title:      Pure/PIDE/markup_tree.scala
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
 Markup trees over nested / non-overlapping text ranges.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.SortedMap
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 
 object Markup_Tree {
   /* construct trees */
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
   def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree =
     trees.foldLeft(empty)(_.merge(_, range, elements))
 
   def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
     trees match {
       case Nil => empty
       case head :: tail =>
         new Markup_Tree(
           tail.foldLeft(head.branches) {
             case (branches, tree) =>
               tree.branches.foldLeft(branches) {
                 case (bs, (r, entry)) =>
                   require(!bs.isDefinedAt(r), "cannot merge markup trees")
                   bs + (r -> entry)
               }
           })
     }
 
 
   /* tree building blocks */
 
   object Entry {
     def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
       Entry(markup.range, List(markup.info), subtree)
   }
 
   sealed case class Entry(
     range: Text.Range,
     rev_markup: List[XML.Elem],
     subtree: Markup_Tree
   ) {
     def markup: List[XML.Elem] = rev_markup.reverse
 
     def filter_markup(elements: Markup.Elements): List[XML.Elem] = {
       var result: List[XML.Elem] = Nil
       for (elem <- rev_markup if elements(elem.name))
         result ::= elem
       result
     }
 
     def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)
     def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup)
   }
 
   object Branches {
     type T = SortedMap[Text.Range, Entry]
     val empty: T = SortedMap.empty(Text.Range.Ordering)
   }
 
 
   /* XML representation */
 
   @tailrec private def strip_elems(
       elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) =
     body match {
       case List(XML.Wrapped_Elem(markup1, body1, body2)) =>
         strip_elems(XML.Elem(markup1, body1) :: elems, body2)
       case List(XML.Elem(markup1, body1)) =>
         strip_elems(XML.Elem(markup1, Nil) :: elems, body1)
       case _ => (elems, body)
     }
 
   private def make_trees(
     acc: (Int, List[Markup_Tree]),
     tree: XML.Tree
   ): (Int, List[Markup_Tree]) = {
     val (offset, markup_trees) = acc
 
     strip_elems(Nil, List(tree)) match {
       case (Nil, body) =>
         (offset + XML.text_length(body), markup_trees)
 
       case (elems, body) =>
         val (end_offset, subtrees) =
            body.foldLeft((offset, List.empty[Markup_Tree]))(make_trees)
         if (offset == end_offset) acc
         else {
           val range = Text.Range(offset, end_offset)
           val entry = Entry(range, elems, merge_disjoint(subtrees))
           (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
         }
     }
   }
 
   def from_XML(body: XML.Body): Markup_Tree =
     merge_disjoint(body.foldLeft((0, List.empty[Markup_Tree]))(make_trees)._2)
 }
 
 
 final class Markup_Tree private(val branches: Markup_Tree.Branches.T) {
   import Markup_Tree._
 
   private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
     this(branches + (entry.range -> entry))
 
   private def overlapping(range: Text.Range): Branches.T =
     if (branches.isEmpty ||
         (range.contains(branches.firstKey.start) && branches.lastKey.stop <= range.stop))
       branches
     else {
       val start = Text.Range(range.start)
       val stop = Text.Range(range.stop)
       val bs = branches.range(start, stop)
       branches.get(stop) match {
         case Some(end) if range overlaps end.range => bs + (end.range -> end)
         case _ => bs
       }
     }
 
   def restrict(range: Text.Range): Markup_Tree =
     new Markup_Tree(overlapping(range))
 
   def is_empty: Boolean = branches.isEmpty
 
   def + (new_markup: Text.Markup): Markup_Tree = {
     val new_range = new_markup.range
 
     branches.get(new_range) match {
       case None => new Markup_Tree(branches, Entry(new_markup, empty))
       case Some(entry) =>
         if (entry.range == new_range)
           new Markup_Tree(branches, entry + new_markup)
         else if (entry.range.contains(new_range))
           new Markup_Tree(branches, entry \ new_markup)
         else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
           new Markup_Tree(Branches.empty, Entry(new_markup, this))
         else {
           val body = overlapping(new_range)
           if (body.forall(e => new_range.contains(e._1)))
             new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
           else {
             Output.warning("Ignored overlapping markup information: " + new_markup + "\n" +
               body.filter(e => !new_range.contains(e._1)).values.mkString("\n"))
             this
           }
         }
     }
   }
 
   def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree = {
     def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
       tree2.branches.foldLeft(tree1) {
         case (tree, (range, entry)) =>
           if (!range.overlaps(root_range)) tree
           else {
             entry.filter_markup(elements).foldLeft(merge_trees(tree, entry.subtree)) {
               case (t, elem) => t + Text.Info(range, elem)
             }
           }
       }
 
     if (this eq other) this
     else {
       val tree1 = this.restrict(root_range)
       val tree2 = other.restrict(root_range)
       if (tree1.is_empty) tree2
       else merge_trees(tree1, tree2)
     }
   }
 
   def cumulate[A](
     root_range: Text.Range,
     root_info: A,
     elements: Markup.Elements,
     result: (A, Text.Markup) => Option[A]
   ): List[Text.Info[A]] = {
     def results(x: A, entry: Entry): Option[A] = {
       var y = x
       var changed = false
       for {
         elem <- entry.filter_markup(elements)
         y1 <- result(y, Text.Info(entry.range, elem))
       } { y = y1; changed = true }
       if (changed) Some(y) else None
     }
 
     def traverse(
       last: Text.Offset,
       stack: List[(Text.Info[A], List[(Text.Range, Entry)])]
     ): List[Text.Info[A]] = {
       stack match {
         case (parent, (range, entry) :: more) :: rest =>
           val subrange = range.restrict(root_range)
           val subtree = entry.subtree.overlapping(subrange).toList
           val start = subrange.start
 
           results(parent.info, entry) match {
             case Some(res) =>
               val next = Text.Info(subrange, res)
               val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)
               if (last < start) parent.restrict(Text.Range(last, start)) :: nexts
               else nexts
             case None => traverse(last, (parent, subtree ::: more) :: rest)
           }
 
         case (parent, Nil) :: rest =>
           val stop = parent.range.stop
           val nexts = traverse(stop, rest)
           if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts
           else nexts
 
         case Nil =>
           val stop = root_range.stop
           if (last < stop) List(Text.Info(Text.Range(last, stop), root_info))
           else Nil
       }
     }
     traverse(root_range.start,
       List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
   }
 
   def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body = {
     def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
       if (start == stop) Nil
       else List(XML.Text(text.subSequence(start, stop).toString))
 
     def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
       rev_markups.foldLeft(body) {
         case (b, elem) =>
           if (!elements(elem.name)) b
           else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
           else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
       }
 
     def make_body(
       elem_range: Text.Range,
       elem_markup: List[XML.Elem],
       entries: Branches.T
     ) : XML.Body = {
       val body = new mutable.ListBuffer[XML.Tree]
       var last = elem_range.start
       for ((range, entry) <- entries) {
         val subrange = range.restrict(elem_range)
         body ++= make_text(last, subrange.start)
         body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
         last = subrange.stop
       }
       body ++= make_text(last, elem_range.stop)
       make_elems(elem_markup, body.toList)
     }
-   make_body(root_range, Nil, overlapping(root_range))
+    make_body(root_range, Nil, overlapping(root_range))
   }
 
   override def toString: String =
     branches.toList.map(_._2) match {
       case Nil => "Empty"
       case list => list.mkString("Tree(", ",", ")")
     }
 }
diff --git a/src/Pure/Thy/bibtex.scala b/src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala
+++ b/src/Pure/Thy/bibtex.scala
@@ -1,688 +1,688 @@
 /*  Title:      Pure/Thy/bibtex.scala
     Author:     Makarius
 
 BibTeX support.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 import scala.collection.mutable
 import scala.util.parsing.combinator.RegexParsers
 import scala.util.parsing.input.Reader
 
 
 object Bibtex {
   /** file format **/
 
   def is_bibtex(name: String): Boolean = name.endsWith(".bib")
 
   class File_Format extends isabelle.File_Format {
     val format_name: String = "bibtex"
     val file_ext: String = "bib"
 
     override def theory_suffix: String = "bibtex_file"
     override def theory_content(name: String): String =
       """theory "bib" imports Pure begin bibtex_file """ +
         Outer_Syntax.quote_string(name) + """ end"""
 
     override def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = {
       val name = snapshot.node_name
       if (detect(name.node)) {
         val title = "Bibliography " + quote(snapshot.node_name.path.file_name)
         val content =
           Isabelle_System.with_tmp_file("bib", "bib") { bib =>
             File.write(bib, snapshot.node.source)
             Bibtex.html_output(List(bib), style = "unsort", title = title)
           }
         Some(Presentation.HTML_Document(title, content))
       }
       else None
     }
   }
 
 
 
   /** bibtex errors **/
 
   def bibtex_errors(dir: Path, root_name: String): List[String] = {
     val log_path = dir + Path.explode(root_name).ext("blg")
     if (log_path.is_file) {
       val Error1 = """^(I couldn't open database file .+)$""".r
       val Error2 = """^(I found no .+)$""".r
       val Error3 = """^(.+)---line (\d+) of file (.+)""".r
       Line.logical_lines(File.read(log_path)).flatMap(line =>
         line match {
           case Error1(msg) => Some("Bibtex error: " + msg)
           case Error2(msg) => Some("Bibtex error: " + msg)
           case Error3(msg, Value.Int(l), file) =>
             val path = File.standard_path(file)
             if (Path.is_wellformed(path)) {
               val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode)
               Some("Bibtex error" + Position.here(pos) + ":\n  " + msg)
             }
             else None
           case _ => None
         })
     }
     else Nil
   }
 
 
 
   /** check database **/
 
   def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) = {
     val chunks = parse(Line.normalize(database))
     var chunk_pos = Map.empty[String, Position.T]
     val tokens = new mutable.ListBuffer[(Token, Position.T)]
     var line = 1
     var offset = 1
 
     def make_pos(length: Int): Position.T =
       Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line)
 
     def advance_pos(tok: Token): Unit = {
       for (s <- Symbol.iterator(tok.source)) {
         if (Symbol.is_newline(s)) line += 1
         offset += 1
       }
     }
 
     def get_line_pos(l: Int): Position.T =
       if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none
 
     for (chunk <- chunks) {
       val name = chunk.name
       if (name != "" && !chunk_pos.isDefinedAt(name)) {
         chunk_pos += (name -> make_pos(chunk.heading_length))
       }
       for (tok <- chunk.tokens) {
         tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length))
         advance_pos(tok)
       }
     }
 
     Isabelle_System.with_tmp_dir("bibtex") { tmp_dir =>
       File.write(tmp_dir + Path.explode("root.bib"),
         tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n"))
       File.write(tmp_dir + Path.explode("root.aux"),
         "\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}")
       Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file)
 
       val Error = """^(.*)---line (\d+) of file root.bib$""".r
       val Warning = """^Warning--(.+)$""".r
       val Warning_Line = """--line (\d+) of file root.bib$""".r
       val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r
 
       val log_file = tmp_dir + Path.explode("root.blg")
       val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil
 
       val (errors, warnings) =
         if (lines.isEmpty) (Nil, Nil)
         else {
           lines.zip(lines.tail ::: List("")).flatMap(
             {
               case (Error(msg, Value.Int(l)), _) =>
                 Some((true, (msg, get_line_pos(l))))
               case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
                 Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name))))
               case (Warning(msg), Warning_Line(Value.Int(l))) =>
                 Some((false, (Word.capitalize(msg), get_line_pos(l))))
               case (Warning(msg), _) =>
                 Some((false, (Word.capitalize(msg), Position.none)))
               case _ => None
             }
           ).partition(_._1)
         }
       (errors.map(_._2), warnings.map(_._2))
     }
   }
 
   object Check_Database extends Scala.Fun_String("bibtex_check_database") {
     val here = Scala_Project.here
     def apply(database: String): String = {
       import XML.Encode._
       YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
         check_database(database)))
     }
   }
 
 
 
   /** document model **/
 
   /* entries */
 
   def entries(text: String): List[Text.Info[String]] = {
     val result = new mutable.ListBuffer[Text.Info[String]]
     var offset = 0
     for (chunk <- Bibtex.parse(text)) {
       val end_offset = offset + chunk.source.length
       if (chunk.name != "" && !chunk.is_command)
         result += Text.Info(Text.Range(offset, end_offset), chunk.name)
       offset = end_offset
     }
     result.toList
   }
 
   def entries_iterator[A, B <: Document.Model](
     models: Map[A, B]
   ): Iterator[Text.Info[(String, B)]] = {
     for {
       (_, model) <- models.iterator
       info <- model.bibtex_entries.iterator
     } yield info.map((_, model))
   }
 
 
   /* completion */
 
   def completion[A, B <: Document.Model](
     history: Completion.History,
     rendering: Rendering,
     caret: Text.Offset,
     models: Map[A, B]
   ): Option[Completion.Result] = {
     for {
       Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
       name1 <- Completion.clean_name(name)
 
       original <- rendering.get_text(r)
       original1 <- Completion.clean_name(Library.perhaps_unquote(original))
 
       entries =
         (for {
           Text.Info(_, (entry, _)) <- entries_iterator(models)
           if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1
         } yield entry).toList
       if entries.nonEmpty
 
       items =
         entries.sorted.map({
           case entry =>
             val full_name = Long_Name.qualify(Markup.CITATION, entry)
             val description = List(entry, "(BibTeX entry)")
             val replacement = quote(entry)
-          Completion.Item(r, original, full_name, description, replacement, 0, false)
+            Completion.Item(r, original, full_name, description, replacement, 0, false)
         }).sorted(history.ordering).take(rendering.options.int("completion_limit"))
     } yield Completion.Result(r, original, false, items)
   }
 
 
 
   /** content **/
 
   private val months = List(
     "jan",
     "feb",
     "mar",
     "apr",
     "may",
     "jun",
     "jul",
     "aug",
     "sep",
     "oct",
     "nov",
     "dec")
   def is_month(s: String): Boolean = months.contains(s.toLowerCase)
 
   private val commands = List("preamble", "string")
   def is_command(s: String): Boolean = commands.contains(s.toLowerCase)
 
   sealed case class Entry(
     kind: String,
     required: List[String],
     optional_crossref: List[String],
     optional_other: List[String]
   ) {
     val optional_standard: List[String] = List("url", "doi", "ee")
 
     def is_required(s: String): Boolean = required.contains(s.toLowerCase)
     def is_optional(s: String): Boolean =
       optional_crossref.contains(s.toLowerCase) ||
       optional_other.contains(s.toLowerCase) ||
       optional_standard.contains(s.toLowerCase)
 
     def fields: List[String] =
       required ::: optional_crossref ::: optional_other ::: optional_standard
 
     def template: String =
       "@" + kind + "{,\n" + fields.map(x => "  " + x + " = {},\n").mkString + "}\n"
   }
 
   val known_entries: List[Entry] =
     List(
       Entry("Article",
         List("author", "title"),
         List("journal", "year"),
         List("volume", "number", "pages", "month", "note")),
       Entry("InProceedings",
         List("author", "title"),
         List("booktitle", "year"),
         List("editor", "volume", "number", "series", "pages", "month", "address",
           "organization", "publisher", "note")),
       Entry("InCollection",
         List("author", "title", "booktitle"),
         List("publisher", "year"),
         List("editor", "volume", "number", "series", "type", "chapter", "pages",
           "edition", "month", "address", "note")),
       Entry("InBook",
         List("author", "editor", "title", "chapter"),
         List("publisher", "year"),
         List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
       Entry("Proceedings",
         List("title", "year"),
         List(),
         List("booktitle", "editor", "volume", "number", "series", "address", "month",
           "organization", "publisher", "note")),
       Entry("Book",
         List("author", "editor", "title"),
         List("publisher", "year"),
         List("volume", "number", "series", "address", "edition", "month", "note")),
       Entry("Booklet",
         List("title"),
         List(),
         List("author", "howpublished", "address", "month", "year", "note")),
       Entry("PhdThesis",
         List("author", "title", "school", "year"),
         List(),
         List("type", "address", "month", "note")),
       Entry("MastersThesis",
         List("author", "title", "school", "year"),
         List(),
         List("type", "address", "month", "note")),
       Entry("TechReport",
         List("author", "title", "institution", "year"),
         List(),
         List("type", "number", "address", "month", "note")),
       Entry("Manual",
         List("title"),
         List(),
         List("author", "organization", "address", "edition", "month", "year", "note")),
       Entry("Unpublished",
         List("author", "title", "note"),
         List(),
         List("month", "year")),
       Entry("Misc",
         List(),
         List(),
         List("author", "title", "howpublished", "month", "year", "note")))
 
   def get_entry(kind: String): Option[Entry] =
     known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
 
   def is_entry(kind: String): Boolean = get_entry(kind).isDefined
 
 
 
   /** tokens and chunks **/
 
   object Token {
     object Kind extends Enumeration {
       val COMMAND = Value("command")
       val ENTRY = Value("entry")
       val KEYWORD = Value("keyword")
       val NAT = Value("natural number")
       val STRING = Value("string")
       val NAME = Value("name")
       val IDENT = Value("identifier")
       val SPACE = Value("white space")
       val COMMENT = Value("ignored text")
       val ERROR = Value("bad input")
     }
   }
 
   sealed case class Token(kind: Token.Kind.Value, source: String) {
     def is_kind: Boolean =
       kind == Token.Kind.COMMAND ||
       kind == Token.Kind.ENTRY ||
       kind == Token.Kind.IDENT
     def is_name: Boolean =
       kind == Token.Kind.NAME ||
       kind == Token.Kind.IDENT
     def is_ignored: Boolean =
       kind == Token.Kind.SPACE ||
       kind == Token.Kind.COMMENT
     def is_malformed: Boolean =
       kind == Token.Kind.ERROR
     def is_open: Boolean =
       kind == Token.Kind.KEYWORD && (source == "{" || source == "(")
   }
 
   case class Chunk(kind: String, tokens: List[Token]) {
     val source = tokens.map(_.source).mkString
 
     private val content: Option[List[Token]] =
       tokens match {
         case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty =>
           (body.init.filterNot(_.is_ignored), body.last) match {
             case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}"))
             if tok.is_kind => Some(toks)
 
             case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")"))
             if tok.is_kind => Some(toks)
 
             case _ => None
           }
         case _ => None
       }
 
     def name: String =
       content match {
         case Some(tok :: _) if tok.is_name => tok.source
         case _ => ""
       }
 
     def heading_length: Int =
       if (name == "") 1
       else {
         tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length }
       }
 
     def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
     def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
     def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
     def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
   }
 
 
 
   /** parsing **/
 
   // context of partial line-oriented scans
   abstract class Line_Context
   case object Ignored extends Line_Context
   case object At extends Line_Context
   case class Item_Start(kind: String) extends Line_Context
   case class Item_Open(kind: String, end: String) extends Line_Context
   case class Item(kind: String, end: String, delim: Delimited) extends Line_Context
 
   case class Delimited(quoted: Boolean, depth: Int)
   val Closed = Delimited(false, 0)
 
   private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source)
   private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
 
 
   // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
   // module @<Scan for and process a \.{.bib} command or database entry@>.
 
   object Parsers extends RegexParsers {
     /* white space and comments */
 
     override val whiteSpace = "".r
 
     private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)
     private val spaces = rep(space)
 
 
     /* ignored text */
 
     private val ignored: Parser[Chunk] =
       rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ {
         case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
 
     private def ignored_line: Parser[(Chunk, Line_Context)] =
       ignored ^^ { case a => (a, Ignored) }
 
 
     /* delimited string: outermost "..." or {...} and body with balanced {...} */
 
     // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces
     private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] =
       new Parser[(String, Delimited)] {
         require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0,
           "bad delimiter depth")
 
         def apply(in: Input) = {
           val start = in.offset
           val end = in.source.length
 
           var i = start
           var q = delim.quoted
           var d = delim.depth
           var finished = false
           while (!finished && i < end) {
             val c = in.source.charAt(i)
 
             if (c == '"' && d == 0) { i += 1; d = 1; q = true }
             else if (c == '"' && d == 1 && q) {
               i += 1; d = 0; q = false; finished = true
             }
             else if (c == '{') { i += 1; d += 1 }
             else if (c == '}') {
               if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true }
               else {i = start; finished = true }
             }
             else if (d > 0) i += 1
             else finished = true
           }
           if (i == start) Failure("bad input", in)
           else {
             val s = in.source.subSequence(start, i).toString
             Success((s, Delimited(q, d)), in.drop(i - start))
           }
         }
       }.named("delimited_depth")
 
     private def delimited: Parser[Token] =
       delimited_depth(Closed) ^?
         { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
 
     private def recover_delimited: Parser[Token] =
       """["{][^@]*""".r ^^ token(Token.Kind.ERROR)
 
     def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
       delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
         (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } |
       recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) }
 
 
     /* other tokens */
 
     private val at = "@" ^^ keyword
 
     private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT)
 
     private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME)
 
     private val identifier =
       """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r
 
     private val ident = identifier ^^ token(Token.Kind.IDENT)
 
     val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space))
 
 
     /* body */
 
     private val body =
       delimited | (recover_delimited | other_token)
 
     private def body_line(ctxt: Item) =
       if (ctxt.delim.depth > 0)
         delimited_line(ctxt)
       else
         delimited_line(ctxt) |
         other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } |
         ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) }
 
 
     /* items: command or entry */
 
     private val item_kind =
       identifier ^^ { case a =>
         val kind =
           if (is_command(a)) Token.Kind.COMMAND
           else if (is_entry(a)) Token.Kind.ENTRY
           else Token.Kind.IDENT
         Token(kind, a)
       }
 
     private val item_begin =
       "{" ^^ { case a => ("}", keyword(a)) } |
       "(" ^^ { case a => (")", keyword(a)) }
 
     private def item_name(kind: String) =
       kind.toLowerCase match {
         case "preamble" => failure("")
         case "string" => identifier ^^ token(Token.Kind.NAME)
         case _ => name
       }
 
     private val item_start =
       at ~ spaces ~ item_kind ~ spaces ^^
         { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) }
 
     private val item: Parser[Chunk] =
       (item_start ~ item_begin ~ spaces) into
         { case (kind, a) ~ ((end, b)) ~ c =>
             opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ {
               case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } }
 
     private val recover_item: Parser[Chunk] =
       at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
 
 
     /* chunks */
 
     val chunk: Parser[Chunk] = ignored | (item | recover_item)
 
     def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = {
       ctxt match {
         case Ignored =>
           ignored_line |
           at ^^ { case a => (Chunk("", List(a)), At) }
 
         case At =>
           space ^^ { case a => (Chunk("", List(a)), ctxt) } |
           item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } |
           recover_item ^^ { case a => (a, Ignored) } |
           ignored_line
 
         case Item_Start(kind) =>
           space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
           item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } |
           recover_item ^^ { case a => (a, Ignored) } |
           ignored_line
 
         case Item_Open(kind, end) =>
           space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
           item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } |
           body_line(Item(kind, end, Closed)) |
           ignored_line
 
         case item_ctxt: Item =>
           body_line(item_ctxt) |
           ignored_line
 
         case _ => failure("")
       }
     }
   }
 
 
   /* parse */
 
   def parse(input: CharSequence): List[Chunk] =
     Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match {
       case Parsers.Success(result, _) => result
       case _ => error("Unexpected failure to parse input:\n" + input.toString)
     }
 
   def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = {
     var in: Reader[Char] = Scan.char_reader(input)
     val chunks = new mutable.ListBuffer[Chunk]
     var ctxt = context
     while (!in.atEnd) {
       val result = Parsers.parse(Parsers.chunk_line(ctxt), in)
       (result : @unchecked) match {
         case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest
         case Parsers.NoSuccess(_, rest) =>
           error("Unepected failure to parse input:\n" + rest.source.toString)
       }
     }
     (chunks.toList, ctxt)
   }
 
 
 
   /** HTML output **/
 
   private val output_styles =
     List(
       "" -> "html-n",
       "plain" -> "html-n",
       "alpha" -> "html-a",
       "named" -> "html-n",
       "paragraph" -> "html-n",
       "unsort" -> "html-u",
       "unsortlist" -> "html-u")
 
   def html_output(bib: List[Path],
     title: String = "Bibliography",
     body: Boolean = false,
     citations: List[String] = List("*"),
     style: String = "",
     chronological: Boolean = false
   ): String = {
     Isabelle_System.with_tmp_dir("bibtex") { tmp_dir =>
       /* database files */
 
       val bib_files = bib.map(_.drop_ext)
       val bib_names = {
         val names0 = bib_files.map(_.file_name)
         if (Library.duplicates(names0).isEmpty) names0
         else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
       }
 
       for ((a, b) <- bib_files zip bib_names) {
         Isabelle_System.copy_file(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
       }
 
 
       /* style file */
 
       val bst =
         output_styles.toMap.get(style) match {
           case Some(base) => base + (if (chronological) "c" else "") + ".bst"
           case None =>
             error("Bad style for bibtex HTML output: " + quote(style) +
               "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")")
         }
       Isabelle_System.copy_file(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
 
 
       /* result */
 
       val in_file = Path.explode("bib.aux")
       val out_file = Path.explode("bib.html")
 
       File.write(tmp_dir + in_file,
         bib_names.mkString("\\bibdata{", ",", "}\n") +
         citations.map(cite => "\\citation{" + cite + "}\n").mkString)
 
       Isabelle_System.bash(
         "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
           " -u -s " + Bash.string(proper_string(style) getOrElse "empty") +
           (if (chronological) " -c" else "") +
           (if (title != "") " -h " + Bash.string(title) + " " else "") +
           " " + File.bash_path(in_file) + " " + File.bash_path(out_file),
         cwd = tmp_dir.file).check
 
       val html = File.read(tmp_dir + out_file)
 
       if (body) {
         cat_lines(
           split_lines(html).
             dropWhile(line => !line.startsWith("<!-- BEGIN BIBLIOGRAPHY")).reverse.
             dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse)
       }
       else html
     }
   }
 }
diff --git a/src/Pure/Tools/build_docker.scala b/src/Pure/Tools/build_docker.scala
--- a/src/Pure/Tools/build_docker.scala
+++ b/src/Pure/Tools/build_docker.scala
@@ -1,157 +1,153 @@
 /*  Title:      Pure/Tools/build_docker.scala
     Author:     Makarius
 
 Build docker image from Isabelle application bundle for Linux.
 */
 
 package isabelle
 
 
 object Build_Docker {
   private val default_base = "ubuntu"
   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
 
   private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux(?:_arm)?\.tar\.gz$""".r
 
   val packages: List[String] =
     List("curl", "less", "libfontconfig1", "libgomp1", "pwgen", "unzip")
 
   val package_collections: Map[String, List[String]] =
     Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),
       "latex" ->
         List("texlive-fonts-extra", "texlive-font-utils", "texlive-latex-extra", "texlive-science"))
 
   def build_docker(progress: Progress,
     app_archive: String,
     base: String = default_base,
     logic: String = default_logic,
     no_build: Boolean = false,
     entrypoint: Boolean = false,
     output: Option[Path] = None,
     more_packages: List[String] = Nil,
     tag: String = "",
     verbose: Boolean = false
   ): Unit = {
     val isabelle_name =
       app_archive match {
         case Isabelle_Name(name) => name
         case _ => error("Cannot determine Isabelle distribution name from " + app_archive)
       }
     val is_remote = Url.is_wellformed(app_archive)
 
     val dockerfile =
       """## Dockerfile for """ + isabelle_name + """
 
 FROM """ + base + """
 SHELL ["/bin/bash", "-c"]
 
 # packages
 ENV DEBIAN_FRONTEND=noninteractive
 RUN apt-get -y update && \
   apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \
   apt-get clean
 
 # user
 RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd)
 USER isabelle
 
 # Isabelle
 WORKDIR /home/isabelle
-""" +
- (if (is_remote)
-   "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz"
-  else "COPY Isabelle.tar.gz .") +
-"""
+""" + (if (is_remote)
+       "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz"
+      else "COPY Isabelle.tar.gz .") + """
 RUN tar xzf Isabelle.tar.gz && \
   mv """ + isabelle_name + """ Isabelle && \
   sed -i -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
   sed -i -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
   Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \
-  rm Isabelle.tar.gz""" +
- (if (entrypoint) """
+  rm Isabelle.tar.gz""" + (if (entrypoint) """
 
 ENTRYPOINT ["Isabelle/bin/isabelle"]
-"""
-  else "")
+""" else "")
 
     output.foreach(File.write(_, dockerfile))
 
     if (!no_build) {
       Isabelle_System.with_tmp_dir("docker") { tmp_dir =>
         File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
 
         if (is_remote) {
           if (!Url.is_readable(app_archive))
             error("Cannot access remote archive " + app_archive)
         }
         else Isabelle_System.copy_file(Path.explode(app_archive),
           tmp_dir + Path.explode("Isabelle.tar.gz"))
 
         val quiet_option = if (verbose) "" else " -q"
         val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
         progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
           echo = true).check
       }
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("build_docker", "build Isabelle docker image",
       Scala_Project.here,
       { args =>
         var base = default_base
         var entrypoint = false
         var logic = default_logic
         var no_build = false
         var output: Option[Path] = None
         var more_packages: List[String] = Nil
         var verbose = false
         var tag = ""
 
         val getopts = Getopts("""
 Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
 
   Options are:
     -B NAME      base image (default """ + quote(default_base) + """)
     -E           set Isabelle/bin/isabelle as entrypoint
     -P NAME      additional Ubuntu package collection (""" +
           package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """)
     -l NAME      default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
     -n           no docker build
     -o FILE      output generated Dockerfile
     -p NAME      additional Ubuntu package
     -t TAG       docker build tag
     -v           verbose
 
   Build Isabelle docker image with default logic image, using a standard
   Isabelle application archive for Linux (local file or remote URL).
 """,
           "B:" -> (arg => base = arg),
           "E" -> (_ => entrypoint = true),
           "P:" -> (arg =>
             package_collections.get(arg) match {
               case Some(ps) => more_packages :::= ps
               case None => error("Unknown package collection " + quote(arg))
             }),
           "l:" -> (arg => logic = arg),
           "n" -> (_ => no_build = true),
           "o:" -> (arg => output = Some(Path.explode(arg))),
           "p:" -> (arg => more_packages ::= arg),
           "t:" -> (arg => tag = arg),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
         val app_archive =
           more_args match {
             case List(arg) => arg
             case _ => getopts.usage()
           }
 
         build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
           no_build = no_build, entrypoint = entrypoint, output = output,
           more_packages = more_packages, tag = tag, verbose = verbose)
       })
 }
diff --git a/src/Pure/Tools/phabricator.scala b/src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala
+++ b/src/Pure/Tools/phabricator.scala
@@ -1,1055 +1,1055 @@
 /*  Title:      Pure/Tools/phabricator.scala
     Author:     Makarius
 
 Support for Phabricator server, notably for Ubuntu 18.04 LTS.
 
 See also:
   - https://www.phacility.com/phabricator
   - https://secure.phabricator.com/book/phabricator
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 import scala.util.matching.Regex
 
 
 object Phabricator {
   /** defaults **/
 
   /* required packages */
 
   val packages_ubuntu_20_04: List[String] =
     Build_Docker.packages :::
     List(
       // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61
       "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql",
       "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring",
       // more packages
       "php-xml", "php-zip", "python3-pygments", "ssh", "subversion", "python-pygments",
       // mercurial build packages
       "make", "gcc", "python", "python2-dev", "python-docutils", "python-openssl")
 
   def packages: List[String] = {
     val release = Linux.Release()
     if (release.is_ubuntu_20_04) packages_ubuntu_20_04
     else error("Bad Linux version: expected Ubuntu 20.04 LTS")
   }
 
 
   /* global system resources */
 
   val www_user = "www-data"
 
   val daemon_user = "phabricator"
 
   val sshd_config: Path = Path.explode("/etc/ssh/sshd_config")
 
 
   /* installation parameters */
 
   val default_name = "vcs"
 
   def phabricator_name(name: String = "", ext: String = ""): String =
     "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext)
 
   def isabelle_phabricator_name(name: String = "", ext: String = ""): String =
     "isabelle-" + phabricator_name(name = name, ext = ext)
 
   def default_root(name: String): Path =
     Path.explode("/var/www") + Path.basic(phabricator_name(name = name))
 
   def default_repo(name: String): Path = default_root(name) + Path.basic("repo")
 
   val default_mailers: Path = Path.explode("mailers.json")
 
   val default_system_port: Int = SSH.default_port
   val alternative_system_port = 222
   val default_server_port = 2222
 
   val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz"
 
 
 
   /** global configuration **/
 
   val global_config: Path = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
 
   def global_config_script(
     init: String = "",
     body: String = "",
     exit: String = ""): String = {
 """#!/bin/bash
 """ + (if (init.nonEmpty) "\n" + init else "") + """
 {
   while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   do
     NAME="$(echo "$REPLY" | cut -d: -f1)"
     ROOT="$(echo "$REPLY" | cut -d: -f2)"
     {
 """ + Library.indent_lines(6, body) + """
     } < /dev/null
   done
 } < """ + File.bash_path(global_config) + "\n" +
     (if (exit.nonEmpty) "\n" + exit + "\n" else "")
   }
 
   sealed case class Config(name: String, root: Path) {
     def home: Path = root + Path.explode(phabricator_name())
 
     def execute(command: String): Process_Result =
       Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check
   }
 
   def read_config(): List[Config] = {
     if (global_config.is_file) {
       for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty)
       yield {
         space_explode(':', entry) match {
           case List(name, root) => Config(name, Path.explode(root))
           case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry))
         }
       }
     }
     else Nil
   }
 
   def write_config(configs: List[Config]): Unit = {
     File.write(global_config,
       configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n"))
   }
 
   def get_config(name: String): Config =
     read_config().find(config => config.name == name) getOrElse
       error("Bad Isabelle/Phabricator installation " + quote(name))
 
 
 
   /** administrative tools **/
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool1 =
     Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory",
       Scala_Project.here,
       { args =>
         var list = false
         var name = default_name
 
         val getopts = Getopts("""
 Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]
 
   Options are:
     -l           list available Phabricator installations
     -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
 
   Invoke a command-line tool within the home directory of the named
   Phabricator installation.
 """,
           "l" -> (_ => list = true),
           "n:" -> (arg => name = arg))
 
         val more_args = getopts(args)
         if (more_args.isEmpty && !list) getopts.usage()
 
         val progress = new Console_Progress
 
         if (list) {
           for (config <- read_config()) {
             progress.echo("phabricator " + quote(config.name) + " root " + config.root)
           }
         }
         else {
           val config = get_config(name)
           val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true)
           if (!result.ok) error(result.print_return_code)
         }
       })
 
 
 
   /** setup **/
 
   def user_setup(name: String, description: String, ssh_setup: Boolean = false): Unit = {
     if (!Linux.user_exists(name)) {
       Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup)
     }
     else if (Linux.user_description(name) != description) {
       error("User " + quote(name) + " already exists --" +
         " for Phabricator it should have the description:\n  " + quote(description))
     }
   }
 
   def command_setup(name: String,
     init: String = "",
     body: String = "",
     exit: String = ""
   ): Path = {
     val command = Path.explode("/usr/local/bin") + Path.basic(name)
     File.write(command, global_config_script(init = init, body = body, exit = exit))
     Isabelle_System.chmod("755", command)
     Isabelle_System.chown("root:root", command)
     command
   }
 
   def mercurial_setup(mercurial_source: String, progress: Progress = new Progress): Unit = {
     progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...")
     Isabelle_System.with_tmp_dir("mercurial") { tmp_dir =>
       val archive =
         if (Url.is_wellformed(mercurial_source)) {
           val archive = tmp_dir + Path.basic("mercurial.tar.gz")
           Isabelle_System.download_file(mercurial_source, archive)
           archive
         }
         else Path.explode(mercurial_source)
 
       Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
       val build_dir = tmp_dir + Path.basic(File.get_dir(tmp_dir))
 
       progress.bash("make all && make install", cwd = build_dir.file, echo = true).check
     }
   }
 
   def phabricator_setup(
     options: Options,
     name: String = default_name,
     root: String = "",
     repo: String = "",
     package_update: Boolean = false,
     mercurial_source: String = "",
     progress: Progress = new Progress
   ): Unit = {
     /* system environment */
 
     Linux.check_system_root()
 
     progress.echo("System packages ...")
 
     if (package_update) {
       Linux.package_update(progress = progress)
       Linux.check_reboot_required()
     }
 
     Linux.package_install(packages, progress = progress)
     Linux.check_reboot_required()
 
 
     if (mercurial_source.nonEmpty) {
       for { name <- List("mercurial", "mercurial-common") if Linux.package_installed(name) } {
         error("Cannot install Mercurial from source:\n" +
           "package package " + quote(name) + " already installed")
       }
       mercurial_setup(mercurial_source, progress = progress)
     }
 
 
     /* users */
 
     if (name.exists((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) ||
         Set("", "ssh", "phd", "dump", daemon_user).contains(name)) {
       error("Bad installation name: " + quote(name))
     }
 
     user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true)
     user_setup(name, "Phabricator SSH User")
 
 
     /* basic installation */
 
     progress.echo("\nPhabricator installation ...")
 
     val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name)
     val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name)
 
     val configs = read_config()
 
     for (config <- configs if config.name == name) {
       error("Duplicate Phabricator installation " + quote(name) + " in " + config.root)
     }
 
     if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) {
       error("Failed to create root directory " + root_path)
     }
 
     Isabelle_System.chown(Bash.string(www_user) + ":" + Bash.string(www_user), root_path)
     Isabelle_System.chmod("755", root_path)
 
     progress.bash(cwd = root_path.file, echo = true,
       script = """
         set -e
         echo "Cloning distribution repositories:"
 
         git clone --branch stable https://github.com/phacility/arcanist.git
         git -C arcanist reset --hard """ +
           Bash.string(options.string("phabricator_version_arcanist")) + """
 
         git clone --branch stable https://github.com/phacility/phabricator.git
         git -C phabricator reset --hard """ +
           Bash.string(options.string("phabricator_version_phabricator")) + """
       """).check
 
     val config = Config(name, root_path)
     write_config(configs ::: List(config))
 
     config.execute("config set pygments.enabled true")
 
 
     /* local repository directory */
 
     progress.echo("\nRepository hosting setup ...")
 
     if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) {
       error("Failed to create local repository directory " + repo_path)
     }
 
     Isabelle_System.chown(
       "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path)
     Isabelle_System.chmod("755", repo_path)
 
     config.execute("config set repository.default-local-path " + File.bash_path(repo_path))
 
 
     val sudoers_file =
       Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name(name = name))
     File.write(sudoers_file,
       www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" +
       name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n")
 
     Isabelle_System.chmod("440", sudoers_file)
 
     config.execute("config set diffusion.ssh-user " + Bash.string(config.name))
 
 
     /* MySQL setup */
 
     progress.echo("\nMySQL setup ...")
 
     File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")),
 """[mysqld]
 max_allowed_packet = 32M
 innodb_buffer_pool_size = 1600M
 local_infile = 0
 """)
 
     Linux.service_restart("mysql")
 
 
     def mysql_conf(R: Regex, which: String): String = {
       val conf = Path.explode("/etc/mysql/debian.cnf")
       split_lines(File.read(conf)).collectFirst({ case R(a) => a }) match {
         case Some(res) => res
         case None => error("Cannot determine " + which + " from " + conf)
       }
     }
 
     val mysql_root_user = mysql_conf("""^user\s*=\s*(\S*)\s*$""".r, "superuser name")
     val mysql_root_password = mysql_conf("""^password\s*=\s*(\S*)\s*$""".r, "superuser password")
 
     val mysql_name = phabricator_name(name = name).replace("-", "_")
     val mysql_user_string = SQL.string(mysql_name) + "@'localhost'"
     val mysql_password = Linux.generate_password()
 
     Isabelle_System.bash("mysql --user=" + Bash.string(mysql_root_user) +
       " --password=" + Bash.string(mysql_root_password) + " --execute=" +
       Bash.string(
         """DROP USER IF EXISTS """ + mysql_user_string + "; " +
         """CREATE USER """ + mysql_user_string +
         """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ +
         """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") +
         """`.* TO """ + mysql_user_string + ";" +
         """GRANT PROCESS ON *.* TO """ + mysql_user_string + ";")).check
 
     config.execute("config set mysql.user " + Bash.string(mysql_name))
     config.execute("config set mysql.pass " + Bash.string(mysql_password))
 
     config.execute("config set phabricator.cache-namespace " + Bash.string(mysql_name))
     config.execute("config set storage.default-namespace " + Bash.string(mysql_name))
     config.execute("config set storage.mysql-engine.max-size 8388608")
 
     progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check
 
 
     /* database dump */
 
     val dump_name = isabelle_phabricator_name(name = "dump")
     command_setup(dump_name, body =
 """mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database"
 [ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz"
 echo -n "Creating $ROOT/database/dump.sql.gz ..."
 "$ROOT/phabricator/bin/storage" dump --compress --output "$ROOT/database/dump.sql.gz" 2>&1 | fgrep -v '[Warning] Using a password on the command line interface can be insecure'
 echo " $(ls -hs "$ROOT/database/dump.sql.gz" | cut -d" " -f1)" """)
 
 
     /* Phabricator upgrade */
 
     command_setup(isabelle_phabricator_name(name = "upgrade"),
       init =
 """BRANCH="${1:-stable}"
 if [ "$BRANCH" != "master" -a "$BRANCH" != "stable" ]
 then
   echo "Bad branch: \"$BRANCH\""
   exit 1
 fi
 
 systemctl stop isabelle-phabricator-phd
 systemctl stop apache2
 """,
       body =
 """echo -e "\nUpgrading phabricator \"$NAME\" root \"$ROOT\" ..."
 for REPO in arcanist phabricator
 do
   cd "$ROOT/$REPO"
   echo -e "\nUpdating \"$REPO\" ..."
   git checkout "$BRANCH"
   git pull
 done
 echo -e "\nUpgrading storage ..."
 "$ROOT/phabricator/bin/storage" upgrade --force
 """,
       exit =
 """systemctl start apache2
 systemctl start isabelle-phabricator-phd""")
 
 
     /* PHP setup */
 
     val php_version =
       Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""")
         .check.out
 
     val php_conf =
       Path.explode("/etc/php") + Path.basic(php_version) +  // educated guess
         Path.explode("apache2/conf.d") +
         Path.basic(isabelle_phabricator_name(ext = "ini"))
 
     File.write(php_conf,
       "post_max_size = 32M\n" +
       "opcache.validate_timestamps = 0\n" +
       "memory_limit = 512M\n" +
       "max_execution_time = 120\n")
 
 
     /* Apache setup */
 
     progress.echo("Apache setup ...")
 
     val apache_root = Path.explode("/etc/apache2")
     val apache_sites = apache_root + Path.explode("sites-available")
 
     if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites)
 
     val server_name = phabricator_name(name = name, ext = "lvh.me")  // alias for "localhost" for testing
     val server_url = "http://" + server_name
 
     File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")),
 """<VirtualHost *:80>
     ServerName """ + server_name + """
     ServerAdmin webmaster@localhost
     DocumentRoot """ + config.home.implode + """/webroot
 
     ErrorLog ${APACHE_LOG_DIR}/error.log
     CustomLog ${APACHE_LOG_DIR}/access.log combined
 
     RewriteEngine on
     RewriteRule ^(.*)$  /index.php?__path__=$1  [B,L,QSA]
 </VirtualHost>
 
 # vim: syntax=apache ts=4 sw=4 sts=4 sr noet
 """)
 
     Isabelle_System.bash( """
       set -e
       a2enmod rewrite
       a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check
 
     config.execute("config set phabricator.base-uri " + Bash.string(server_url))
 
     Linux.service_restart("apache2")
 
     progress.echo("\nFurther manual configuration via " + server_url)
 
 
     /* PHP daemon */
 
     progress.echo("\nPHP daemon setup ...")
 
     val phd_log_path = Isabelle_System.make_directory(Path.explode("/var/tmp/phd"))
     Isabelle_System.chown(
       "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path)
     Isabelle_System.chmod("755", phd_log_path)
 
     config.execute("config set phd.user " + Bash.string(daemon_user))
     config.execute("config set phd.log-directory /var/tmp/phd/" +
       isabelle_phabricator_name(name = name) + "/log")
 
     val phd_name = isabelle_phabricator_name(name = "phd")
     Linux.service_shutdown(phd_name)
     val phd_command = command_setup(phd_name, body = """"$ROOT/phabricator/bin/phd" "$@" """)
     try {
       Linux.service_install(phd_name,
 """[Unit]
 Description=PHP daemon manager for Isabelle/Phabricator
 After=syslog.target network.target apache2.service mysql.service
 
 [Service]
 Type=oneshot
 User=""" + daemon_user + """
 Group=""" + daemon_user + """
 Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin
 ExecStart=""" + phd_command.implode + """ start --force
 ExecStop=""" + phd_command.implode + """ stop
 RemainAfterExit=yes
 
 [Install]
 WantedBy=multi-user.target
 """)
     }
     catch {
       case ERROR(msg) =>
         progress.bash("bin/phd status", cwd = config.home.file, echo = true).check
         error(msg)
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool2 =
     Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux",
       Scala_Project.here,
       { args =>
         var mercurial_source = ""
         var repo = ""
         var package_update = false
         var name = default_name
         var options = Options.init()
         var root = ""
 
         val getopts = Getopts("""
 Usage: isabelle phabricator_setup [OPTIONS]
 
   Options are:
     -M SOURCE    install Mercurial from source: local PATH, or URL, or ":" for
                  """ + standard_mercurial_source + """
     -R DIR       repository directory (default: """ + default_repo("NAME") + """)
     -U           full update of system packages before installation
     -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -r DIR       installation root directory (default: """ + default_root("NAME") + """)
 
   Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP).
 
   The installation name (default: """ + quote(default_name) + """) is mapped to a regular
   Unix user; this is relevant for public SSH access.
 """,
           "M:" -> (arg => mercurial_source = (if (arg == ":") standard_mercurial_source else arg)),
           "R:" -> (arg => repo = arg),
           "U" -> (_ => package_update = true),
           "n:" -> (arg => name = arg),
           "o:" -> (arg => options = options + arg),
           "r:" -> (arg => root = arg))
 
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
         val progress = new Console_Progress
 
         phabricator_setup(options, name = name, root = root, repo = repo,
           package_update = package_update, mercurial_source = mercurial_source, progress = progress)
       })
 
 
 
   /** setup mail **/
 
   val mailers_template: String =
-"""[
+    """[
   {
     "key": "example.org",
     "type": "smtp",
     "options": {
       "host": "mail.example.org",
       "port": 465,
       "user": "phabricator@example.org",
       "password": "********",
       "protocol": "ssl",
       "message-id": true
     }
   }
 ]"""
 
   def phabricator_setup_mail(
     name: String = default_name,
     config_file: Option[Path] = None,
     test_user: String = "",
     progress: Progress = new Progress
   ): Unit = {
     Linux.check_system_root()
 
     val config = get_config(name)
     val default_config_file = config.root + default_mailers
 
     val mail_config = config_file getOrElse default_config_file
 
     def setup_mail: Unit = {
       progress.echo("Using mail configuration from " + mail_config)
       config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config))
 
       if (test_user.nonEmpty) {
         progress.echo("Sending test mail to " + quote(test_user))
         progress.bash(cwd = config.home.file, echo = true,
           script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ +
             Bash.string(test_user)).check
       }
     }
 
     if (config_file.isEmpty) {
       if (!default_config_file.is_file) {
         File.write(default_config_file, mailers_template)
         Isabelle_System.chmod("600", default_config_file)
       }
       if (File.read(default_config_file) == mailers_template) {
         progress.echo("Please invoke the tool again, after providing details in\n  " +
           default_config_file.implode + "\n")
       }
       else setup_mail
     }
     else setup_mail
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool3 =
     Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phabricator installation",
       Scala_Project.here,
       { args =>
         var test_user = ""
         var name = default_name
         var config_file: Option[Path] = None
 
         val getopts = Getopts("""
 Usage: isabelle phabricator_setup_mail [OPTIONS]
 
   Options are:
     -T USER      send test mail to Phabricator user
     -f FILE      config file (default: """ + default_mailers + """ within Phabricator root)
     -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
 
   Provide mail configuration for existing Phabricator installation.
 """,
           "T:" -> (arg => test_user = arg),
           "f:" -> (arg => config_file = Some(Path.explode(arg))),
           "n:" -> (arg => name = arg))
 
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
         val progress = new Console_Progress
 
         phabricator_setup_mail(name = name, config_file = config_file,
           test_user = test_user, progress = progress)
       })
 
 
 
   /** setup ssh **/
 
   /* sshd config */
 
   private val Port = """^\s*Port\s+(\d+)\s*$""".r
   private val No_Port = """^#\s*Port\b.*$""".r
   private val Any_Port = """^#?\s*Port\b.*$""".r
 
   def conf_ssh_port(port: Int): String =
     if (port == SSH.default_port) "#Port " + SSH.default_port else "Port " + port
 
   def read_ssh_port(conf: Path): Int = {
     val lines = split_lines(File.read(conf))
     val ports =
       lines.flatMap({
         case Port(Value.Int(p)) => Some(p)
         case No_Port() => Some(SSH.default_port)
         case _ => None
       })
     ports match {
       case List(port) => port
       case Nil => error("Missing Port specification in " + conf)
       case _ => error("Multiple Port specifications in " + conf)
     }
   }
 
   def write_ssh_port(conf: Path, port: Int): Boolean = {
     val old_port = read_ssh_port(conf)
     if (old_port == port) false
     else {
       val lines = split_lines(File.read(conf))
       val lines1 = lines.map({ case Any_Port() => conf_ssh_port(port) case line => line })
       File.write(conf, cat_lines(lines1))
       true
     }
   }
 
 
   /* phabricator_setup_ssh */
 
   def phabricator_setup_ssh(
     server_port: Int = default_server_port,
     system_port: Int = default_system_port,
     progress: Progress = new Progress
   ): Unit = {
     Linux.check_system_root()
 
     val configs = read_config()
 
     if (server_port == system_port) {
       error("Port for Phabricator sshd coincides with system port: " + system_port)
     }
 
     val sshd_conf_system = Path.explode("/etc/ssh/sshd_config")
     val sshd_conf_server = sshd_conf_system.ext(isabelle_phabricator_name())
 
     val ssh_name = isabelle_phabricator_name(name = "ssh")
     Linux.service_shutdown(ssh_name)
 
     val old_system_port = read_ssh_port(sshd_conf_system)
     if (old_system_port != system_port) {
       progress.echo("Reconfigurig system ssh service")
       Linux.service_shutdown("ssh")
       write_ssh_port(sshd_conf_system, system_port)
       Linux.service_start("ssh")
     }
 
     progress.echo("Configuring " + ssh_name + " service")
 
     val ssh_command = command_setup(ssh_name, body =
 """if [ "$1" = "$NAME" ]
 then
   exec "$ROOT/phabricator/bin/ssh-auth" "$@"
 fi""", exit = "exit 1")
 
     File.write(sshd_conf_server,
 """# OpenBSD Secure Shell server for Isabelle/Phabricator
 AuthorizedKeysCommand """ + ssh_command.implode + """
 AuthorizedKeysCommandUser """ + daemon_user + """
 AuthorizedKeysFile none
 AllowUsers """ + configs.map(_.name).mkString(" ") + """
 Port """ + server_port + """
 Protocol 2
 PermitRootLogin no
 AllowAgentForwarding no
 AllowTcpForwarding no
 PrintMotd no
 PrintLastLog no
 PasswordAuthentication no
 ChallengeResponseAuthentication no
 PidFile /var/run/""" + ssh_name + """.pid
 """)
 
     Linux.service_install(ssh_name,
 """[Unit]
 Description=OpenBSD Secure Shell server for Isabelle/Phabricator
 After=network.target auditd.service
 ConditionPathExists=!/etc/ssh/sshd_not_to_be_run
 
 [Service]
 EnvironmentFile=-/etc/default/ssh
 ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
 ExecStart=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -D $SSHD_OPTS
 ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
 ExecReload=/bin/kill -HUP $MAINPID
 KillMode=process
 Restart=on-failure
 RestartPreventExitStatus=255
 Type=notify
 RuntimeDirectory=sshd-phabricator
 RuntimeDirectoryMode=0755
 
 [Install]
 WantedBy=multi-user.target
 Alias=""" + ssh_name + """.service
 """)
 
     for (config <- configs) {
       progress.echo("phabricator " + quote(config.name) + " port " +  server_port)
       config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString))
       if (server_port == SSH.default_port) config.execute("config delete diffusion.ssh-port")
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool4 =
     Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phabricator installations",
       Scala_Project.here,
       { args =>
         var server_port = default_server_port
         var system_port = default_system_port
 
         val getopts = Getopts("""
 Usage: isabelle phabricator_setup_ssh [OPTIONS]
 
   Options are:
     -p PORT      sshd port for Phabricator servers (default: """ + default_server_port + """)
     -q PORT      sshd port for the operating system (default: """ + default_system_port + """)
 
   Configure ssh service for all Phabricator installations: a separate sshd
   is run in addition to the one of the operating system, and ports need to
   be distinct.
 
   A particular Phabricator installation is addressed by using its
   name as the ssh user; the actual Phabricator user is determined via
   stored ssh keys.
 """,
           "p:" -> (arg => server_port = Value.Int.parse(arg)),
           "q:" -> (arg => system_port = Value.Int.parse(arg)))
 
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
         val progress = new Console_Progress
 
         phabricator_setup_ssh(
           server_port = server_port, system_port = system_port, progress = progress)
       })
 
 
 
   /** conduit API **/
 
   object API {
     /* user information */
 
     sealed case class User(
       id: Long,
       phid: String,
       name: String,
       real_name: String,
       roles: List[String]
     ) {
       def is_valid: Boolean =
         roles.contains("verified") &&
         roles.contains("approved") &&
         roles.contains("activated")
       def is_admin: Boolean = roles.contains("admin")
       def is_regular: Boolean = !(roles.contains("bot") || roles.contains("list"))
     }
 
 
     /* repository information */
 
     sealed case class Repository(
       vcs: VCS.Value,
       id: Long,
       phid: String,
       name: String,
       callsign: String,
       short_name: String,
       importing: Boolean,
       ssh_url: String
     ) {
       def is_hg: Boolean = vcs == VCS.hg
     }
 
     object VCS extends Enumeration {
       val hg, git, svn = Value
       def read(s: String): Value =
         try { withName(s) }
         catch { case _: java.util.NoSuchElementException => error("Unknown vcs type " + quote(s)) }
     }
 
     def edits(typ: String, value: JSON.T): List[JSON.Object.T] =
       List(JSON.Object("type" -> typ, "value" -> value))
 
     def opt_edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] =
       value.toList.flatMap(edits(typ, _))
 
 
     /* result with optional error */
 
     sealed case class Result(result: JSON.T, error: Option[String]) {
       def ok: Boolean = error.isEmpty
       def get: JSON.T = if (ok) result else Exn.error(error.get)
 
       def get_value[A](unapply: JSON.T => Option[A]): A =
         unapply(get) getOrElse Exn.error("Bad JSON result: " + JSON.Format(result))
 
       def get_string: String = get_value(JSON.Value.String.unapply)
     }
 
     def make_result(json: JSON.T): Result = {
       val result = JSON.value(json, "result").getOrElse(JSON.Object.empty)
       val error_info = JSON.string(json, "error_info")
       val error_code = JSON.string(json, "error_code")
       Result(result, error_info orElse error_code)
     }
 
 
     /* context for operations */
 
     def apply(user: String, host: String, port: Int = SSH.default_port): API =
       new API(user, host, port)
   }
 
   final class API private(ssh_user: String, ssh_host: String, ssh_port: Int) {
     /* connection */
 
     require(ssh_host.nonEmpty && ssh_port >= 0, "bad ssh host or port")
 
     private def ssh_user_prefix: String = SSH.user_prefix(ssh_user)
     private def ssh_port_suffix: String = SSH.port_suffix(ssh_port)
 
     override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix
     def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix
 
 
     /* execute methods */
 
     def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T = {
       Isabelle_System.with_tmp_file("params", "json") { params_file =>
         File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params))))
         val result =
           Isabelle_System.bash(
             "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) +
             " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check
         JSON.parse(result.out, strict = false)
       }
     }
 
     def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result =
       API.make_result(execute_raw(method, params = params))
 
     def execute_search[A](
       method: String,
       params: JSON.Object.T,
       unapply: JSON.T => Option[A]
     ): List[A] = {
       val results = new mutable.ListBuffer[A]
       var after = ""
 
       var cont = true
       while (cont) {
         val result =
           execute(method, params = params ++ JSON.optional("after" -> proper_string(after)))
         results ++= result.get_value(JSON.list(_, "data", unapply))
         after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after")))
         cont = after.nonEmpty
       }
 
       results.toList
     }
 
     def ping(): String = execute("conduit.ping").get_string
 
 
     /* users */
 
     lazy val user_phid: String = execute("user.whoami").get_value(JSON.string(_, "phid"))
     lazy val user_name: String = execute("user.whoami").get_value(JSON.string(_, "userName"))
 
     def get_users(
       all: Boolean = false,
       phid: String = "",
       name: String = ""
     ): List[API.User] = {
       val constraints: JSON.Object.T =
         (for { (key, value) <- List("phids" -> phid, "usernames" -> name) if value.nonEmpty }
           yield (key, List(value))).toMap
 
       execute_search("user.search",
           JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints),
             data => JSON.value(data, "fields", fields =>
               for {
                 id <- JSON.long(data, "id")
                 phid <- JSON.string(data, "phid")
                 name <- JSON.string(fields, "username")
                 real_name <- JSON.string0(fields, "realName")
                 roles <- JSON.strings(fields, "roles")
               } yield API.User(id, phid, name, real_name, roles)))
     }
 
     def the_user(phid: String): API.User =
       get_users(phid = phid) match {
         case List(user) => user
         case _ => error("Bad user PHID " + quote(phid))
       }
 
 
     /* repositories */
 
     def get_repositories(
       all: Boolean = false,
       phid: String = "",
       callsign: String = "",
       short_name: String = ""
     ): List[API.Repository] = {
       val constraints: JSON.Object.T =
         (for {
           (key, value) <- List("phids" -> phid, "callsigns" -> callsign, "shortNames" -> short_name)
           if value.nonEmpty
         } yield (key, List(value))).toMap
 
       execute_search("diffusion.repository.search",
           JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints),
             data => JSON.value(data, "fields", fields =>
               for {
                 vcs_name <- JSON.string(fields, "vcs")
                 id <- JSON.long(data, "id")
                 phid <- JSON.string(data, "phid")
                 name <- JSON.string(fields, "name")
                 callsign <- JSON.string0(fields, "callsign")
                 short_name <- JSON.string0(fields, "shortName")
                 importing <- JSON.bool(fields, "isImporting")
               }
               yield {
                 val vcs = API.VCS.read(vcs_name)
                 val url_path =
                   if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name
                 val ssh_url =
                   vcs match {
                     case API.VCS.hg => hg_url + url_path
                     case API.VCS.git => hg_url + url_path + ".git"
                     case API.VCS.svn => ""
                   }
                 API.Repository(vcs, id, phid, name, callsign, short_name, importing, ssh_url)
               }))
     }
 
     def the_repository(phid: String): API.Repository =
       get_repositories(phid = phid) match {
         case List(repo) => repo
         case _ => error("Bad repository PHID " + quote(phid))
       }
 
     def create_repository(
       name: String,
       callsign: String = "",    // unique name, UPPERCASE
       short_name: String = "",  // unique name
       description: String = "",
       public: Boolean = false,
       vcs: API.VCS.Value = API.VCS.hg
     ): API.Repository = {
       require(name.nonEmpty, "bad repository name")
 
       val transactions =
         API.edits("vcs", vcs.toString) :::
         API.edits("name", name) :::
         API.opt_edits("callsign", proper_string(callsign)) :::
         API.opt_edits("shortName", proper_string(short_name)) :::
         API.opt_edits("description", proper_string(description)) :::
         (if (public) Nil
          else API.edits("view", user_phid) ::: API.edits("policy.push", user_phid)) :::
         API.edits("status", "active")
 
       val phid =
         execute("diffusion.repository.edit", params = JSON.Object("transactions" -> transactions))
           .get_value(JSON.value(_, "object", JSON.string(_, "phid")))
 
       execute("diffusion.looksoon", params = JSON.Object("repositories" -> List(phid))).get
 
       the_repository(phid)
     }
   }
 }
diff --git a/src/Pure/Tools/scala_project.scala b/src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala
+++ b/src/Pure/Tools/scala_project.scala
@@ -1,298 +1,298 @@
 /*  Title:      Pure/Tools/scala_project.scala
     Author:     Makarius
 
 Manage Isabelle/Scala/Java project sources, with output to Gradle or
 Maven for IntelliJ IDEA.
 */
 
 package isabelle
 
 
 object Scala_Project {
   /** build tools **/
 
   val java_version: String = "17"
   val scala_version: String = "3.1.3"
 
   abstract class Build_Tool {
     def project_root: Path
     def init_project(dir: Path, jars: List[Path]): Unit
 
     val java_src_dir: Path = Path.explode("src/main/java")
     val scala_src_dir: Path = Path.explode("src/main/scala")
 
     def detect_project(dir: Path): Boolean =
       (dir + project_root).is_file &&
       (dir + scala_src_dir).is_dir
 
     def package_dir(source_file: Path): Path = {
       val dir =
         package_name(source_file) match {
           case Some(name) => Path.explode(space_explode('.', name).mkString("/"))
           case None => error("Failed to guess package from " + source_file)
         }
       (if (source_file.is_java) java_src_dir else scala_src_dir) + dir
     }
   }
 
   def build_tools: List[Build_Tool] = List(Gradle, Maven)
 
 
   /* Gradle */
 
   object Gradle extends Build_Tool {
     override def toString: String = "Gradle"
 
     val project_settings: Path = Path.explode("settings.gradle")
     override val project_root: Path = Path.explode("build.gradle")
 
     private def groovy_string(s: String): String = {
       s.map(c =>
         c match {
           case '\t' | '\b' | '\n' | '\r' | '\f' | '\\' | '\'' | '"' => "\\" + c
           case _ => c.toString
         }).mkString("'", "", "'")
     }
 
     override def init_project(dir: Path, jars: List[Path]): Unit = {
       File.write(dir + project_settings, "rootProject.name = 'Isabelle'\n")
       File.write(dir + project_root,
 """plugins {
   id 'scala'
 }
 
 repositories {
   mavenCentral()
 }
 
 dependencies {
   implementation 'org.scala-lang:scala3-library_3:scala-library:""" + scala_version + """'
   compileOnly files(
     """ + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n    ", ")") +
 """
 }
 """)
     }
   }
 
 
   /* Maven */
 
   object Maven extends Build_Tool {
     override def toString: String = "Maven"
 
     override val project_root: Path = Path.explode("pom.xml")
 
     override def init_project(dir: Path, jars: List[Path]): Unit = {
       def dependency(jar: Path): String = {
         val name = jar.expand.drop_ext.base.implode
         val system_path = File.platform_path(jar.absolute)
-      """  <dependency>
+        """  <dependency>
     <groupId>classpath</groupId>
     <artifactId>""" + XML.text(name) + """</artifactId>
     <version>0</version>
     <scope>system</scope>
     <systemPath>""" + XML.text(system_path) + """</systemPath>
   </dependency>"""
       }
 
       val project = """<?xml version="1.0" encoding="UTF-8"?>
 <project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
   xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
   <modelVersion>4.0.0</modelVersion>
 
   <groupId>isabelle</groupId>
   <artifactId>isabelle</artifactId>
   <version>0</version>
 
   <properties>
     <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
     <maven.compiler.source>""" + java_version + """</maven.compiler.source>
     <maven.compiler.target>""" + java_version + """</maven.compiler.target>
   </properties>
 
   <build>
     <plugins>
       <plugin>
         <groupId>net.alchim31.maven</groupId>
         <artifactId>scala-maven-plugin</artifactId>
         <version>4.5.3</version>
         <configuration>
             <scalaVersion>""" + scala_version + """</scalaVersion>
         </configuration>
         </plugin>
     </plugins>
   </build>
 
   <dependencies>""" + jars.map(dependency).mkString("\n", "\n", "\n") + """</dependencies>
 </project>"""
 
       File.write(dir + project_root, project)
     }
   }
 
 
   /* plugins: modules with dynamic build */
 
   class Plugin(dir: Path) extends Isabelle_System.Service {
     def context(): Scala_Build.Context = Scala_Build.context(dir)
   }
 
   lazy val plugins: List[Plugin] = Isabelle_System.make_services(classOf[Plugin])
 
 
   /* file and directories */
 
   lazy val isabelle_files: (List[Path], List[Path]) = {
     val contexts = Scala_Build.component_contexts() ::: plugins.map(_.context())
 
     val jars1 = Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH"))
     val jars2 = contexts.flatMap(_.requirements)
 
     val jars =
       Library.distinct(jars1 ::: jars2).filterNot(path => contexts.exists(_.is_module(path)))
 
     val sources =
       (for {
         context <- contexts.iterator
         path <- context.sources.iterator
         if path.is_scala || path.is_java
       } yield path).toList
 
     (jars, sources)
   }
 
   lazy val isabelle_scala_files: Map[String, Path] =
     Scala_Build.context(Path.ISABELLE_HOME, component = true)
       .sources.iterator.foldLeft(Map.empty[String, Path]) {
         case (map, path) =>
           if (path.is_scala) {
           val base = path.base.implode
             map.get(base) match {
               case None => map + (base -> path)
               case Some(path2) => error("Conflicting base names: " + path + " vs. " + path2)
             }
           }
           else map
       }
 
 
   /* compile-time position */
 
   def here: Here = {
     val exn = new Exception
     exn.getStackTrace.toList match {
       case _ :: caller :: _ =>
         val name = proper_string(caller.getFileName).getOrElse("")
         val line = caller.getLineNumber
         new Here(name, line)
       case _ => new Here("", 0)
     }
   }
 
   class Here private[Scala_Project](name: String, line: Int) {
     override def toString: String = name + ":" + line
     def position: Position.T =
       isabelle_scala_files.get(name) match {
         case Some(path) => Position.Line_File(line, path.implode)
         case None => Position.none
       }
   }
 
 
   /* scala project */
 
   val default_project_dir = Path.explode("$ISABELLE_HOME_USER/scala_project")
 
   def package_name(source_file: Path): Option[String] = {
     val lines = Library.trim_split_lines(File.read(source_file))
     val Package = """\s*\bpackage\b\s*(?:object\b\s*)?((?:\w|\.)+)\b.*""".r
     lines.collectFirst({ case Package(name) => name })
   }
 
   def scala_project(
     build_tool: Build_Tool,
     project_dir: Path = default_project_dir,
     more_sources: List[Path] = Nil,
     symlinks: Boolean = false,
     force: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
     if (project_dir.file.exists) {
       val detect = project_dir.is_dir && build_tools.exists(_.detect_project(project_dir))
 
       if (force && detect) {
         progress.echo("Purging existing project directory: " + project_dir.absolute)
         Isabelle_System.rm_tree(project_dir)
       }
       else error("Project directory already exists: " + project_dir.absolute)
     }
 
     progress.echo("Creating " + build_tool + " project directory: " + project_dir.absolute)
     Isabelle_System.make_directory(project_dir)
 
     val java_src_dir = Isabelle_System.make_directory(project_dir + build_tool.java_src_dir)
     val scala_src_dir = Isabelle_System.make_directory(project_dir + build_tool.scala_src_dir)
 
     val (jars, sources) = isabelle_files
     isabelle_scala_files
 
     build_tool.init_project(project_dir, jars)
 
     for (source <- sources ::: more_sources) {
       val dir = build_tool.package_dir(source)
       val target_dir = project_dir + dir
       if (!target_dir.is_dir) {
         progress.echo("  Creating package directory: " + dir)
         Isabelle_System.make_directory(target_dir)
       }
       if (symlinks) Isabelle_System.symlink(source.absolute, target_dir, native = true)
       else Isabelle_System.copy_file(source, target_dir)
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("scala_project", "setup IDE project for Isabelle/Java/Scala sources",
       Scala_Project.here,
       { args =>
         var build_tool: Option[Build_Tool] = None
         var project_dir = default_project_dir
         var symlinks = false
         var force = false
 
         val getopts = Getopts("""
 Usage: isabelle scala_project [OPTIONS] [MORE_SOURCES ...]
 
   Options are:
     -D DIR       project directory (default: """ + default_project_dir + """)
     -G           use Gradle as build tool
     -L           make symlinks to original source files
     -M           use Maven as build tool
     -f           force update of existing directory
 
   Setup project for Isabelle/Scala/jEdit --- to support common IDEs such
   as IntelliJ IDEA. Either option -G or -M is mandatory to specify the
   build tool.
 """,
           "D:" -> (arg => project_dir = Path.explode(arg)),
           "G" -> (_ => build_tool = Some(Gradle)),
           "L" -> (_ => symlinks = true),
           "M" -> (_ => build_tool = Some(Maven)),
           "f" -> (_ => force = true))
 
         val more_args = getopts(args)
 
         val more_sources = more_args.map(Path.explode)
         val progress = new Console_Progress
 
         if (build_tool.isEmpty) {
           error("Unspecified build tool: need to provide option -G or -M")
         }
 
         scala_project(build_tool.get, project_dir = project_dir, more_sources = more_sources,
           symlinks = symlinks, force = force, progress = progress)
       })
 }
diff --git a/src/Tools/jEdit/src/syntax_style.scala b/src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala
+++ b/src/Tools/jEdit/src/syntax_style.scala
@@ -1,197 +1,199 @@
 /*  Title:      Tools/jEdit/src/syntax_style.scala
     Author:     Makarius
 
 Support for extended syntax styles: subscript, superscript, bold, user fonts.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.util.{Map => JMap}
 import java.awt.{Font, Color}
 import java.awt.font.TextAttribute
 import java.awt.geom.AffineTransform
 
 import org.gjt.sp.util.SyntaxUtilities
 import org.gjt.sp.jedit.jEdit
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
 import org.gjt.sp.jedit.textarea.TextArea
 
 
 object Syntax_Style {
   /* extended syntax styles */
 
   private val plain_range: Int = JEditToken.ID_COUNT
   private val full_range: Int = 6 * plain_range
   private def check_range(i: Int): Unit =
     require(0 <= i && i < plain_range, "bad syntax style range")
 
   def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
   def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
   def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
   def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
   val hidden: Byte = full_range.toByte
   val control: Byte = (hidden + JEditToken.DIGIT).toByte
 
   private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
     new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
 
   private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = {
     font_style(style, { font0 =>
       val font1 = font0.deriveFont(JMap.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
 
       def shift(y: Float): Font =
         GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
 
       val m0 = GUI.line_metrics(font0)
       val m1 = GUI.line_metrics(font1)
       val a = m1.getAscent - m0.getAscent
       val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
       if (a > 0.0f) shift(a)
       else if (b > 0.0f) shift(- b)
       else font1
     })
   }
 
   private def bold_style(style: SyntaxStyle): SyntaxStyle =
     font_style(style, font => font.deriveFont(if (font.isBold) Font.PLAIN else Font.BOLD))
 
   val hidden_color: Color = new Color(255, 255, 255, 0)
 
   def set_extender(extender: SyntaxUtilities.StyleExtender): Unit = {
     SyntaxUtilities.setStyleExtender(extender)
     GUI_Thread.later { jEdit.propertiesChanged }
   }
 
   object Base_Extender extends SyntaxUtilities.StyleExtender {
     override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = {
       val new_styles = Array.fill[SyntaxStyle](java.lang.Byte.MAX_VALUE)(styles(0))
       for (i <- 0 until full_range) {
         new_styles(i) = styles(i % plain_range)
       }
       new_styles
     }
   }
 
   object Main_Extender extends SyntaxUtilities.StyleExtender {
     val max_user_fonts = 2
     if (Symbol.symbols.font_names.length > max_user_fonts)
       error("Too many user symbol fonts (" + max_user_fonts + " permitted): " +
         Symbol.symbols.font_names.mkString(", "))
 
     override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = {
       val style0 = styles(0)
       val font0 = style0.getFont
 
       val new_styles = Array.fill[SyntaxStyle](java.lang.Byte.MAX_VALUE)(styles(0))
       for (i <- 0 until plain_range) {
         val style = styles(i)
         new_styles(i) = style
         new_styles(subscript(i.toByte)) = script_style(style, -1)
         new_styles(superscript(i.toByte)) = script_style(style, 1)
         new_styles(bold(i.toByte)) = bold_style(style)
         for (idx <- 0 until max_user_fonts)
           new_styles(user_font(idx, i.toByte)) = style
         for ((family, idx) <- Symbol.symbols.font_index)
           new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family))
       }
       new_styles(hidden) =
         new SyntaxStyle(hidden_color, null,
           GUI.transform_font(new Font(font0.getFamily, 0, 1),
             AffineTransform.getScaleInstance(2.0, font0.getSize.toDouble)))
       new_styles(control) =
         new SyntaxStyle(style0.getForegroundColor, style0.getBackgroundColor,
-          { val font_style =
+          {
+            val font_style =
               (if (font0.isItalic) 0 else Font.ITALIC) |
               (if (font0.isBold) 0 else Font.BOLD)
-            new Font(font0.getFamily, font_style, font0.getSize) })
+            new Font(font0.getFamily, font_style, font0.getSize)
+          })
       new_styles
     }
   }
 
   private def control_style(sym: String): Option[Byte => Byte] =
     if (sym == Symbol.sub_decoded) Some(subscript)
     else if (sym == Symbol.sup_decoded) Some(superscript)
     else if (sym == Symbol.bold_decoded) Some(bold)
     else None
 
   def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] = {
     var result = Map[Text.Offset, Byte => Byte]()
     def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte): Unit = {
       for (i <- start until stop) result += (i -> style)
     }
 
     var offset = 0
     var control_sym = ""
     for (sym <- Symbol.iterator(text)) {
       val end_offset = offset + sym.length
 
       if (control_style(sym).isDefined) control_sym = sym
       else if (control_sym != "") {
         if (Symbol.is_controllable(sym) && !Symbol.symbols.fonts.isDefinedAt(sym)) {
           mark(offset - control_sym.length, offset, _ => hidden)
           mark(offset, end_offset, control_style(control_sym).get)
         }
         control_sym = ""
       }
 
       if (Symbol.is_control_encoded(sym)) {
         val a = offset + Symbol.control_prefix.length
         val b = end_offset - Symbol.control_suffix.length
         mark(offset, a, _ => hidden)
         mark(a, b, _ => control)
         mark(b, end_offset, _ => hidden)
       }
 
       Symbol.symbols.lookup_font(sym) match {
         case Some(idx) => mark(offset, end_offset, user_font(idx, _))
         case _ =>
       }
 
       offset = end_offset
     }
 
     result
   }
 
 
   /* editing support for control symbols */
 
   def edit_control_style(text_area: TextArea, control_sym: String): Unit = {
     GUI_Thread.assert {}
 
     val buffer = text_area.getBuffer
 
     val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control_sym)
 
     def update_style(text: String): String = {
       val result = new StringBuilder
       for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) {
         if (Symbol.is_controllable(sym)) result ++= control_decoded
         result ++= sym
       }
       result.toString
     }
 
     text_area.getSelection.foreach { sel =>
       val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
       JEdit_Lib.get_text(buffer, before) match {
         case Some(s) if HTML.is_control(s) =>
           text_area.extendSelection(before.start, before.stop)
         case _ =>
       }
     }
 
     text_area.getSelection.toList match {
       case Nil =>
         text_area.setSelectedText(control_decoded)
       case sels =>
         JEdit_Lib.buffer_edit(buffer) {
           sels.foreach(sel =>
             text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel))))
         }
     }
   }
 }