diff --git a/src/Pure/GUI/gui.scala b/src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala
+++ b/src/Pure/GUI/gui.scala
@@ -1,355 +1,355 @@
 /*  Title:      Pure/GUI/gui.scala
     Author:     Makarius
 
 Basic GUI tools (for AWT/Swing).
 */
 
 package isabelle
 
 import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point,
   Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit}
 import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
 import java.awt.geom.AffineTransform
 import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
   JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities}
 import scala.swing.{ComboBox, ScrollPane, TextArea}
 import scala.swing.event.SelectionChanged
 
 
 object GUI
 {
   /* Swing look-and-feel */
 
   def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.install()
 
   def current_laf(): String = UIManager.getLookAndFeel.getClass.getName()
 
   def is_macos_laf(): Boolean =
     Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf()
 
   class Look_And_Feel(laf: LookAndFeel) extends Isabelle_System.Service
   {
     def info: UIManager.LookAndFeelInfo =
       new UIManager.LookAndFeelInfo(laf.getName, laf.getClass.getName)
   }
 
   lazy val look_and_feels: List[Look_And_Feel] =
     Isabelle_System.make_services(classOf[Look_And_Feel])
 
   def init_lafs()
   {
     val old_lafs =
       Set(
         "com.sun.java.swing.plaf.motif.MotifLookAndFeel",
         "com.sun.java.swing.plaf.windows.WindowsClassicLookAndFeel")
     val lafs =
       UIManager.getInstalledLookAndFeels().toList
         .filterNot(info => old_lafs(info.getClassName))
     val more_lafs = look_and_feels.map(_.info)
     UIManager.setInstalledLookAndFeels((more_lafs ::: lafs).toArray)
   }
 
 
   /* additional look-and-feels */
 
   /* plain focus traversal, notably for text fields */
 
   def plain_focus_traversal(component: Component)
   {
     val dummy_button = new JButton
     def apply(id: Int): Unit =
       component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id))
     apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS)
     apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS)
   }
 
 
   /* simple dialogs */
 
   def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
     : ScrollPane =
   {
     val txt = Output.clean_yxml(raw_txt)
     val text = new TextArea(txt)
     if (width > 0) text.columns = width
     if (height > 0 && split_lines(txt).length > height) text.rows = height
     text.editable = editable
     new ScrollPane(text)
   }
 
   private def simple_dialog(kind: Int, default_title: String,
     parent: Component, title: String, message: Iterable[Any])
   {
     GUI_Thread.now {
       val java_message =
         message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }).
           toArray.asInstanceOf[Array[AnyRef]]
       JOptionPane.showMessageDialog(parent, java_message,
         if (title == null) default_title else title, kind)
     }
   }
 
   def dialog(parent: Component, title: String, message: Any*): Unit =
     simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
 
   def warning_dialog(parent: Component, title: String, message: Any*): Unit =
     simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
 
   def error_dialog(parent: Component, title: String, message: Any*): Unit =
     simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
 
   def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
     GUI_Thread.now {
       val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
       JOptionPane.showConfirmDialog(parent,
         java_message.toArray.asInstanceOf[Array[AnyRef]], title,
           option_type, JOptionPane.QUESTION_MESSAGE)
     }
 
 
   /* zoom box */
 
   private val Zoom_Factor = "([0-9]+)%?".r
 
   abstract class Zoom_Box extends ComboBox[String](
     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
   {
     def changed: Unit
     def factor: Int = parse(selection.item)
 
     private def parse(text: String): Int =
       text match {
         case Zoom_Factor(s) =>
           val i = Integer.parseInt(s)
           if (10 <= i && i < 1000) i else 100
         case _ => 100
       }
 
     private def print(i: Int): String = i.toString + "%"
 
     def set_item(i: Int) {
       peer.getEditor match {
         case null =>
         case editor => editor.setItem(print(i))
       }
     }
 
     makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
     peer.getEditor.getEditorComponent match {
       case text: JTextField => text.setColumns(4)
       case _ =>
     }
 
     selection.index = 3
 
     listenTo(selection)
     reactions += { case SelectionChanged(_) => changed }
   }
 
 
   /* tooltip with multi-line support */
 
   def tooltip_lines(text: String): String =
     if (text == null || text == "") null
     else "<html>" + HTML.output(text) + "</html>"
 
 
   /* icon */
 
   def isabelle_icon(): ImageIcon =
     new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle_transparent-32.gif"))
 
   def isabelle_icons(): List[ImageIcon] =
     for (icon <- List("isabelle/isabelle_transparent-32.gif", "isabelle/isabelle_transparent.gif"))
       yield new ImageIcon(getClass.getClassLoader.getResource(icon))
 
   def isabelle_image(): Image = isabelle_icon().getImage
 
 
   /* location within multi-screen environment */
 
   final case class Screen_Location(point: Point, bounds: Rectangle)
   {
     def relative(parent: Component, size: Dimension): Point =
     {
       val w = size.width
       val h = size.height
 
       val x0 = parent.getLocationOnScreen.x
       val y0 = parent.getLocationOnScreen.y
       val x1 = x0 + parent.getWidth - w
       val y1 = y0 + parent.getHeight - h
       val x2 = point.x min (bounds.x + bounds.width - w)
       val y2 = point.y min (bounds.y + bounds.height - h)
 
       val location = new Point((x2 min x1) max x0, (y2 min y1) max y0)
       SwingUtilities.convertPointFromScreen(location, parent)
       location
     }
   }
 
   def screen_location(component: Component, point: Point): Screen_Location =
   {
     val screen_point = new Point(point.x, point.y)
     if (component != null) SwingUtilities.convertPointToScreen(screen_point, component)
 
     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
     val screen_bounds =
       (for {
         device <- ge.getScreenDevices.iterator
         config <- device.getConfigurations.iterator
         bounds = config.getBounds
       } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
 
     Screen_Location(screen_point, screen_bounds)
   }
 
   def mouse_location(): Screen_Location =
     screen_location(null, MouseInfo.getPointerInfo.getLocation)
 
 
   /* screen size */
 
   sealed case class Screen_Size(bounds: Rectangle, insets: Insets)
   {
     def full_screen_bounds: Rectangle =
       if (Platform.is_linux) {
         // avoid menu bar and docking areas
         new Rectangle(
           bounds.x + insets.left,
           bounds.y + insets.top,
           bounds.width - insets.left - insets.right,
           bounds.height - insets.top - insets.bottom)
       }
       else if (Platform.is_macos) {
         // avoid menu bar, but ignore docking areas
         new Rectangle(
           bounds.x,
           bounds.y + insets.top,
           bounds.width,
           bounds.height - insets.top)
       }
       else bounds
   }
 
   def screen_size(component: Component): Screen_Size =
   {
     val config = component.getGraphicsConfiguration
     val bounds = config.getBounds
     val insets = Toolkit.getDefaultToolkit.getScreenInsets(config)
     Screen_Size(bounds, insets)
   }
 
 
   /* component hierachy */
 
   def get_parent(component: Component): Option[Container] =
     component.getParent match {
       case null => None
       case parent => Some(parent)
     }
 
   def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
     private var next_elem = get_parent(component)
-    def hasNext(): Boolean = next_elem.isDefined
+    def hasNext: Boolean = next_elem.isDefined
     def next(): Container =
       next_elem match {
         case Some(parent) =>
           next_elem = get_parent(parent)
           parent
         case None => Iterator.empty.next()
       }
   }
 
   def parent_window(component: Component): Option[Window] =
     ancestors(component).collectFirst({ case x: Window => x })
 
   def layered_pane(component: Component): Option[JLayeredPane] =
     parent_window(component) match {
       case Some(w: JWindow) => Some(w.getLayeredPane)
       case Some(w: JFrame) => Some(w.getLayeredPane)
       case Some(w: JDialog) => Some(w.getLayeredPane)
       case _ => None
     }
 
   def traverse_components(component: Component, apply: Component => Unit)
   {
     def traverse(comp: Component)
     {
       apply(comp)
       comp match {
         case cont: Container =>
           for (i <- 0 until cont.getComponentCount)
             traverse(cont.getComponent(i))
         case _ =>
       }
     }
     traverse(component)
   }
 
 
   /* font operations */
 
   def copy_font(font: Font): Font =
     if (font == null) null
     else new Font(font.getFamily, font.getStyle, font.getSize)
 
   def line_metrics(font: Font): LineMetrics =
     font.getLineMetrics("", new FontRenderContext(null, false, false))
 
   def transform_font(font: Font, transform: AffineTransform): Font =
     font.deriveFont(java.util.Map.of(TextAttribute.TRANSFORM, new TransformAttribute(transform)))
 
   def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
     new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
 
   def label_font(): Font = (new JLabel).getFont
 
 
   /* Isabelle fonts */
 
   def imitate_font(font: Font,
     family: String = Isabelle_Fonts.sans,
     scale: Double = 1.0): Font =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
     val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
     new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt)
   }
 
   def imitate_font_css(font: Font,
     family: String = Isabelle_Fonts.sans,
     scale: Double = 1.0): String =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
     val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
     "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
   }
 
   def use_isabelle_fonts()
   {
     val default_font = label_font()
     val ui = UIManager.getDefaults
     for (prop <- List(
       "ToggleButton.font",
       "CheckBoxMenuItem.font",
       "Label.font",
       "Menu.font",
       "MenuItem.font",
       "PopupMenu.font",
       "Table.font",
       "TableHeader.font",
       "TextArea.font",
       "TextField.font",
       "TextPane.font",
       "ToolTip.font",
       "Tree.font"))
     {
       val font = ui.get(prop) match { case font: Font => font case _ => default_font }
       ui.put(prop, GUI.imitate_font(font))
     }
   }
 }
 
 class FlatLightLaf extends GUI.Look_And_Feel(new com.formdev.flatlaf.FlatLightLaf)
 class FlatDarkLaf extends GUI.Look_And_Feel(new com.formdev.flatlaf.FlatDarkLaf)
diff --git a/src/Pure/General/codepoint.scala b/src/Pure/General/codepoint.scala
--- a/src/Pure/General/codepoint.scala
+++ b/src/Pure/General/codepoint.scala
@@ -1,34 +1,34 @@
 /*  Title:      Pure/General/codepoint.scala
     Author:     Makarius
 
 Unicode codepoints vs. Unicode string encoding.
 */
 
 package isabelle
 
 import isabelle.Text.Offset
 
 
 object Codepoint
 {
   def string(c: Int): String = new String(Array(c), 0, 1)
 
   private class Iterator_Offset[A](s: String, result: (Int, Text.Offset) => A)
     extends Iterator[A]
   {
     var offset = 0
     def hasNext: Boolean = offset < s.length
-    def next: A =
+    def next(): A =
     {
       val c = s.codePointAt(offset)
       val i = offset
       offset += Character.charCount(c)
       result(c, i)
     }
   }
 
   def iterator_offset(s: String): Iterator[(Int, Text.Offset)] = new Iterator_Offset(s, (_, _))
   def iterator(s: String): Iterator[Int] = new Iterator_Offset(s, (c, _) => c)
 
   def length(s: String): Int = iterator(s).length
 }
diff --git a/src/Pure/General/linear_set.scala b/src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala
+++ b/src/Pure/General/linear_set.scala
@@ -1,164 +1,164 @@
 /*  Title:      Pure/General/linear_set.scala
     Author:     Makarius
     Author:     Fabian Immler, TU Munich
 
 Sets with canonical linear order, or immutable linked-lists.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 import scala.collection.immutable.SetOps
 import scala.collection.{IterableFactory, IterableFactoryDefaults}
 
 
 object Linear_Set extends IterableFactory[Linear_Set]
 {
   private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
   override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]]
 
   def from[A](entries: IterableOnce[A]): Linear_Set[A] = (empty[A] /: entries)(_.incl(_))
 
   override def newBuilder[A]: mutable.Builder[A, Linear_Set[A]] = new Builder[A]
   private class Builder[A] extends mutable.Builder[A, Linear_Set[A]]
   {
     private var res = empty[A]
     override def clear() { res = empty[A] }
     override def addOne(elem: A): this.type = { res = res.incl(elem); this }
     override def result(): Linear_Set[A] = res
   }
 
   class Duplicate[A](x: A) extends Exception
   class Undefined[A](x: A) extends Exception
   class Next_Undefined[A](x: Option[A]) extends Exception
 }
 
 
 final class Linear_Set[A] private(
     start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
   extends Iterable[A]
     with SetOps[A, Linear_Set, Linear_Set[A]]
     with IterableFactoryDefaults[A, Linear_Set]
 {
   /* relative addressing */
 
   def next(elem: A): Option[A] =
     if (contains(elem)) nexts.get(elem)
     else throw new Linear_Set.Undefined(elem)
 
   def prev(elem: A): Option[A] =
     if (contains(elem)) prevs.get(elem)
     else throw new Linear_Set.Undefined(elem)
 
   def get_after(hook: Option[A]): Option[A] =
     hook match {
       case None => start
       case Some(elem) => next(elem)
     }
 
   def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
     if (contains(elem)) throw new Linear_Set.Duplicate(elem)
     else
       hook match {
         case None =>
           start match {
             case None => new Linear_Set[A](Some(elem), Some(elem), Map(), Map())
             case Some(elem1) =>
               new Linear_Set[A](Some(elem), end,
                 nexts + (elem -> elem1), prevs + (elem1 -> elem))
           }
         case Some(elem1) =>
           if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
           else
             nexts.get(elem1) match {
               case None =>
                 new Linear_Set[A](start, Some(elem),
                   nexts + (elem1 -> elem), prevs + (elem -> elem1))
               case Some(elem2) =>
                 new Linear_Set[A](start, end,
                   nexts + (elem1 -> elem) + (elem -> elem2),
                   prevs + (elem2 -> elem) + (elem -> elem1))
             }
       }
 
   def append_after(hook: Option[A], elems: Iterable[A]): Linear_Set[A] =  // FIXME reverse fold
     ((hook, this) /: elems) {
       case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
     }._2
 
   def delete_after(hook: Option[A]): Linear_Set[A] =
     hook match {
       case None =>
         start match {
           case None => throw new Linear_Set.Next_Undefined[A](None)
           case Some(elem1) =>
             nexts.get(elem1) match {
               case None => empty
               case Some(elem2) =>
                 new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2)
             }
         }
       case Some(elem1) =>
         if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
         else
           nexts.get(elem1) match {
             case None => throw new Linear_Set.Next_Undefined(Some(elem1))
             case Some(elem2) =>
               nexts.get(elem2) match {
                 case None =>
                   new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2)
                 case Some(elem3) =>
                   new Linear_Set[A](start, end,
                     nexts - elem2 + (elem1 -> elem3),
                     prevs - elem2 + (elem3 -> elem1))
               }
           }
     }
 
 
   /* Set methods */
 
   override def isEmpty: Boolean = start.isEmpty
   override def size: Int = if (isEmpty) 0 else nexts.size + 1
 
   def contains(elem: A): Boolean =
     nonEmpty && (end.get == elem || nexts.isDefinedAt(elem))
 
   private def make_iterator(from: Option[A]): Iterator[A] = new Iterator[A] {
     private var next_elem = from
-    def hasNext(): Boolean = next_elem.isDefined
+    def hasNext: Boolean = next_elem.isDefined
     def next(): A =
       next_elem match {
         case Some(elem) =>
           next_elem = nexts.get(elem)
           elem
         case None => Iterator.empty.next()
       }
   }
 
   override def iterator: Iterator[A] = make_iterator(start)
 
   def iterator(elem: A): Iterator[A] =
     if (contains(elem)) make_iterator(Some(elem))
     else throw new Linear_Set.Undefined(elem)
 
   def iterator(from: A, to: A): Iterator[A] =
     if (contains(to))
       nexts.get(to) match {
         case None => iterator(from)
         case Some(stop) => iterator(from).takeWhile(_ != stop)
       }
     else throw new Linear_Set.Undefined(to)
 
   def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
 
   override def last: A = reverse.head
 
   def incl(elem: A): Linear_Set[A] = insert_after(end, elem)
   def excl(elem: A): Linear_Set[A] = delete_after(prev(elem))
 
   override def iterableFactory: IterableFactory[Linear_Set] = Linear_Set
 
   override def toString: String = mkString("Linear_Set(", ", ", ")")
 }
diff --git a/src/Pure/General/sql.scala b/src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala
+++ b/src/Pure/General/sql.scala
@@ -1,514 +1,514 @@
 /*  Title:      Pure/General/sql.scala
     Author:     Makarius
 
 Support for SQL databases: SQLite and PostgreSQL.
 */
 
 package isabelle
 
 
 import java.time.OffsetDateTime
 import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
 
 import scala.collection.mutable
 
 
 object SQL
 {
   /** SQL language **/
 
   type Source = String
 
 
   /* concrete syntax */
 
   def escape_char(c: Char): String =
     c match {
       case '\u0000' => "\\0"
       case '\'' => "\\'"
       case '\"' => "\\\""
       case '\b' => "\\b"
       case '\n' => "\\n"
       case '\r' => "\\r"
       case '\t' => "\\t"
       case '\u001a' => "\\Z"
       case '\\' => "\\\\"
       case _ => c.toString
     }
 
   def string(s: String): Source =
     s.iterator.map(escape_char).mkString("'", "", "'")
 
   def ident(s: String): Source =
     Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))
 
   def enclose(s: Source): Source = "(" + s + ")"
   def enclosure(ss: Iterable[Source]): Source = ss.mkString("(", ", ", ")")
 
   def select(columns: List[Column] = Nil, distinct: Boolean = false): Source =
     "SELECT " + (if (distinct) "DISTINCT " else "") +
     (if (columns.isEmpty) "*" else commas(columns.map(_.ident))) + " FROM "
 
   val join_outer: Source = " LEFT OUTER JOIN "
   val join_inner: Source = " INNER JOIN "
   def join(outer: Boolean): Source = if (outer) join_outer else join_inner
 
   def member(x: Source, set: Iterable[String]): Source =
     set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")")
 
 
   /* types */
 
   object Type extends Enumeration
   {
     val Boolean = Value("BOOLEAN")
     val Int = Value("INTEGER")
     val Long = Value("BIGINT")
     val Double = Value("DOUBLE PRECISION")
     val String = Value("TEXT")
     val Bytes = Value("BLOB")
     val Date = Value("TIMESTAMP WITH TIME ZONE")
   }
 
   def sql_type_default(T: Type.Value): Source = T.toString
 
   def sql_type_sqlite(T: Type.Value): Source =
     if (T == Type.Boolean) "INTEGER"
     else if (T == Type.Date) "TEXT"
     else sql_type_default(T)
 
   def sql_type_postgresql(T: Type.Value): Source =
     if (T == Type.Bytes) "BYTEA"
     else sql_type_default(T)
 
 
   /* columns */
 
   object Column
   {
     def bool(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
       Column(name, Type.Boolean, strict, primary_key)
     def int(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
       Column(name, Type.Int, strict, primary_key)
     def long(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
       Column(name, Type.Long, strict, primary_key)
     def double(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
       Column(name, Type.Double, strict, primary_key)
     def string(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
       Column(name, Type.String, strict, primary_key)
     def bytes(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
       Column(name, Type.Bytes, strict, primary_key)
     def date(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
       Column(name, Type.Date, strict, primary_key)
   }
 
   sealed case class Column(
     name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false,
     expr: SQL.Source = "")
   {
     def make_primary_key: Column = copy(primary_key = true)
 
     def apply(table: Table): Column =
       Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
 
     def ident: Source =
       if (expr == "") SQL.ident(name)
       else enclose(expr) + " AS " + SQL.ident(name)
 
     def decl(sql_type: Type.Value => Source): Source =
       ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
 
     def defined: String = ident + " IS NOT NULL"
     def undefined: String = ident + " IS NULL"
 
     def equal(s: String): Source = ident + " = " + string(s)
     def where_equal(s: String): Source = "WHERE " + equal(s)
 
     override def toString: Source = ident
   }
 
 
   /* tables */
 
   sealed case class Table(name: String, columns: List[Column], body: Source = "")
   {
     private val columns_index: Map[String, Int] =
       columns.iterator.map(_.name).zipWithIndex.toMap
 
     Library.duplicates(columns.map(_.name)) match {
       case Nil =>
       case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
     }
 
     def ident: Source = SQL.ident(name)
 
     def query: Source =
       if (body == "") error("Missing SQL body for table " + quote(name))
       else SQL.enclose(body)
 
     def query_named: Source = query + " AS " + SQL.ident(name)
 
     def create(strict: Boolean = false, sql_type: Type.Value => Source): Source =
     {
       val primary_key =
         columns.filter(_.primary_key).map(_.name) match {
           case Nil => Nil
           case keys => List("PRIMARY KEY " + enclosure(keys))
         }
       "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
         ident + " " + enclosure(columns.map(_.decl(sql_type)) ::: primary_key)
     }
 
     def create_index(index_name: String, index_columns: List[Column],
         strict: Boolean = false, unique: Boolean = false): Source =
       "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
         (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
         ident + " " + enclosure(index_columns.map(_.name))
 
     def insert_cmd(cmd: Source, sql: Source = ""): Source =
       cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
         (if (sql == "") "" else " " + sql)
 
     def insert(sql: Source = ""): Source = insert_cmd("INSERT", sql)
 
     def delete(sql: Source = ""): Source =
       "DELETE FROM " + ident +
         (if (sql == "") "" else " " + sql)
 
     def select(
         select_columns: List[Column] = Nil, sql: Source = "", distinct: Boolean = false): Source =
       SQL.select(select_columns, distinct = distinct) + ident +
         (if (sql == "") "" else " " + sql)
 
     override def toString: Source = ident
   }
 
 
 
   /** SQL database operations **/
 
   /* statements */
 
   class Statement private[SQL](val db: Database, val rep: PreparedStatement)
     extends AutoCloseable
   {
     stmt =>
 
     object bool
     {
       def update(i: Int, x: Boolean) { rep.setBoolean(i, x) }
       def update(i: Int, x: Option[Boolean])
       {
         if (x.isDefined) update(i, x.get)
         else rep.setNull(i, java.sql.Types.BOOLEAN)
       }
     }
     object int
     {
       def update(i: Int, x: Int) { rep.setInt(i, x) }
       def update(i: Int, x: Option[Int])
       {
         if (x.isDefined) update(i, x.get)
         else rep.setNull(i, java.sql.Types.INTEGER)
       }
     }
     object long
     {
       def update(i: Int, x: Long) { rep.setLong(i, x) }
       def update(i: Int, x: Option[Long])
       {
         if (x.isDefined) update(i, x.get)
         else rep.setNull(i, java.sql.Types.BIGINT)
       }
     }
     object double
     {
       def update(i: Int, x: Double) { rep.setDouble(i, x) }
       def update(i: Int, x: Option[Double])
       {
         if (x.isDefined) update(i, x.get)
         else rep.setNull(i, java.sql.Types.DOUBLE)
       }
     }
     object string
     {
       def update(i: Int, x: String) { rep.setString(i, x) }
       def update(i: Int, x: Option[String]): Unit = update(i, x.orNull)
     }
     object bytes
     {
       def update(i: Int, bytes: Bytes)
       {
         if (bytes == null) rep.setBytes(i, null)
         else rep.setBinaryStream(i, bytes.stream(), bytes.length)
       }
       def update(i: Int, bytes: Option[Bytes]): Unit = update(i, bytes.orNull)
     }
     object date
     {
       def update(i: Int, date: Date): Unit = db.update_date(stmt, i, date)
       def update(i: Int, date: Option[Date]): Unit = update(i, date.orNull)
     }
 
     def execute(): Boolean = rep.execute()
     def execute_query(): Result = new Result(this, rep.executeQuery())
 
     def close(): Unit = rep.close
   }
 
 
   /* results */
 
   class Result private[SQL](val stmt: Statement, val rep: ResultSet)
   {
     res =>
 
     def next(): Boolean = rep.next()
 
     def iterator[A](get: Result => A): Iterator[A] = new Iterator[A]
     {
       private var _next: Boolean = res.next()
       def hasNext: Boolean = _next
-      def next: A = { val x = get(res); _next = res.next(); x }
+      def next(): A = { val x = get(res); _next = res.next(); x }
     }
 
     def bool(column: Column): Boolean = rep.getBoolean(column.name)
     def int(column: Column): Int = rep.getInt(column.name)
     def long(column: Column): Long = rep.getLong(column.name)
     def double(column: Column): Double = rep.getDouble(column.name)
     def string(column: Column): String =
     {
       val s = rep.getString(column.name)
       if (s == null) "" else s
     }
     def bytes(column: Column): Bytes =
     {
       val bs = rep.getBytes(column.name)
       if (bs == null) Bytes.empty else Bytes(bs)
     }
     def date(column: Column): Date = stmt.db.date(res, column)
 
     def timing(c1: Column, c2: Column, c3: Column): Timing =
       Timing(Time.ms(long(c1)), Time.ms(long(c2)), Time.ms(long(c3)))
 
     def get[A](column: Column, f: Column => A): Option[A] =
     {
       val x = f(column)
       if (rep.wasNull) None else Some(x)
     }
     def get_bool(column: Column): Option[Boolean] = get(column, bool)
     def get_int(column: Column): Option[Int] = get(column, int)
     def get_long(column: Column): Option[Long] = get(column, long)
     def get_double(column: Column): Option[Double] = get(column, double)
     def get_string(column: Column): Option[String] = get(column, string)
     def get_bytes(column: Column): Option[Bytes] = get(column, bytes)
     def get_date(column: Column): Option[Date] = get(column, date)
   }
 
 
   /* database */
 
   trait Database extends AutoCloseable
   {
     db =>
 
 
     /* types */
 
     def sql_type(T: Type.Value): Source
 
 
     /* connection */
 
     def connection: Connection
 
     def close() { connection.close }
 
     def transaction[A](body: => A): A =
     {
       val auto_commit = connection.getAutoCommit
       try {
         connection.setAutoCommit(false)
         val savepoint = connection.setSavepoint
         try {
           val result = body
           connection.commit
           result
         }
         catch { case exn: Throwable => connection.rollback(savepoint); throw exn }
       }
       finally { connection.setAutoCommit(auto_commit) }
     }
 
 
     /* statements and results */
 
     def statement(sql: Source): Statement =
       new Statement(db, connection.prepareStatement(sql))
 
     def using_statement[A](sql: Source)(f: Statement => A): A =
       using(statement(sql))(f)
 
     def update_date(stmt: Statement, i: Int, date: Date): Unit
     def date(res: Result, column: Column): Date
 
     def insert_permissive(table: Table, sql: Source = ""): Source
 
 
     /* tables and views */
 
     def tables: List[String] =
     {
       val result = new mutable.ListBuffer[String]
       val rs = connection.getMetaData.getTables(null, null, "%", null)
       while (rs.next) { result += rs.getString(3) }
       result.toList
     }
 
     def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit =
       using_statement(
         table.create(strict, sql_type) + (if (sql == "") "" else " " + sql))(_.execute())
 
     def create_index(table: Table, name: String, columns: List[Column],
         strict: Boolean = false, unique: Boolean = false): Unit =
       using_statement(table.create_index(name, columns, strict, unique))(_.execute())
 
     def create_view(table: Table, strict: Boolean = false): Unit =
     {
       if (strict || !tables.contains(table.name)) {
         val sql = "CREATE VIEW " + table + " AS " + { table.query; table.body }
         using_statement(sql)(_.execute())
       }
     }
   }
 }
 
 
 
 /** SQLite **/
 
 object SQLite
 {
   // see https://www.sqlite.org/lang_datefunc.html
   val date_format: Date.Format = Date.Format("uuuu-MM-dd HH:mm:ss.SSS x")
 
   lazy val init_jdbc: Unit =
   {
     val lib_path = Path.explode("$ISABELLE_SQLITE_HOME/" + Platform.jvm_platform)
     val lib_name =
       File.find_files(lib_path.file) match {
         case List(file) => file.getName
         case _ => error("Exactly one file expected in directory " + lib_path.expand)
       }
     System.setProperty("org.sqlite.lib.path", File.platform_path(lib_path))
     System.setProperty("org.sqlite.lib.name", lib_name)
 
     Class.forName("org.sqlite.JDBC")
   }
 
   def open_database(path: Path): Database =
   {
     init_jdbc
     val path0 = path.expand
     val s0 = File.platform_path(path0)
     val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
     val connection = DriverManager.getConnection("jdbc:sqlite:" + s1)
     new Database(path0.toString, connection)
   }
 
   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database
   {
     override def toString: String = name
 
     def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
 
     def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
       if (date == null) stmt.string(i) = (null: String)
       else stmt.string(i) = date_format(date)
 
     def date(res: SQL.Result, column: SQL.Column): Date =
       date_format.parse(res.string(column))
 
     def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
       table.insert_cmd("INSERT OR IGNORE", sql = sql)
 
     def rebuild { using_statement("VACUUM")(_.execute()) }
   }
 }
 
 
 
 /** PostgreSQL **/
 
 object PostgreSQL
 {
   val default_port = 5432
 
   lazy val init_jdbc: Unit = Class.forName("org.postgresql.Driver")
 
   def open_database(
     user: String,
     password: String,
     database: String = "",
     host: String = "",
     port: Int = 0,
     ssh: Option[SSH.Session] = None,
     ssh_close: Boolean = false): Database =
   {
     init_jdbc
 
     if (user == "") error("Undefined database user")
 
     val db_host = proper_string(host) getOrElse "localhost"
     val db_port = if (port > 0 && port != default_port) ":" + port else ""
     val db_name = "/" + (proper_string(database) getOrElse user)
 
     val (url, name, port_forwarding) =
       ssh match {
         case None =>
           val spec = db_host + db_port + db_name
           val url = "jdbc:postgresql://" + spec
           val name = user + "@" + spec
           (url, name, None)
         case Some(ssh) =>
           val fw =
             ssh.port_forwarding(remote_host = db_host,
               remote_port = if (port > 0) port else default_port,
               ssh_close = ssh_close)
           val url = "jdbc:postgresql://localhost:" + fw.local_port + db_name
           val name = user + "@" + fw + db_name + " via ssh " + ssh
           (url, name, Some(fw))
       }
     try {
       val connection = DriverManager.getConnection(url, user, password)
       new Database(name, connection, port_forwarding)
     }
     catch { case exn: Throwable => port_forwarding.foreach(_.close); throw exn }
   }
 
   class Database private[PostgreSQL](
       name: String, val connection: Connection, port_forwarding: Option[SSH.Port_Forwarding])
     extends SQL.Database
   {
     override def toString: String = name
 
     def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_postgresql(T)
 
     // see https://jdbc.postgresql.org/documentation/head/8-date-time.html
     def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
       if (date == null) stmt.rep.setObject(i, null)
       else stmt.rep.setObject(i, OffsetDateTime.from(date.to(Date.timezone_utc).rep))
 
     def date(res: SQL.Result, column: SQL.Column): Date =
     {
       val obj = res.rep.getObject(column.name, classOf[OffsetDateTime])
       if (obj == null) null else Date.instant(obj.toInstant)
     }
 
     def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
       table.insert_cmd("INSERT",
         sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
 
     override def close() { super.close; port_forwarding.foreach(_.close) }
   }
 }
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,668 @@
 /*  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
   }
 
 
   /* 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.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig)
 
   def ascii(c: Char): Symbol =
   {
     if (c > 127) error("Non-ASCII character: " + quote(c.toString))
     else char_symbols(c.toInt)
   }
 
   def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128
 
 
   /* symbol matching */
 
   private val symbol_total = new Regex("""(?xs)
     [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""")
 
   private def is_plain(c: Char): Boolean =
     !(c == '\r' || c == '\\' || Character.isHighSurrogate(c))
 
   def is_malformed(s: Symbol): Boolean =
     s.length match {
       case 1 =>
         val c = s(0)
         Character.isHighSurrogate(c) || Character.isLowSurrogate(c) || c == '\ufffd'
       case 2 =>
         val c1 = s(0)
         val c2 = s(1)
         !(c1 == '\r' && c2 == '\n' || Character.isSurrogatePair(c1, c2))
       case _ => !s.endsWith(">") || s == "\\<>" || s == "\\<^>"
     }
 
   def is_newline(s: Symbol): Boolean =
     s == "\n" || s == "\r" || s == "\r\n"
 
   class Matcher(text: CharSequence)
   {
     private val matcher = symbol_total.pattern.matcher(text)
     def apply(start: Int, end: Int): Int =
     {
       require(0 <= start && start < end && end <= text.length, "bad matcher range")
       if (is_plain(text.charAt(start))) 1
       else {
         matcher.region(start, end).lookingAt
         matcher.group.length
       }
     }
   }
 
 
   /* iterator */
 
   private val char_symbols: Array[Symbol] =
     (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
 
   def iterator(text: CharSequence): Iterator[Symbol] =
     new Iterator[Symbol]
     {
       private val matcher = new Matcher(text)
       private var i = 0
       def hasNext: Boolean = i < text.length
-      def next: Symbol =
+      def next(): Symbol =
       {
         val n = matcher(i, text.length)
         val s =
           if (n == 0) ""
           else if (n == 1) {
             val c = text.charAt(i)
             if (c < char_symbols.length) char_symbols(c)
             else text.subSequence(i, i + n).toString
           }
           else text.subSequence(i, i + n).toString
         i += n
         s
       }
     }
 
   def explode(text: CharSequence): List[Symbol] = iterator(text).toList
 
   def length(text: CharSequence): Int = iterator(text).length
 
   def trim_blanks(text: CharSequence): String =
     Library.trim(is_blank, explode(text)).mkString
 
   def all_blank(str: String): Boolean =
     iterator(str).forall(is_blank)
 
   def trim_blank_lines(text: String): String =
     cat_lines(split_lines(text).dropWhile(all_blank).reverse.dropWhile(all_blank).reverse)
 
 
   /* decoding offsets */
 
   object Index
   {
     private sealed case class Entry(chr: Int, sym: Int)
 
     val empty: Index = new Index(Nil)
 
     def apply(text: CharSequence): Index =
     {
       val matcher = new Matcher(text)
       val buf = new mutable.ListBuffer[Entry]
       var chr = 0
       var sym = 0
       while (chr < text.length) {
         val n = matcher(chr, text.length)
         chr += n
         sym += 1
         if (n > 1) buf += Entry(chr, sym)
       }
       if (buf.isEmpty) empty else new Index(buf.toList)
     }
   }
 
   final class Index private(entries: List[Index.Entry])
   {
     private val hash: Int = entries.hashCode
     private val index: Array[Index.Entry] = entries.toArray
 
     def decode(symbol_offset: Offset): Text.Offset =
     {
       val sym = symbol_offset - 1
       val end = index.length
       @tailrec def bisect(a: Int, b: Int): Int =
       {
         if (a < b) {
           val c = (a + b) / 2
           if (sym < index(c).sym) bisect(a, c)
           else if (c + 1 == end || sym < index(c + 1).sym) c
           else bisect(c + 1, b)
         }
         else -1
       }
       val i = bisect(0, end)
       if (i < 0) sym
       else index(i).chr + sym - index(i).sym
     }
     def decode(symbol_range: Range): Text.Range = symbol_range.map(decode)
 
     override def hashCode: Int = hash
     override def equals(that: Any): Boolean =
       that match {
         case other: Index => index.sameElements(other.index)
         case _ => false
       }
   }
 
 
   /* symbolic text chunks -- without actual text */
 
   object Text_Chunk
   {
     sealed abstract class Name
     case object Default extends Name
     case class Id(id: Document_ID.Generic) extends Name
     case class File(name: String) extends Name
 
     def apply(text: CharSequence): Text_Chunk =
       new Text_Chunk(Text.Range(0, text.length), Index(text))
   }
 
   final class Text_Chunk private(val range: Text.Range, private val index: Index)
   {
     override def hashCode: Int = (range, index).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Text_Chunk =>
           range == other.range &&
           index == other.index
         case _ => false
       }
 
     override def toString: String = "Text_Chunk" + range.toString
 
     def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset)
     def decode(symbol_range: Range): Text.Range = index.decode(symbol_range)
     def incorporate(symbol_range: Range): Option[Text.Range] =
     {
       def in(r: Range): Option[Text.Range] =
         range.try_restrict(decode(r)) match {
           case Some(r1) if !r1.is_singularity => Some(r1)
           case _ => None
         }
      in(symbol_range) orElse in(symbol_range - 1)
     }
   }
 
 
   /* recoding text */
 
   private class Recoder(list: List[(String, String)])
   {
     private val (min, max) =
     {
       var min = '\uffff'
       var max = '\u0000'
       for ((x, _) <- list) {
         val c = x(0)
         if (c < min) min = c
         if (c > max) max = c
       }
       (min, max)
     }
     private val table =
     {
       var tab = Map[String, String]()
       for ((x, y) <- list) {
         tab.get(x) match {
           case None => tab += (x -> y)
           case Some(z) =>
             error("Duplicate symbol mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z))
         }
       }
       tab
     }
     def recode(text: String): String =
     {
       val len = text.length
       val matcher = symbol_total.pattern.matcher(text)
       val result = new StringBuilder(len)
       var i = 0
       while (i < len) {
         val c = text(i)
         if (min <= c && c <= max) {
           matcher.region(i, len).lookingAt
           val x = matcher.group
           result.append(table.getOrElse(x, x))
           i = matcher.end
         }
         else { result.append(c); i += 1 }
       }
       result.toString
     }
   }
 
 
 
   /** symbol interpretation **/
 
   val ARGUMENT_CARTOUCHE = "cartouche"
   val ARGUMENT_SPACE_CARTOUCHE = "space_cartouche"
 
   private lazy val symbols =
   {
     val contents =
       for (path <- Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS")) if path.is_file)
         yield (File.read(path))
     new Interpretation(cat_lines(contents))
   }
 
   private class Interpretation(symbols_spec: String)
   {
     /* read symbols */
 
     private val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
     private val Key = new Regex("""(?xs) (.+): """)
 
     private def read_decl(decl: String): (Symbol, Properties.T) =
     {
       def err() = error("Bad symbol declaration: " + decl)
 
       def read_props(props: List[String]): Properties.T =
       {
         props match {
           case Nil => Nil
           case _ :: Nil => err()
           case Key(x) :: y :: rest => (x -> y.replace('\u2423', ' ')) :: read_props(rest)
           case _ => err()
         }
       }
       decl.split("\\s+").toList match {
         case sym :: props if sym.length > 1 && !is_malformed(sym) =>
           (sym, read_props(props))
         case _ => err()
       }
     }
 
     private val symbols: List[(Symbol, Properties.T)] =
       (((List.empty[(Symbol, Properties.T)], Set.empty[Symbol]) /:
           split_lines(symbols_spec).reverse)
         { case (res, No_Decl()) => res
           case ((list, known), decl) =>
             val (sym, props) = read_decl(decl)
             if (known(sym)) (list, known)
             else ((sym, props) :: list, known + sym)
         })._1
 
 
     /* basic properties */
 
     val properties: Map[Symbol, Properties.T] = Map(symbols: _*)
 
     val names: Map[Symbol, (String, String)] =
     {
       val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
       val Argument = new Properties.String("argument")
       def argument(sym: Symbol, props: Properties.T): String =
         props match {
           case Argument(arg) =>
             if (arg == ARGUMENT_CARTOUCHE || arg == ARGUMENT_SPACE_CARTOUCHE) arg
             else error("Bad argument: " + quote(arg) + " for symbol " + quote(sym))
           case _ => ""
         }
       Map((for ((sym @ Name(a), props) <- symbols) yield sym -> (a, argument(sym, props))): _*)
     }
 
     val groups: List[(String, List[Symbol])] =
       symbols.flatMap({ case (sym, props) =>
         val gs = for (("group", g) <- props) yield g
         if (gs.isEmpty) List(sym -> "unsorted") else gs.map(sym -> _)
       }).groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
         .sortBy(_._1)
 
     val abbrevs: Multi_Map[Symbol, String] =
       Multi_Map((
         for {
           (sym, props) <- symbols
           ("abbrev", a) <- props.reverse
         } yield sym -> a): _*)
 
     val codes: List[(Symbol, Int)] =
     {
       val Code = new Properties.String("code")
       for {
         (sym, props) <- symbols
         code <-
           props match {
             case Code(s) =>
               try { Some(Integer.decode(s).intValue) }
               catch { case _: NumberFormatException => error("Bad code for symbol " + sym) }
             case _ => None
           }
       } yield {
         if (code < 128) error("Illegal ASCII code for symbol " + sym)
         else (sym, code)
       }
     }
 
 
     /* recoding */
 
     private val (decoder, encoder) =
     {
       val mapping =
         for ((sym, code) <- codes) yield (sym, new String(Character.toChars(code)))
       (new Recoder(mapping), new Recoder(for ((x, y) <- mapping) yield (y, x)))
     }
 
     def decode(text: String): String = decoder.recode(text)
     def encode(text: String): String = encoder.recode(text)
 
     private def recode_set(elems: String*): Set[String] =
     {
       val content = elems.toList
       Set((content ::: content.map(decode)): _*)
     }
 
     private def recode_map[A](elems: (String, A)*): Map[String, A] =
     {
       val content = elems.toList
       Map((content ::: content.map({ case (sym, a) => (decode(sym), a) })): _*)
     }
 
 
     /* user fonts */
 
     private val Font = new Properties.String("font")
     val fonts: Map[Symbol, String] =
       recode_map((for ((sym, Font(font)) <- symbols) yield sym -> font): _*)
 
     val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
     val font_index: Map[String, Int] = Map((font_names zip font_names.indices.toList): _*)
 
 
     /* classification */
 
     val letters: Set[String] = recode_set(
       "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
       "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
       "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
       "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z",
 
       "\\<A>", "\\<B>", "\\<C>", "\\<D>", "\\<E>", "\\<F>", "\\<G>",
       "\\<H>", "\\<I>", "\\<J>", "\\<K>", "\\<L>", "\\<M>", "\\<N>",
       "\\<O>", "\\<P>", "\\<Q>", "\\<R>", "\\<S>", "\\<T>", "\\<U>",
       "\\<V>", "\\<W>", "\\<X>", "\\<Y>", "\\<Z>", "\\<a>", "\\<b>",
       "\\<c>", "\\<d>", "\\<e>", "\\<f>", "\\<g>", "\\<h>", "\\<i>",
       "\\<j>", "\\<k>", "\\<l>", "\\<m>", "\\<n>", "\\<o>", "\\<p>",
       "\\<q>", "\\<r>", "\\<s>", "\\<t>", "\\<u>", "\\<v>", "\\<w>",
       "\\<x>", "\\<y>", "\\<z>",
 
       "\\<AA>", "\\<BB>", "\\<CC>", "\\<DD>", "\\<EE>", "\\<FF>",
       "\\<GG>", "\\<HH>", "\\<II>", "\\<JJ>", "\\<KK>", "\\<LL>",
       "\\<MM>", "\\<NN>", "\\<OO>", "\\<PP>", "\\<QQ>", "\\<RR>",
       "\\<SS>", "\\<TT>", "\\<UU>", "\\<VV>", "\\<WW>", "\\<XX>",
       "\\<YY>", "\\<ZZ>", "\\<aa>", "\\<bb>", "\\<cc>", "\\<dd>",
       "\\<ee>", "\\<ff>", "\\<gg>", "\\<hh>", "\\<ii>", "\\<jj>",
       "\\<kk>", "\\<ll>", "\\<mm>", "\\<nn>", "\\<oo>", "\\<pp>",
       "\\<qq>", "\\<rr>", "\\<ss>", "\\<tt>", "\\<uu>", "\\<vv>",
       "\\<ww>", "\\<xx>", "\\<yy>", "\\<zz>",
 
       "\\<alpha>", "\\<beta>", "\\<gamma>", "\\<delta>", "\\<epsilon>",
       "\\<zeta>", "\\<eta>", "\\<theta>", "\\<iota>", "\\<kappa>",
       "\\<mu>", "\\<nu>", "\\<xi>", "\\<pi>", "\\<rho>", "\\<sigma>",
       "\\<tau>", "\\<upsilon>", "\\<phi>", "\\<chi>", "\\<psi>",
       "\\<omega>", "\\<Gamma>", "\\<Delta>", "\\<Theta>", "\\<Lambda>",
       "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
       "\\<Psi>", "\\<Omega>")
 
     val blanks: Set[String] = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n")
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
 
     val symbolic: Set[String] = recode_set((for {(sym, _) <- symbols; if raw_symbolic(sym)} yield sym): _*)
 
 
     /* misc symbols */
 
     val newline_decoded = decode(newline)
     val comment_decoded = decode(comment)
     val cancel_decoded = decode(cancel)
     val latex_decoded = decode(latex)
     val marker_decoded = decode(marker)
     val open_decoded = decode(open)
     val close_decoded = decode(close)
 
 
     /* control symbols */
 
     val control_decoded: Set[Symbol] =
       Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
 
     val sub_decoded = decode(sub)
     val sup_decoded = decode(sup)
     val bold_decoded = decode(bold)
     val emph_decoded = decode(emph)
     val bsub_decoded = decode(bsub)
     val esub_decoded = decode(esub)
     val bsup_decoded = decode(bsup)
     val esup_decoded = decode(esup)
   }
 
 
   /* tables */
 
   def properties: Map[Symbol, Properties.T] = symbols.properties
   def names: Map[Symbol, (String, String)] = symbols.names
   def groups: List[(String, List[Symbol])] = symbols.groups
   def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs
   def codes: List[(Symbol, Int)] = symbols.codes
   def groups_code: List[(String, List[Symbol])] =
   {
     val has_code = codes.iterator.map(_._1).toSet
     groups.flatMap({ case (group, symbols) =>
       val symbols1 = symbols.filter(has_code)
       if (symbols1.isEmpty) None else Some((group, symbols1))
     })
   }
 
   lazy val is_code: Int => Boolean = codes.map(_._2).toSet
   def decode(text: String): String = symbols.decode(text)
   def encode(text: String): String = symbols.encode(text)
 
   def decode_yxml(text: String, 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)
 
   def fonts: Map[Symbol, String] = symbols.fonts
   def font_names: List[String] = symbols.font_names
   def font_index: Map[String, Int] = symbols.font_index
   def lookup_font(sym: Symbol): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
 
 
   /* classification */
 
   def is_letter(sym: Symbol): Boolean = symbols.letters.contains(sym)
   def is_digit(sym: Symbol): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
   def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'"
   def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
   def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
 
 
   /* symbolic newline */
 
   val newline: Symbol = "\\<newline>"
   def newline_decoded: Symbol = symbols.newline_decoded
 
   def print_newlines(str: String): String =
     if (str.contains('\n'))
       (for (s <- iterator(str)) yield { if (s == "\n") newline_decoded else s }).mkString
     else str
 
 
   /* formal comments */
 
   val comment: Symbol = "\\<comment>"
   val cancel: Symbol = "\\<^cancel>"
   val latex: Symbol = "\\<^latex>"
   val marker: Symbol = "\\<^marker>"
 
   def comment_decoded: Symbol = symbols.comment_decoded
   def cancel_decoded: Symbol = symbols.cancel_decoded
   def latex_decoded: Symbol = symbols.latex_decoded
   def marker_decoded: Symbol = symbols.marker_decoded
 
 
   /* cartouches */
 
   val open: Symbol = "\\<open>"
   val close: Symbol = "\\<close>"
 
   def open_decoded: Symbol = symbols.open_decoded
   def close_decoded: Symbol = symbols.close_decoded
 
   def is_open(sym: Symbol): Boolean = sym == open_decoded || sym == open
   def is_close(sym: Symbol): Boolean = sym == close_decoded || sym == close
 
   def cartouche(s: String): String = open + s + close
   def cartouche_decoded(s: String): String = open_decoded + s + close_decoded
 
 
   /* symbols for symbolic identifiers */
 
   private def raw_symbolic(sym: Symbol): Boolean =
     sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
 
   def is_symbolic(sym: Symbol): Boolean =
     !is_open(sym) && !is_close(sym) && (raw_symbolic(sym) || symbols.symbolic.contains(sym))
 
   def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
 
 
   /* control symbols */
 
   val control_prefix = "\\<^"
   val control_suffix = ">"
 
   def control_name(sym: Symbol): Option[String] =
     if (is_control_encoded(sym))
       Some(sym.substring(control_prefix.length, sym.length - control_suffix.length))
     else None
 
   def is_control_encoded(sym: Symbol): Boolean =
     sym.startsWith(control_prefix) && sym.endsWith(control_suffix)
 
   def is_control(sym: Symbol): Boolean =
     is_control_encoded(sym) || symbols.control_decoded.contains(sym)
 
   def is_controllable(sym: Symbol): Boolean =
     !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) &&
     !is_malformed(sym) && sym != "\""
 
   val sub: 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/General/untyped.scala b/src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala
+++ b/src/Pure/General/untyped.scala
@@ -1,60 +1,60 @@
 /*  Title:      Pure/General/untyped.scala
     Author:     Makarius
 
 Untyped, unscoped, unchecked access to JVM objects.
 */
 
 package isabelle
 
 
 import java.lang.reflect.{Constructor, Method, Field}
 
 
 object Untyped
 {
   def constructor[C](c: Class[C], arg_types: Class[_]*): Constructor[C] =
   {
     val con = c.getDeclaredConstructor(arg_types: _*)
     con.setAccessible(true)
     con
   }
 
   def method(c: Class[_], name: String, arg_types: Class[_]*): Method =
   {
     val m = c.getDeclaredMethod(name, arg_types: _*)
     m.setAccessible(true)
     m
   }
 
   def classes(obj: AnyRef): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] {
     private var next_elem: Class[_ <: AnyRef] = obj.getClass
-    def hasNext(): Boolean = next_elem != null
+    def hasNext: Boolean = next_elem != null
     def next(): Class[_ <: AnyRef] = {
       val c = next_elem
       next_elem = c.getSuperclass.asInstanceOf[Class[_ <: AnyRef]]
       c
     }
   }
 
   def field(obj: AnyRef, x: String): Field =
   {
     val iterator =
       for {
         c <- classes(obj)
         field <- c.getDeclaredFields.iterator
         if field.getName == x
       } yield {
         field.setAccessible(true)
         field
       }
     if (iterator.hasNext) iterator.next
     else error("No field " + quote(x) + " for " + obj)
   }
 
   def get[A](obj: AnyRef, x: String): A =
     if (obj == null) null.asInstanceOf[A]
     else field(obj, x).get(obj).asInstanceOf[A]
 
   def set[A](obj: AnyRef, x: String, y: A): Unit =
     field(obj, x).set(obj, y)
 }
diff --git a/src/Pure/library.scala b/src/Pure/library.scala
--- a/src/Pure/library.scala
+++ b/src/Pure/library.scala
@@ -1,298 +1,298 @@
 /*  Title:      Pure/library.scala
     Author:     Makarius
 
 Basic library.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.util.matching.Regex
 
 
 object Library
 {
   /* resource management */
 
   def using[A <: AutoCloseable, B](a: A)(f: A => B): B =
   {
     try { f(a) }
     finally { if (a != null) a.close() }
   }
 
 
   /* integers */
 
   private val small_int = 10000
   private lazy val small_int_table =
   {
     val array = new Array[String](small_int)
     for (i <- 0 until small_int) array(i) = i.toString
     array
   }
 
   def is_small_int(s: String): Boolean =
   {
     val len = s.length
     1 <= len && len <= 4 &&
     s.forall(c => '0' <= c && c <= '9') &&
     (len == 1 || s(0) != '0')
   }
 
   def signed_string_of_long(i: Long): String =
     if (0 <= i && i < small_int) small_int_table(i.toInt)
     else i.toString
 
   def signed_string_of_int(i: Int): String =
     if (0 <= i && i < small_int) small_int_table(i)
     else i.toString
 
 
   /* separated chunks */
 
   def separate[A](s: A, list: List[A]): List[A] =
   {
     val result = new mutable.ListBuffer[A]
     var first = true
     for (x <- list) {
       if (first) {
         first = false
         result += x
       }
       else {
         result += s
         result += x
       }
     }
     result.toList
   }
 
   def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
     new Iterator[CharSequence] {
       private val end = source.length
       private def next_chunk(i: Int): Option[(CharSequence, Int)] =
       {
         if (i < end) {
           var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
           Some((source.subSequence(i + 1, j), j))
         }
         else None
       }
       private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
 
-      def hasNext(): Boolean = state.isDefined
+      def hasNext: Boolean = state.isDefined
       def next(): CharSequence =
         state match {
           case Some((s, i)) => state = next_chunk(i); s
           case None => Iterator.empty.next()
         }
     }
 
   def space_explode(sep: Char, str: String): List[String] =
     separated_chunks(_ == sep, str).map(_.toString).toList
 
 
   /* lines */
 
   def terminate_lines(lines: TraversableOnce[String]): String = lines.mkString("", "\n", "\n")
 
   def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
   def prefix_lines(prfx: String, str: String): String =
     if (str == "") str else cat_lines(split_lines(str).map(prfx + _))
 
   def first_line(source: CharSequence): String =
   {
     val lines = separated_chunks(_ == '\n', source)
     if (lines.hasNext) lines.next.toString
     else ""
   }
 
   def trim_line(s: String): String =
     if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
     else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
     else s
 
   def trim_split_lines(s: String): List[String] =
     split_lines(trim_line(s)).map(trim_line)
 
   def encode_lines(s: String): String = s.replace('\n', '\u000b')
   def decode_lines(s: String): String = s.replace('\u000b', '\n')
 
 
   /* strings */
 
   def cat_strings0(strs: TraversableOnce[String]): String = strs.mkString("\u0000")
   def split_strings0(str: String): List[String] = space_explode('\u0000', str)
 
   def make_string(f: StringBuilder => Unit): String =
   {
     val s = new StringBuilder
     f(s)
     s.toString
   }
 
   def try_unprefix(prfx: String, s: String): Option[String] =
     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
 
   def try_unsuffix(sffx: String, s: String): Option[String] =
     if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
 
   def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s
   def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s
 
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
   def strip_ansi_color(s: String): String =
     s.replaceAll("""\u001b\[\d+m""", "")
 
 
   /* quote */
 
   def single_quote(s: String): String = "'" + s + "'"
 
   def quote(s: String): String = "\"" + s + "\""
 
   def try_unquote(s: String): Option[String] =
     if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
     else None
 
   def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
 
   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
 
 
   /* CharSequence */
 
   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
   {
     require(0 <= start && start <= end && end <= text.length, "bad reverse range")
 
     def this(text: CharSequence) = this(text, 0, text.length)
 
     def length: Int = end - start
     def charAt(i: Int): Char = text.charAt(end - i - 1)
 
     def subSequence(i: Int, j: Int): CharSequence =
       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
       else throw new IndexOutOfBoundsException
 
     override def toString: String =
     {
       val buf = new StringBuilder(length)
       for (i <- 0 until length)
         buf.append(charAt(i))
       buf.toString
     }
   }
 
   class Line_Termination(text: CharSequence) extends CharSequence
   {
     def length: Int = text.length + 1
     def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
     def subSequence(i: Int, j: Int): CharSequence =
       if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
       else text.subSequence(i, j)
     override def toString: String = text.toString + "\n"
   }
 
 
   /* regular expressions */
 
   def make_regex(s: String): Option[Regex] =
     try { Some(new Regex(s)) } catch { case ERROR(_) => None }
 
   def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
 
   def escape_regex(s: String): String =
     if (s.exists(is_regex_meta)) {
       (for (c <- s.iterator)
        yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
     }
     else s
 
 
   /* lists */
 
   def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
     (xs.takeWhile(pred), xs.dropWhile(pred))
 
   def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
   {
     val rev_xs = xs.reverse
     (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse)
   }
 
   def trim[A](pred: A => Boolean, xs: List[A]): List[A] =
     take_suffix(pred, take_prefix(pred, xs)._2)._1
 
   def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
 
   def merge[A](xs: List[A], ys: List[A]): List[A] =
     if (xs.eq(ys)) xs
     else if (xs.isEmpty) ys
     else ys.foldRight(xs)(Library.insert(_)(_))
 
   def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
   {
     val result = new mutable.ListBuffer[A]
     xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x)
     result.toList
   }
 
   def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
   {
     val result = new mutable.ListBuffer[A]
     @tailrec def dups(rest: List[A]): Unit =
       rest match {
         case Nil =>
         case x :: xs =>
           if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x
           dups(xs)
       }
     dups(lst)
     result.toList
   }
 
   def replicate[A](n: Int, a: A): List[A] =
     if (n < 0) throw new IllegalArgumentException
     else if (n == 0) Nil
     else {
       val res = new mutable.ListBuffer[A]
       (1 to n).foreach(_ => res += a)
       res.toList
     }
 
 
   /* proper values */
 
   def proper_string(s: String): Option[String] =
     if (s == null || s == "") None else Some(s)
 
   def proper_list[A](list: List[A]): Option[List[A]] =
     if (list == null || list.isEmpty) None else Some(list)
 
 
   /* reflection */
 
   def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean =
   {
     @tailrec def subclass(c: Class[_]): Boolean =
     {
       c == b ||
         {
           val d = c.getSuperclass
           d != null && subclass(d)
         }
     }
     subclass(a)
   }
 }
diff --git a/src/Tools/Graphview/layout.scala b/src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala
+++ b/src/Tools/Graphview/layout.scala
@@ -1,407 +1,407 @@
 /*  Title:      Tools/Graphview/layout.scala
     Author:     Markus Kaiser, TU Muenchen
     Author:     Makarius
 
 DAG layout according to:
 
   Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing,
   DIMACS International Workshop (GD'94), Springer LNCS 894, 1995.
 
   https://doi.org/10.1007/3-540-58950-3_371
   ftp://ftp.cs.uni-sb.de/pub/graphics/vcg/doc/tr-A03-94.ps.gz
 */
 
 package isabelle.graphview
 
 
 import isabelle._
 
 
 object Layout
 {
   /* graph structure */
 
   object Vertex
   {
     object Ordering extends scala.math.Ordering[Vertex]
     {
       def compare(v1: Vertex, v2: Vertex): Int =
         (v1, v2) match {
           case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b)
           case (Dummy(a1, a2, i), Dummy(b1, b2, j)) =>
             Graph_Display.Node.Ordering.compare(a1, b1) match {
               case 0 =>
                 Graph_Display.Node.Ordering.compare(a2, b2) match {
                   case 0 => i compare j
                   case ord => ord
                 }
               case ord => ord
             }
           case (Node(a), Dummy(b, _, _)) =>
             Graph_Display.Node.Ordering.compare(a, b) match {
               case 0 => -1
               case ord => ord
             }
           case (Dummy(a, _, _), Node(b)) =>
             Graph_Display.Node.Ordering.compare(a, b) match {
               case 0 => 1
               case ord => ord
             }
         }
     }
   }
 
   sealed abstract class Vertex
   case class Node(node: Graph_Display.Node) extends Vertex
   case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex
 
   sealed case class Info(
     x: Double, y: Double, width2: Double, height2: Double, lines: List[String])
   {
     def left: Double = x - width2
     def right: Double = x + width2
     def width: Double = 2 * width2
     def height: Double = 2 * height2
   }
 
   type Graph = isabelle.Graph[Vertex, Info]
 
   def make_graph(entries: List[((Vertex, Info), List[Vertex])]): Graph =
     isabelle.Graph.make(entries)(Vertex.Ordering)
 
   val empty_graph: Graph = make_graph(Nil)
 
 
   /* vertex x coordinate */
 
   private def vertex_left(graph: Graph, v: Vertex) = graph.get_node(v).left
   private def vertex_right(graph: Graph, v: Vertex) = graph.get_node(v).right
 
   private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph =
     if (dx == 0.0) graph else graph.map_node(v, info => info.copy(x = info.x + dx))
 
 
   /* layout */
 
   val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph)
 
 
   private type Levels = Map[Vertex, Int]
   private val empty_levels: Levels = Map.empty
 
   def make(options: Options, metrics: Metrics,
     node_text: (Graph_Display.Node, XML.Body) => String,
     input_graph: Graph_Display.Graph): Layout =
   {
     if (input_graph.is_empty) empty
     else {
       /* initial graph */
 
       val initial_graph =
         make_graph(
           input_graph.iterator.map(
             { case (a, (content, (_, bs))) =>
                 val lines = split_lines(node_text(a, content))
                 val w2 = metrics.node_width2(lines)
                 val h2 = metrics.node_height2(lines.length)
                 ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node))
             }).toList)
 
       val initial_levels: Levels =
         (empty_levels /: initial_graph.topological_order) {
           case (levels, vertex) =>
             val level =
               1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) }
             levels + (vertex -> level)
         }
 
 
       /* graph with dummies */
 
       val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil)
 
       val (dummy_graph, dummy_levels) =
         ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
             case ((graph, levels), (node1, node2)) =>
               val v1 = Node(node1); val l1 = levels(v1)
               val v2 = Node(node2); val l2 = levels(v2)
               if (l2 - l1 <= 1) (graph, levels)
               else {
                 val dummies_levels =
                   (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
                     yield (Dummy(node1, node2, i), l)).toList
                 val dummies = dummies_levels.map(_._1)
 
                 val levels1 = (levels /: dummies_levels)(_ + _)
                 val graph1 =
                   ((graph /: dummies)(_.new_node(_, dummy_info)).del_edge(v1, v2) /:
                     (v1 :: dummies ::: List(v2)).sliding(2)) {
                       case (g, List(a, b)) => g.add_edge(a, b) }
                 (graph1, levels1)
               }
           }
 
 
       /* minimize edge crossings and initial coordinates */
 
       val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels))
 
       val levels_graph: Graph =
         (((dummy_graph, 0.0) /: levels) {
           case ((graph, y), level) =>
             val num_lines = (0 /: level) { case (n, v) => n max graph.get_node(v).lines.length }
             val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size }
 
             val y1 = y + metrics.node_height2(num_lines)
 
             val graph1 =
               (((graph, 0.0) /: level) { case ((g, x), v) =>
                 val info = g.get_node(v)
                 val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
                 val x1 = x + info.width + metrics.gap
                 (g1, x1)
               })._1
 
             val y2 = y1 + metrics.level_height2(num_lines, num_edges)
 
             (graph1, y2)
         })._1
 
 
       /* pendulum/rubberband layout */
 
       val output_graph =
         rubberband(options, metrics, levels,
           pendulum(options, metrics, levels, levels_graph))
 
       new Layout(metrics, input_graph, output_graph)
     }
   }
 
 
 
   /** edge crossings **/
 
   private type Level = List[Vertex]
 
   private def minimize_crossings(
     options: Options, graph: Graph, levels: List[Level]): List[Level] =
   {
     def resort(parent: Level, child: Level, top_down: Boolean): Level =
       child.map(v => {
           val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
           val weight =
             (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
           (v, weight)
       }).sortBy(_._2).map(_._1)
 
     ((levels, count_crossings(graph, levels)) /:
       (1 to (2 * options.int("graphview_iterations_minimize_crossings")))) {
       case ((old_levels, old_crossings), iteration) =>
         val top_down = (iteration % 2 == 1)
         val new_levels =
           if (top_down)
             (List(old_levels.head) /: old_levels.tail)((tops, bot) =>
               resort(tops.head, bot, top_down) :: tops).reverse
           else {
             val rev_old_levels = old_levels.reverse
             (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) =>
               resort(bots.head, top, top_down) :: bots)
           }
         val new_crossings = count_crossings(graph, new_levels)
         if (new_crossings < old_crossings)
           (new_levels, new_crossings)
         else
           (old_levels, old_crossings)
     }._1
   }
 
   private def level_list(levels: Levels): List[Level] =
   {
     val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
     val buckets = new Array[Level](max_lev + 1)
     for (l <- 0 to max_lev) { buckets(l) = Nil }
     for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
     buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
   }
 
   private def count_crossings(graph: Graph, levels: List[Level]): Int =
     levels.iterator.sliding(2).map {
       case List(top, bot) =>
         top.iterator.zipWithIndex.map {
           case (outer_parent, outer_parent_index) =>
             graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child =>
               (0 until outer_parent_index).iterator.map(inner_parent =>
                 graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
                   .count(inner_child => outer_child < inner_child)).sum).sum
         }.sum
       case _ => 0
     }.sum
 
 
 
   /** pendulum method **/
 
   /*This is an auxiliary class which is used by the layout algorithm when
     calculating coordinates with the "pendulum method". A "region" is a
     group of vertices which "stick together".*/
   private class Region(val content: List[Vertex])
   {
     def distance(metrics: Metrics, graph: Graph, that: Region): Double =
       vertex_left(graph, that.content.head) -
       vertex_right(graph, this.content.last) -
       metrics.gap
 
     def deflection(graph: Graph, top_down: Boolean): Double =
       ((for (a <- content.iterator) yield {
         val x = graph.get_node(a).x
         val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
         bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
       }).sum / content.length).round.toDouble
 
     def move(graph: Graph, dx: Double): Graph =
       if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx))
 
     def combine(that: Region): Region = new Region(content ::: that.content)
   }
 
   private def pendulum(
     options: Options, metrics: Metrics, levels: List[Level], levels_graph: Graph): Graph =
   {
     def combine_regions(graph: Graph, top_down: Boolean, level: List[Region]): List[Region] =
       level match {
         case r1 :: rest =>
           val rest1 = combine_regions(graph, top_down, rest)
           rest1 match {
             case r2 :: rest2 =>
               val d1 = r1.deflection(graph, top_down)
               val d2 = r2.deflection(graph, top_down)
               if (// Do regions touch?
                   r1.distance(metrics, graph, r2) <= 0.0 &&
                   // Do they influence each other?
                   (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0))
                 r1.combine(r2) :: rest2
               else r1 :: rest1
             case _ => r1 :: rest1
           }
         case _ => level
       }
 
     def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) =
     {
       ((graph, false) /: level.indices) {
         case ((graph, moved), i) =>
           val r = level(i)
           val d = r.deflection(graph, top_down)
           val dx =
             if (d < 0.0 && i > 0)
               - (level(i - 1).distance(metrics, graph, r) min (- d))
             else if (d >= 0.0 && i < level.length - 1)
               r.distance(metrics, graph, level(i + 1)) min d
             else d
           (r.move(graph, dx), moved || d != 0.0)
       }
     }
 
     val initial_regions = levels.map(level => level.map(l => new Region(List(l))))
 
     ((levels_graph, initial_regions, true) /:
       (1 to (2 * options.int("graphview_iterations_pendulum")))) {
       case ((graph, regions, moved), iteration) =>
         val top_down = (iteration % 2 == 1)
         if (moved) {
           val (graph1, regions1, moved1) =
             ((graph, List.empty[List[Region]], false) /:
               (if (top_down) regions else regions.reverse)) { case ((graph, tops, moved), bot) =>
                 val bot1 = combine_regions(graph, top_down, bot)
                 val (graph1, moved1) = deflect(bot1, top_down, graph)
                 (graph1, bot1 :: tops, moved || moved1)
             }
           (graph1, regions1.reverse, moved1)
         }
         else (graph, regions, moved)
     }._1
   }
 
 
 
   /** rubberband method **/
 
   private def force_weight(graph: Graph, v: Vertex): Double =
   {
     val preds = graph.imm_preds(v)
     val succs = graph.imm_succs(v)
     val n = preds.size + succs.size
     if (n == 0) 0.0
     else {
       val x = graph.get_node(v).x
       ((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n
     }
   }
 
   private def rubberband(
     options: Options, metrics: Metrics, levels: List[Level], graph: Graph): Graph =
   {
     val gap = metrics.gap
 
     (graph /: (1 to (2 * options.int("graphview_iterations_rubberband")))) { case (graph, _) =>
       (graph /: levels) { case (graph, level) =>
         val m = level.length - 1
         (graph /: level.iterator.zipWithIndex) {
           case (g, (v, i)) =>
             val d = force_weight(g, v)
             if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
                 d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
               move_vertex(g, v, d.round.toDouble)
             else g
         }
       }
     }
   }
 }
 
 final class Layout private(
   val metrics: Metrics,
   val input_graph: Graph_Display.Graph,
   val output_graph: Layout.Graph)
 {
   /* vertex coordinates */
 
   def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout =
   {
     if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this
     else {
       val output_graph1 =
         output_graph.map_node(v, info => info.copy(x = info.x + dx, y = info.y + dy))
       new Layout(metrics, input_graph, output_graph1)
     }
   }
 
 
   /* regular nodes */
 
   def get_node(node: Graph_Display.Node): Layout.Info =
     output_graph.get_node(Layout.Node(node))
 
   def nodes_iterator: Iterator[Layout.Info] =
     for ((_: Layout.Node, (info, _)) <- output_graph.iterator) yield info
 
 
   /* dummies */
 
   def dummies_iterator: Iterator[Layout.Info] =
     for ((_: Layout.Dummy, (info, _)) <- output_graph.iterator) yield info
 
   def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Info] =
     new Iterator[Layout.Info] {
       private var index = 0
       def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index))
-      def next: Layout.Info =
+      def next(): Layout.Info =
       {
         val info = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
         index += 1
         info
       }
     }
 }
 
diff --git a/src/Tools/jEdit/src/jedit_options.scala b/src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala
+++ b/src/Tools/jEdit/src/jedit_options.scala
@@ -1,136 +1,136 @@
 /*  Title:      Tools/jEdit/src/jedit_options.scala
     Author:     Makarius
 
 Options for Isabelle/jEdit.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.{Font, Color}
 import javax.swing.{InputVerifier, JComponent, UIManager}
 import javax.swing.text.JTextComponent
 
 import scala.swing.{Component, CheckBox, TextArea}
 import scala.swing.event.ButtonClicked
 
 import org.gjt.sp.jedit.gui.ColorWellButton
 
 
 trait Option_Component extends Component
 {
   val title: String
   def load(): Unit
   def save(): Unit
 }
 
 object JEdit_Options
 {
   val RENDERING_SECTION = "Rendering of Document Content"
 
   class Check_Box(name: String, label: String, description: String) extends CheckBox(label)
   {
     tooltip = description
     reactions += { case ButtonClicked(_) => update(selected) }
 
     def stored: Boolean = PIDE.options.bool(name)
     def update(b: Boolean): Unit =
       GUI_Thread.require {
         if (selected != b) selected = b
         if (stored != b) {
           PIDE.options.bool(name) = b
           PIDE.session.update_options(PIDE.options.value)
         }
       }
     def load() { selected = stored }
     load()
   }
 }
 
 class JEdit_Options(init_options: Options) extends Options_Variable(init_options)
 {
   def color_value(s: String): Color = Color_Value(string(s))
 
   def make_color_component(opt: Options.Opt): Option_Component =
   {
     GUI_Thread.require {}
 
     val opt_name = opt.name
     val opt_title = opt.title("jedit")
 
     val button = new ColorWellButton(Color_Value(opt.value))
     val component = new Component with Option_Component {
       override lazy val peer = button
       name = opt_name
       val title = opt_title
-      def load = button.setSelectedColor(Color_Value(string(opt_name)))
-      def save = string(opt_name) = Color_Value.print(button.getSelectedColor)
+      def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name)))
+      def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor)
     }
     component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
   }
 
   def make_component(opt: Options.Opt): Option_Component =
   {
     GUI_Thread.require {}
 
     val opt_name = opt.name
     val opt_title = opt.title("jedit")
 
     val component =
       if (opt.typ == Options.Bool)
         new CheckBox with Option_Component {
           name = opt_name
           val title = opt_title
-          def load = selected = bool(opt_name)
-          def save = bool(opt_name) = selected
+          def load(): Unit = selected = bool(opt_name)
+          def save(): Unit = bool(opt_name) = selected
         }
       else {
         val default_font = GUI.copy_font(UIManager.getFont("TextField.font"))
         val text_area =
           new TextArea with Option_Component {
             if (default_font != null) font = default_font
             name = opt_name
             val title = opt_title
-            def load = text = value.check_name(opt_name).value
-            def save =
+            def load(): Unit = text = value.check_name(opt_name).value
+            def save(): Unit =
               try { JEdit_Options.this += (opt_name, text) }
               catch {
                 case ERROR(msg) =>
                   GUI.error_dialog(this.peer, "Failed to update options",
                     GUI.scrollable_text(msg))
               }
           }
         text_area.peer.setInputVerifier(new InputVerifier {
           def verify(jcomponent: JComponent): Boolean =
             jcomponent match {
               case text: JTextComponent =>
                 try { value + (opt_name, text.getText); true }
                 catch { case ERROR(_) => false }
               case _ => true
             }
           })
         GUI.plain_focus_traversal(text_area.peer)
         text_area
       }
     component.load()
     component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
   }
 
   def make_components(predefined: List[Option_Component], filter: String => Boolean)
     : List[(String, List[Option_Component])] =
   {
     def mk_component(opt: Options.Opt): List[Option_Component] =
       predefined.find(opt.name == _.name) match {
         case Some(c) => List(c)
         case None => if (filter(opt.name)) List(make_component(opt)) else Nil
       }
     value.sections.sortBy(_._1).map(
         { case (a, opts) => (a, opts.sortBy(_.title("jedit")).flatMap(mk_component)) })
       .filterNot(_._2.isEmpty)
   }
 }
 
diff --git a/src/Tools/jEdit/src/jedit_sessions.scala b/src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala
+++ b/src/Tools/jEdit/src/jedit_sessions.scala
@@ -1,152 +1,152 @@
 /*  Title:      Tools/jEdit/src/jedit_sessions.scala
     Author:     Makarius
 
 Isabelle/jEdit session information, based on implicit process environment
 and explicit options.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import scala.swing.ComboBox
 import scala.swing.event.SelectionChanged
 
 
 object JEdit_Sessions
 {
   /* session options */
 
   def session_dirs(): List[Path] =
     Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-")
 
   def session_no_build(): Boolean =
     Isabelle_System.getenv("JEDIT_NO_BUILD") == "true"
 
   def session_options(options: Options): Options =
   {
     val options1 =
       Isabelle_System.getenv("JEDIT_BUILD_MODE") match {
         case "default" => options
         case mode => options.bool.update("system_heaps", mode == "system")
       }
 
     val options2 =
       Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
         case "" => options1
         case s => options1.string.update("ML_process_policy", s)
       }
 
     options2
   }
 
   def sessions_structure(options: Options, dirs: List[Path] = session_dirs()): Sessions.Structure =
     Sessions.load_structure(session_options(options), dirs = dirs)
 
 
   /* raw logic info */
 
   private val jedit_logic_option = "jedit_logic"
 
   def logic_name(options: Options): String =
     Isabelle_System.default_logic(
       Isabelle_System.getenv("JEDIT_LOGIC"),
       options.string(jedit_logic_option))
 
   def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
   def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
   def logic_include_sessions: List[String] =
     space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
 
   def logic_info(options: Options): Option[Sessions.Info] =
     try { sessions_structure(options).get(logic_name(options)) }
     catch { case ERROR(_) => None }
 
   def logic_root(options: Options): Position.T =
     if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none
     else Position.none
 
 
   /* logic selector */
 
   private class Logic_Entry(val name: String, val description: String)
   {
     override def toString: String = description
   }
 
   def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component =
   {
     GUI_Thread.require {}
 
     val session_list =
     {
       val sessions = sessions_structure(options.value)
       val (main_sessions, other_sessions) =
         sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main"))
       main_sessions.sorted ::: other_sessions.sorted
     }
 
     val entries =
       new Logic_Entry("", "default (" + logic_name(options.value) + ")") ::
         session_list.map(name => new Logic_Entry(name, name))
 
     val component = new ComboBox(entries) with Option_Component {
       name = jedit_logic_option
       val title = "Logic"
-      def load: Unit =
+      def load(): Unit =
       {
         val logic = options.string(jedit_logic_option)
         entries.find(_.name == logic) match {
           case Some(entry) => selection.item = entry
           case None =>
         }
       }
-      def save: Unit = options.string(jedit_logic_option) = selection.item.name
+      def save(): Unit = options.string(jedit_logic_option) = selection.item.name
     }
 
     component.load()
     if (autosave) {
       component.listenTo(component.selection)
       component.reactions += { case SelectionChanged(_) => component.save() }
     }
     component.tooltip = "Logic session name (change requires restart)"
     component
   }
 
 
   /* session build process */
 
   def session_base_info(options: Options): Sessions.Base_Info =
     Sessions.base_info(options,
       dirs = JEdit_Sessions.session_dirs(),
       include_sessions = logic_include_sessions,
       session = logic_name(options),
       session_ancestor = logic_ancestor,
       session_requirements = logic_requirements)
 
   def session_build(
     options: Options, progress: Progress = new Progress, no_build: Boolean = false): Int =
   {
     Build.build(session_options(options),
       selection = Sessions.Selection.session(PIDE.resources.session_name),
       progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs(),
       infos = PIDE.resources.session_base_info.infos).rc
   }
 
   def session_start(options0: Options)
   {
     val session = PIDE.session
     val options = session_options(options0)
     val sessions_structure = PIDE.resources.session_base_info.sessions_structure
     val store = Sessions.store(options)
 
     session.phase_changed += PIDE.plugin.session_phase_changed
 
     Isabelle_Process(session, options, sessions_structure, store,
       logic = PIDE.resources.session_name,
       modes =
         (space_explode(',', options.string("jedit_print_mode")) :::
          space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)
   }
 }
diff --git a/src/Tools/jEdit/src/jedit_spell_checker.scala b/src/Tools/jEdit/src/jedit_spell_checker.scala
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala
@@ -1,109 +1,109 @@
 /*  Title:      Tools/jEdit/src/jedit_spell_checker.scala
     Author:     Makarius
 
 Specific spell-checker support for Isabelle/jEdit.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import javax.swing.JMenuItem
 import scala.swing.ComboBox
 
 import org.gjt.sp.jedit.menu.EnhancedMenuItem
 import org.gjt.sp.jedit.jEdit
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 
 
 object JEdit_Spell_Checker
 {
   /* completion */
 
   def completion(
     rendering: JEdit_Rendering, explicit: Boolean, caret: Text.Offset): Option[Completion.Result] =
   {
     PIDE.plugin.spell_checker.get match {
       case Some(spell_checker) if explicit =>
         spell_checker.completion(rendering, caret)
       case _ => None
     }
   }
 
 
   /* context menu */
 
   def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
   {
     val result =
       for {
         spell_checker <- PIDE.plugin.spell_checker.get
         doc_view <- Document_View.get(text_area)
         rendering = doc_view.get_rendering()
         range = JEdit_Lib.point_range(text_area.getBuffer, offset)
         Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
       } yield (spell_checker, word)
 
     result match {
       case Some((spell_checker, word)) =>
 
         val context = jEdit.getActionContext()
         def item(name: String): JMenuItem =
           new EnhancedMenuItem(context.getAction(name).getLabel, name, context)
 
         val complete_items =
           if (spell_checker.complete(word).nonEmpty) List(item("isabelle.complete-word"))
           else Nil
 
         val update_items =
           if (spell_checker.check(word))
             List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
           else
             List(item("isabelle.include-word"), item("isabelle.include-word-permanently"))
 
         val reset_items =
           spell_checker.reset_enabled() match {
             case 0 => Nil
             case n =>
               val name = "isabelle.reset-words"
               val label = context.getAction(name).getLabel
               List(new EnhancedMenuItem(label + " (" + n + ")", name, context))
           }
 
         complete_items ::: update_items ::: reset_items
 
       case None => Nil
     }
   }
 
 
   /* dictionaries */
 
   def dictionaries_selector(): Option_Component =
   {
     GUI_Thread.require {}
 
     val option_name = "spell_checker_dictionary"
     val opt = PIDE.options.value.check_name(option_name)
 
     val entries = Spell_Checker.dictionaries()
     val component = new ComboBox(entries) with Option_Component {
       name = option_name
       val title = opt.title()
-      def load: Unit =
+      def load(): Unit =
       {
         val lang = PIDE.options.string(option_name)
         entries.find(_.lang == lang) match {
           case Some(entry) => selection.item = entry
           case None =>
         }
       }
-      def save: Unit = PIDE.options.string(option_name) = selection.item.lang
+      def save(): Unit = PIDE.options.string(option_name) = selection.item.lang
     }
 
     component.load()
     component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
   }
 }
diff --git a/src/Tools/jEdit/src/token_markup.scala b/src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala
+++ b/src/Tools/jEdit/src/token_markup.scala
@@ -1,314 +1,314 @@
 /*  Title:      Tools/jEdit/src/token_markup.scala
     Author:     Makarius
 
 Outer syntax token markup.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import javax.swing.text.Segment
 
 import scala.collection.JavaConverters
 
 import org.gjt.sp.jedit.{Mode, Buffer}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
   ParserRuleSet, ModeProvider, XModeHandler}
 import org.gjt.sp.jedit.indent.IndentRule
 import org.gjt.sp.jedit.buffer.JEditBuffer
 
 
 object Token_Markup
 {
   /* line context */
 
   object Line_Context
   {
     def init(mode: String): Line_Context =
       new Line_Context(mode, Some(Scan.Finished), Line_Structure.init)
 
     def before(buffer: JEditBuffer, line: Int): Line_Context =
       if (line == 0) init(JEdit_Lib.buffer_mode(buffer))
       else after(buffer, line - 1)
 
     def after(buffer: JEditBuffer, line: Int): Line_Context =
     {
       val line_mgr = JEdit_Lib.buffer_line_manager(buffer)
       def context =
         line_mgr.getLineContext(line) match {
           case c: Line_Context => Some(c)
           case _ => None
         }
       context getOrElse {
         buffer.markTokens(line, DummyTokenHandler.INSTANCE)
         context getOrElse init(JEdit_Lib.buffer_mode(buffer))
       }
     }
   }
 
   class Line_Context(
       val mode: String,
       val context: Option[Scan.Line_Context],
       val structure: Line_Structure)
     extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null)
   {
     def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished)
 
     override def hashCode: Int = (mode, context, structure).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Line_Context =>
           mode == other.mode && context == other.context && structure == other.structure
         case _ => false
       }
   }
 
 
   /* tokens from line (inclusive) */
 
   private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
     : Option[List[Token]] =
   {
     val line_context = Line_Context.before(buffer, line)
     for {
       ctxt <- line_context.context
       text <- JEdit_Lib.get_text(buffer, JEdit_Lib.line_range(buffer, line))
     } yield Token.explode_line(syntax.keywords, text, ctxt)._1
   }
 
   def line_token_iterator(
       syntax: Outer_Syntax,
       buffer: JEditBuffer,
       start_line: Int,
       end_line: Int): Iterator[Text.Info[Token]] =
     for {
       line <- Range(start_line max 0, end_line min buffer.getLineCount).iterator
       tokens <- try_line_tokens(syntax, buffer, line).iterator
       starts =
         tokens.iterator.scanLeft(buffer.getLineStartOffset(line))(
           (i, tok) => i + tok.source.length)
       (i, tok) <- starts zip tokens.iterator
     } yield Text.Info(Text.Range(i, i + tok.source.length), tok)
 
   def line_token_reverse_iterator(
       syntax: Outer_Syntax,
       buffer: JEditBuffer,
       start_line: Int,
       end_line: Int): Iterator[Text.Info[Token]] =
     for {
       line <- Range(start_line min (buffer.getLineCount - 1), end_line max -1, -1).iterator
       tokens <- try_line_tokens(syntax, buffer, line).iterator
       stops =
         tokens.reverseIterator.scanLeft(buffer.getLineEndOffset(line) min buffer.getLength)(
           (i, tok) => i - tok.source.length)
       (i, tok) <- stops zip tokens.reverseIterator
     } yield Text.Info(Text.Range(i - tok.source.length, i), tok)
 
 
   /* tokens from offset (inclusive) */
 
   def token_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
       Iterator[Text.Info[Token]] =
     if (JEdit_Lib.buffer_range(buffer).contains(offset))
       line_token_iterator(syntax, buffer, buffer.getLineOfOffset(offset), buffer.getLineCount).
         dropWhile(info => !info.range.contains(offset))
     else Iterator.empty
 
   def token_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
       Iterator[Text.Info[Token]] =
     if (JEdit_Lib.buffer_range(buffer).contains(offset))
       line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1).
         dropWhile(info => !info.range.contains(offset))
     else Iterator.empty
 
 
   /* command spans */
 
   def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
     : Option[Text.Info[Command_Span.Span]] =
   {
     val keywords = syntax.keywords
 
     def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
       token_reverse_iterator(syntax, buffer, i).
         find(info => keywords.is_before_command(info.info) || info.info.is_command)
 
     def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
       token_iterator(syntax, buffer, i).
         find(info => keywords.is_before_command(info.info) || info.info.is_command)
 
     if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
       val start_info =
       {
         val info1 = maybe_command_start(offset)
         info1 match {
           case Some(Text.Info(range1, tok1)) if tok1.is_command =>
             val info2 = maybe_command_start(range1.start - 1)
             info2 match {
               case Some(Text.Info(_, tok2)) if keywords.is_before_command(tok2) => info2
               case _ => info1
             }
           case _ => info1
         }
       }
       val (start_before_command, start, start_next) =
         start_info match {
           case Some(Text.Info(range, tok)) =>
             (keywords.is_before_command(tok), range.start, range.stop)
           case None => (false, 0, 0)
         }
 
       val stop_info =
       {
         val info1 = maybe_command_stop(start_next)
         info1 match {
           case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command =>
             maybe_command_stop(range1.stop)
           case _ => info1
         }
       }
       val stop =
         stop_info match {
           case Some(Text.Info(range, _)) => range.start
           case None => buffer.getLength
         }
 
       val text = JEdit_Lib.get_text(buffer, Text.Range(start, stop)).getOrElse("")
       val spans = syntax.parse_spans(text)
 
       (spans.iterator.scanLeft(start)(_ + _.length) zip spans.iterator).
         map({ case (i, span) => Text.Info(Text.Range(i, i + span.length), span) }).
         find(_.range.contains(offset))
     }
     else None
   }
 
   private def _command_span_iterator(
       syntax: Outer_Syntax,
       buffer: JEditBuffer,
       offset: Text.Offset,
       next_offset: Text.Range => Text.Offset): Iterator[Text.Info[Command_Span.Span]] =
     new Iterator[Text.Info[Command_Span.Span]]
     {
       private var next_span = command_span(syntax, buffer, offset)
       def hasNext: Boolean = next_span.isDefined
-      def next: Text.Info[Command_Span.Span] =
+      def next(): Text.Info[Command_Span.Span] =
       {
         val span = next_span.getOrElse(Iterator.empty.next)
         next_span = command_span(syntax, buffer, next_offset(span.range))
         span
       }
     }
 
   def command_span_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
       : Iterator[Text.Info[Command_Span.Span]] =
     _command_span_iterator(syntax, buffer, offset max 0, range => range.stop)
 
   def command_span_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
       : Iterator[Text.Info[Command_Span.Span]] =
     _command_span_iterator(syntax, buffer,
       (offset min buffer.getLength) - 1, range => range.start - 1)
 
 
   /* token marker */
 
   class Marker(
     protected val mode: String,
     protected val opt_buffer: Option[Buffer]) extends TokenMarker
   {
     override def hashCode: Int = (mode, opt_buffer).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Marker => mode == other.mode && opt_buffer == other.opt_buffer
         case _ => false
       }
 
     override def toString: String =
       opt_buffer match {
         case None => "Marker(" + mode + ")"
         case Some(buffer) => "Marker(" + mode + "," + JEdit_Lib.buffer_name(buffer) + ")"
       }
 
     override def markTokens(context: TokenMarker.LineContext,
         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
     {
       val line = if (raw_line == null) new Segment else raw_line
       val line_context =
         context match { case c: Line_Context => c case _ => Line_Context.init(mode) }
       val structure = line_context.structure
 
       val context1 =
       {
         val opt_syntax =
           opt_buffer match {
             case Some(buffer) => Isabelle.buffer_syntax(buffer)
             case None => Isabelle.mode_syntax(mode)
           }
         val (styled_tokens, context1) =
           (line_context.context, opt_syntax) match {
             case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
               val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
               val styled_tokens =
                 tokens.map(tok => (JEdit_Rendering.ml_token_markup(tok), tok.source))
               (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure))
 
             case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
               val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt)
               val structure1 = structure.update(syntax.keywords, tokens)
               val styled_tokens =
                 tokens.map(tok => (JEdit_Rendering.token_markup(syntax, tok), tok.source))
               (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1))
 
             case _ =>
               val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
               (List(styled_token), new Line_Context(line_context.mode, None, structure))
           }
 
         val extended = Syntax_Style.extended(line)
         def special(i: Int): Boolean = extended.isDefinedAt(i) || line.charAt(i) == '\t'
 
         var offset = 0
         for ((style, token) <- styled_tokens) {
           val length = token.length
           if ((offset until (offset + length)).exists(special)) {
             for ((c, i) <- Codepoint.iterator_offset(token)) {
               val style1 =
                 extended.get(offset + i) match {
                   case None => style
                   case Some(ext) => ext(style)
                 }
               handler.handleToken(line, style1, offset + i, Character.charCount(c), context1)
             }
           }
           else handler.handleToken(line, style, offset, length, context1)
           offset += length
         }
         handler.handleToken(line, JEditToken.END, line.count, 0, context1)
         context1
       }
 
       val context2 = context1.intern
       handler.setLineContext(context2)
       context2
     }
   }
 
 
   /* mode provider */
 
   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   {
     for (mode <- orig_provider.getModes) addMode(mode)
 
     override def loadMode(mode: Mode, xmh: XModeHandler)
     {
       super.loadMode(mode, xmh)
       Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
       Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
         Untyped.set[java.util.List[IndentRule]](
           mode, "indentRules", JavaConverters.seqAsJavaList(List(indent_rule))))
     }
   }
 }