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,373 +1,413 @@
 /*  Title:      Pure/GUI/gui.scala
     Author:     Makarius
 
 Basic GUI tools (for AWT/Swing).
 */
 
 package isabelle
 
 import java.util.{Map => JMap}
 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.{CheckBox, ComboBox, ScrollPane, TextArea}
+
+import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator,
+  Orientation}
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 
 object GUI {
   /* Swing look-and-feel */
 
   def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.setup()
 
   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(): Unit = {
     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): Unit = {
     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]
   ): Unit = {
     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)
     }
 
 
   /* basic GUI components */
 
   class Button(label: String) extends scala.swing.Button(label) {
     def clicked(): Unit = {}
 
     reactions += { case ButtonClicked(_) => clicked() }
   }
 
   class Check(label: String, init: Boolean = false) extends CheckBox(label) {
     def clicked(state: Boolean): Unit = {}
     def clicked(): Unit = {}
 
     selected = init
     reactions += { case ButtonClicked(_) => clicked(selected); clicked() }
   }
 
-  class Selector[A](val entries: List[A]) extends ComboBox[A](entries) {
+
+  /* list selector */
+
+  object Selector {
+    sealed abstract class Entry[A] {
+      def get_item: Option[A] =
+        this match {
+          case Item(item, _) => Some(item)
+          case _ => None
+        }
+    }
+    case class Item[A](item: A, description: String = "") extends Entry[A] {
+      override def toString: String = proper_string(description) getOrElse item.toString
+    }
+    case class Separator[A](name: String = "") extends Entry[A] {
+      override def toString: String = "<b>" + name + "</b>"
+    }
+
+    def item(name: String): Item[String] = Item(name)
+    def separator: Separator[String] = Separator()
+  }
+
+  class Selector[A](val entries: List[Selector.Entry[A]])
+  extends ComboBox[Selector.Entry[A]](entries) {
     def changed(): Unit = {}
 
+    private val default_renderer = renderer
+    private val render_separator = new Separator
+    private val render_label = new Label
+    renderer =
+      (list: ListView[_ <: Selector.Entry[A]], selected: Boolean, focus: Boolean, entry: Selector.Entry[A], i: Int) => {
+        entry match {
+          case sep: Selector.Separator[_] =>
+            if (sep.name.isEmpty) render_separator
+            else { render_label.text = entry.toString; render_label }
+          case _ => default_renderer.componentFor(list, selected, focus, entry, i)
+        }
+      }
+
     listenTo(selection)
     reactions += { case SelectionChanged(_) => changed() }
   }
 
 
   /* zoom factor */
 
   private val Zoom_Factor = "([0-9]+)%?".r
 
   class Zoom extends Selector[String](
     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")
+      .map(GUI.Selector.item)
   ) {
-    def factor: Int = parse(selection.item)
+    def factor: Int = parse(selection.item.toString)
 
     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): Unit = {
       peer.getEditor match {
         case null =>
         case editor => editor.setItem(print(i))
       }
     }
 
-    makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
+    makeEditable()(c =>
+      new ComboBox.BuiltInEditor(c)(text => Selector.Item(print(parse(text))), _.toString))
     peer.getEditor.getEditorComponent match {
       case text: JTextField => text.setColumns(4)
       case _ =>
     }
 
     selection.index = 3
   }
 
 
   /* 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 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): Unit = {
     def traverse(comp: Component): Unit = {
       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(JMap.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(): Unit = {
     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/Thy/sessions.scala b/src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala
+++ b/src/Pure/Thy/sessions.scala
@@ -1,1550 +1,1553 @@
 /*  Title:      Pure/Thy/sessions.scala
     Author:     Makarius
 
 Cumulative session information.
 */
 
 package isabelle
 
 import java.io.{File => JFile}
 import java.nio.ByteBuffer
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption
 import java.sql.SQLException
 
 import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.collection.mutable
 
 
 object Sessions {
   /* session and theory names */
 
   val ROOTS: Path = Path.explode("ROOTS")
   val ROOT: Path = Path.explode("ROOT")
 
   val roots_name: String = "ROOTS"
   val root_name: String = "ROOT"
   val theory_import: String = "Pure.Sessions"
 
   val UNSORTED = "Unsorted"
   val DRAFT = "Draft"
 
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
   def illegal_session(name: String): Boolean = name == "" || name == DRAFT
   def illegal_theory(name: String): Boolean = name == root_name || name == "bib"
 
 
   /* ROOTS file format */
 
   class File_Format extends isabelle.File_Format {
     val format_name: String = roots_name
     val file_ext = ""
 
     override def detect(name: String): Boolean =
       Thy_Header.split_file_name(name) match {
         case Some((_, file_name)) => file_name == roots_name
         case None => false
       }
 
     override def theory_suffix: String = "ROOTS_file"
     override def theory_content(name: String): String =
       """theory "ROOTS" imports Pure begin ROOTS_file """ +
         Outer_Syntax.quote_string(name) + """ end"""
   }
 
 
   /* base info and source dependencies */
 
   sealed case class Base(
     session_name: String = "",
     session_pos: Position.T = Position.none,
     proper_session_theories: List[Document.Node.Name] = Nil,
     document_theories: List[Document.Node.Name] = Nil,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,  // cumulative imports
     used_theories: List[(Document.Node.Name, Options)] = Nil,  // new imports
     load_commands: Map[Document.Node.Name, List[Command_Span.Span]] = Map.empty,
     known_theories: Map[String, Document.Node.Entry] = Map.empty,
     known_loaded_files: Map[String, List[Path]] = Map.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     imported_sources: List[(Path, SHA1.Digest)] = Nil,
     session_sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph,
     errors: List[String] = Nil
   ) {
     def session_entry: (String, Base) = session_name -> this
 
     override def toString: String =
       "Sessions.Base(session_name = " + quote(session_name) +
         ", loaded_theories = " + loaded_theories.size +
         ", used_theories = " + used_theories.length + ")"
 
     def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
     def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
 
     def loaded_theory_syntax(name: String): Option[Outer_Syntax] =
       if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None
     def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
       loaded_theory_syntax(name.theory)
 
     def theory_syntax(name: Document.Node.Name): Outer_Syntax =
       loaded_theory_syntax(name) getOrElse overall_syntax
 
     def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   }
 
   val bootstrap_base: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
 
   sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
     override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
 
     def is_empty: Boolean = session_bases.keysIterator.forall(_.isEmpty)
     def apply(name: String): Base = session_bases(name)
     def get(name: String): Option[Base] = session_bases.get(name)
 
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
     def session_sources(name: String): List[SHA1.Digest] =
       session_bases(name).session_sources.map(_._2)
 
     def errors: List[String] =
       (for {
         (name, base) <- session_bases.iterator
         if base.errors.nonEmpty
       } yield cat_lines(base.errors) +
           "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.session_pos)
       ).toList
 
     def check_errors: Deps =
       errors match {
         case Nil => this
         case errs => error(cat_lines(errs))
       }
 
     def base_info(session: String): Base_Info =
       Base_Info(base = apply(session), sessions_structure = sessions_structure, errors = errors)
   }
 
   def deps(sessions_structure: Structure,
     progress: Progress = new Progress,
     inlined_files: Boolean = false,
     verbose: Boolean = false,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty
   ): Deps = {
     var cache_sources = Map.empty[JFile, SHA1.Digest]
     def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = {
       for {
         path <- paths
         file = path.file
         if cache_sources.isDefinedAt(file) || file.isFile
       }
       yield {
         cache_sources.get(file) match {
           case Some(digest) => (path, digest)
           case None =>
             val digest = SHA1.digest(file)
             cache_sources = cache_sources + (file -> digest)
             (path, digest)
         }
       }
     }
 
     val session_bases =
       sessions_structure.imports_topological_order.foldLeft(
           Map(Sessions.bootstrap_base.session_entry)) {
         case (session_bases, session_name) =>
           progress.expose_interrupt()
 
           val info = sessions_structure(session_name)
           try {
             val deps_base = info.deps_base(session_bases)
             val resources = new Resources(sessions_structure, deps_base)
 
             if (verbose || list_files) {
               val groups =
                 if (info.groups.isEmpty) ""
                 else info.groups.mkString(" (", " ", ")")
               progress.echo("Session " + info.chapter + "/" + session_name + groups)
             }
 
             val dependencies = resources.session_dependencies(info)
 
             val overall_syntax = dependencies.overall_syntax
 
             val proper_session_theories =
               dependencies.theories.filter(name =>
                 sessions_structure.theory_qualifier(name) == session_name)
 
             val theory_files = dependencies.theories.map(_.path)
 
             val (load_commands, load_commands_errors) =
               try { if (inlined_files) (dependencies.load_commands, Nil) else (Nil, Nil) }
               catch { case ERROR(msg) => (Nil, List(msg)) }
 
             val loaded_files =
               load_commands.map({ case (name, spans) => dependencies.loaded_files(name, spans) })
 
             val session_files =
               (theory_files ::: loaded_files.flatMap(_._2) :::
                 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
 
             val imported_files = if (inlined_files) dependencies.imported_files else Nil
 
             if (list_files) {
               progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
             }
 
             if (check_keywords.nonEmpty) {
               Check_Keywords.check_keywords(
                 progress, overall_syntax.keywords, check_keywords, theory_files)
             }
 
             val session_graph_display: Graph_Display.Graph = {
               def session_node(name: String): Graph_Display.Node =
                 Graph_Display.Node("[" + name + "]", "session." + name)
 
               def node(name: Document.Node.Name): Graph_Display.Node = {
                 val qualifier = sessions_structure.theory_qualifier(name)
                 if (qualifier == info.name) {
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
                 }
                 else session_node(qualifier)
               }
 
               val required_sessions =
                 dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory))
                   .map(theory => sessions_structure.theory_qualifier(theory))
                   .filter(name => name != info.name && sessions_structure.defined(name))
 
               val required_subgraph =
                 sessions_structure.imports_graph
                   .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet)
                   .transitive_closure
                   .restrict(required_sessions.toSet)
                   .transitive_reduction_acyclic
 
               val graph0 =
                 required_subgraph.topological_order.foldLeft(Graph_Display.empty_graph) {
                   case (g, session) =>
                     val a = session_node(session)
                     val bs = required_subgraph.imm_preds(session).toList.map(session_node)
                     bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a))
                 }
 
               dependencies.entries.foldLeft(graph0) {
                 case (g, entry) =>
                   val a = node(entry.name)
                   val bs = entry.header.imports.map(node).filterNot(_ == a)
                   bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a))
               }
             }
 
             val known_theories =
               dependencies.entries.iterator.map(entry => entry.name.theory -> entry).
                 foldLeft(deps_base.known_theories)(_ + _)
 
             val known_loaded_files = deps_base.known_loaded_files ++ loaded_files
 
             val import_errors = {
               val known_sessions =
                 sessions_structure.imports_requirements(List(session_name)).toSet
               for {
                 name <- dependencies.theories
                 qualifier = sessions_structure.theory_qualifier(name)
                 if !known_sessions(qualifier)
               } yield "Bad import of theory " + quote(name.toString) +
                 ": need to include sessions " + quote(qualifier) + " in ROOT"
             }
 
             val document_errors =
               info.document_theories.flatMap(
               {
                 case (thy, pos) =>
                   val build_hierarchy =
                     if (sessions_structure.build_graph.defined(session_name)) {
                       sessions_structure.build_hierarchy(session_name)
                     }
                     else Nil
 
                   def err(msg: String): Option[String] =
                     Some(msg + " " + quote(thy) + Position.here(pos))
 
                   known_theories.get(thy).map(_.name) match {
                     case None => err("Unknown document theory")
                     case Some(name) =>
                       val qualifier = sessions_structure.theory_qualifier(name)
                       if (proper_session_theories.contains(name)) {
                         err("Redundant document theory from this session:")
                       }
                       else if (build_hierarchy.contains(qualifier)) None
                       else if (dependencies.theories.contains(name)) None
                       else err("Document theory from other session not imported properly:")
                   }
               })
             val document_theories =
               info.document_theories.map({ case (thy, _) => known_theories(thy).name })
 
             val dir_errors = {
               val ok = info.dirs.map(_.canonical_file).toSet
               val bad =
                 (for {
                   name <- proper_session_theories.iterator
                   path = name.master_dir_path
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
                 } yield (path1, name)).toList
               val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted
 
               val errs1 =
                 for { (path1, name) <- bad }
                 yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString)
               val errs2 =
                 if (bad_dirs.isEmpty) Nil
                 else List("Implicit use of session directories: " + commas(bad_dirs))
               val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
               val errs4 =
                 (for {
                   name <- proper_session_theories.iterator
                   name1 <- resources.find_theory_node(name.theory)
                   if name.node != name1.node
                 } yield "Incoherent theory file import:\n  " + name.path + " vs. \n  " + name1.path)
                 .toList
 
               errs1 ::: errs2 ::: errs3 ::: errs4
             }
 
             val sources_errors =
               for (p <- session_files if !p.is_file) yield "No such file: " + p
 
             val path_errors =
               try { Path.check_case_insensitive(session_files ::: imported_files); Nil }
               catch { case ERROR(msg) => List(msg) }
 
             val bibtex_errors =
               try { info.bibtex_entries; Nil }
               catch { case ERROR(msg) => List(msg) }
 
             val base =
               Base(
                 session_name = info.name,
                 session_pos = info.pos,
                 proper_session_theories = proper_session_theories,
                 document_theories = document_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = dependencies.theories_adjunct,
                 load_commands = load_commands.toMap,
                 known_theories = known_theories,
                 known_loaded_files = known_loaded_files,
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),
                 session_sources = check_sources(session_files),
                 session_graph_display = session_graph_display,
                 errors = dependencies.errors ::: load_commands_errors ::: import_errors :::
                   document_errors ::: dir_errors ::: sources_errors ::: path_errors :::
                   bibtex_errors)
 
             session_bases + base.session_entry
           }
           catch {
             case ERROR(msg) =>
               cat_error(msg, "The error(s) above occurred in session " +
                 quote(info.name) + Position.here(info.pos))
           }
       }
 
     Deps(sessions_structure, session_bases)
   }
 
 
   /* base info */
 
   sealed case class Base_Info(
     base: Base,
     sessions_structure: Structure = Structure.empty,
     errors: List[String] = Nil,
     infos: List[Info] = Nil
   ) {
     def session_name: String = base.session_name
 
     def check_errors: Base_Info =
       if (errors.isEmpty) this
       else error(cat_lines(errors))
   }
 
   def base_info0(session: String): Base_Info =
     Base_Info(Base(session_name = session))
 
   def base_info(options: Options,
     session: String,
     progress: Progress = new Progress,
     dirs: List[Path] = Nil,
     include_sessions: List[String] = Nil,
     session_ancestor: Option[String] = None,
     session_requirements: Boolean = false
   ): Base_Info = {
     val full_sessions = load_structure(options, dirs = dirs)
 
     val selected_sessions =
       full_sessions.selection(Selection(sessions = session :: session_ancestor.toList))
     val info = selected_sessions(session)
     val ancestor = session_ancestor orElse info.parent
 
     val (session1, infos1) =
       if (session_requirements && ancestor.isDefined) {
         val deps = Sessions.deps(selected_sessions, progress = progress)
         val base = deps(session)
 
         val ancestor_loaded =
           deps.get(ancestor.get) match {
             case Some(ancestor_base)
             if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) =>
               ancestor_base.loaded_theories.defined _
             case _ =>
               error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
           }
 
         val required_theories =
           for {
             thy <- base.loaded_theories.keys
             if !ancestor_loaded(thy) && selected_sessions.theory_qualifier(thy) != session
           }
           yield thy
 
         if (required_theories.isEmpty) (ancestor.get, Nil)
         else {
           val other_name = info.name + "_requirements(" + ancestor.get + ")"
           Isabelle_System.isabelle_tmp_prefix()
 
           (other_name,
             List(
               make_info(
                 Chapter_Defs.empty,
                 info.options,
                 dir_selected = false,
                 dir = Path.explode("$ISABELLE_TMP_PREFIX"),
                 chapter = info.chapter,
                 Session_Entry(
                   pos = info.pos,
                   name = other_name,
                   groups = info.groups,
                   path = ".",
                   parent = ancestor,
                   description = "Required theory imports from other sessions",
                   options = Nil,
                   imports = info.deps,
                   directories = Nil,
                   theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
                   document_theories = Nil,
                   document_files = Nil,
                   export_files = Nil,
                   export_classpath = Nil))))
         }
       }
       else (session, Nil)
 
     val full_sessions1 =
       if (infos1.isEmpty) full_sessions
       else load_structure(options, dirs = dirs, infos = infos1)
 
     val selected_sessions1 =
       full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions))
 
     val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
     Base_Info(deps1(session1), sessions_structure = full_sessions1,
       errors = deps1.errors, infos = infos1)
   }
 
 
   /* cumulative session info */
 
   sealed case class Chapter_Info(
     name: String,
     pos: Position.T,
     groups: List[String],
     description: String,
     sessions: List[String]
   )
 
   sealed case class Info(
     name: String,
     chapter: String,
     dir_selected: Boolean,
     pos: Position.T,
     groups: List[String],
     dir: Path,
     parent: Option[String],
     description: String,
     directories: List[Path],
     options: Options,
     imports: List[String],
     theories: List[(Options, List[(String, Position.T)])],
     global_theories: List[String],
     document_theories: List[(String, Position.T)],
     document_files: List[(Path, Path)],
     export_files: List[(Path, Int, List[String])],
     export_classpath: List[String],
     meta_digest: SHA1.Digest
   ) {
     def deps: List[String] = parent.toList ::: imports
 
     def deps_base(session_bases: String => Base): Base = {
       val parent_base = session_bases(parent.getOrElse(""))
       val imports_bases = imports.map(session_bases)
       parent_base.copy(
         known_theories =
           (for {
             base <- imports_bases.iterator
             (_, entry) <- base.known_theories.iterator
           } yield (entry.name.theory -> entry)).foldLeft(parent_base.known_theories)(_ + _),
         known_loaded_files =
           imports_bases.iterator.map(_.known_loaded_files).
             foldLeft(parent_base.known_loaded_files)(_ ++ _))
     }
 
     def dirs: List[Path] = dir :: directories
 
+    def main_group: Boolean = groups.contains("main")
+    def doc_group: Boolean = groups.contains("doc")
+
     def timeout_ignored: Boolean =
       !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
 
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
     def document_enabled: Boolean =
       options.string("document") match {
         case "" | "false" => false
         case "pdf" | "true" => true
         case doc => error("Bad document specification " + quote(doc))
       }
 
     def document_variants: List[Document_Build.Document_Variant] = {
       val variants =
         Library.space_explode(':', options.string("document_variants")).
           map(Document_Build.Document_Variant.parse)
 
       val dups = Library.duplicates(variants.map(_.name))
       if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups))
 
       variants
     }
 
     def document_echo: Boolean = options.bool("document_echo")
 
     def documents: List[Document_Build.Document_Variant] = {
       val variants = document_variants
       if (!document_enabled || document_files.isEmpty) Nil else variants
     }
 
     def document_output: Option[Path] =
       options.string("document_output") match {
         case "" => None
         case s => Some(dir + Path.explode(s))
       }
 
     def browser_info: Boolean = options.bool("browser_info")
 
     lazy val bibtex_entries: List[Text.Info[String]] =
       (for {
         (document_dir, file) <- document_files.iterator
         if File.is_bib(file.file_name)
         info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
       } yield info).toList
 
     def record_proofs: Boolean = options.int("record_proofs") >= 2
 
     def is_afp: Boolean = chapter == AFP.chapter
     def is_afp_bulky: Boolean = is_afp && groups.exists(AFP.groups_bulky.contains)
   }
 
   def make_info(
     chapter_defs: Chapter_Defs,
     options: Options,
     dir_selected: Boolean,
     dir: Path,
     chapter: String,
     entry: Session_Entry
   ): Info = {
     try {
       val name = entry.name
 
       if (illegal_session(name)) error("Illegal session name " + quote(name))
       if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
       if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
       val session_path = dir + Path.explode(entry.path)
       val directories = entry.directories.map(dir => session_path + Path.explode(dir))
 
       val session_options = options ++ entry.options
 
       val theories =
         entry.theories.map({ case (opts, thys) =>
           (session_options ++ opts,
             thys.map({ case ((thy, pos), _) =>
               val thy_name = Thy_Header.import_name(thy)
               if (illegal_theory(thy_name)) {
                 error("Illegal theory name " + quote(thy_name) + Position.here(pos))
               }
               else (thy, pos) })) })
 
       val global_theories =
         for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
         yield {
           val thy_name = Path.explode(thy).file_name
           if (Long_Name.is_qualified(thy_name)) {
             error("Bad qualified name for global theory " +
               quote(thy_name) + Position.here(pos))
           }
           else thy_name
         }
 
       val conditions =
         theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted.
           map(x => (x, Isabelle_System.getenv(x) != ""))
 
       val document_files =
         entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
 
       val export_files =
         entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) })
 
       val meta_digest =
         SHA1.digest(
           (name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
             entry.theories_no_position, conditions, entry.document_theories_no_position,
             entry.document_files)
           .toString)
 
       val chapter_groups = chapter_defs(chapter).groups
       val groups = chapter_groups ::: entry.groups.filterNot(chapter_groups.contains)
 
       Info(name, chapter, dir_selected, entry.pos, groups, session_path,
         entry.parent, entry.description, directories, session_options,
         entry.imports, theories, global_theories, entry.document_theories, document_files,
         export_files, entry.export_classpath, meta_digest)
     }
     catch {
       case ERROR(msg) =>
         error(msg + "\nThe error(s) above occurred in session entry " +
           quote(entry.name) + Position.here(entry.pos))
     }
   }
 
   object Selection {
     val empty: Selection = Selection()
     val all: Selection = Selection(all_sessions = true)
     def session(session: String): Selection = Selection(sessions = List(session))
   }
 
   sealed case class Selection(
     requirements: Boolean = false,
     all_sessions: Boolean = false,
     base_sessions: List[String] = Nil,
     exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,
     session_groups: List[String] = Nil,
     sessions: List[String] = Nil
   ) {
     def ++ (other: Selection): Selection =
       Selection(
         requirements = requirements || other.requirements,
         all_sessions = all_sessions || other.all_sessions,
         base_sessions = Library.merge(base_sessions, other.base_sessions),
         exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups),
         exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
         session_groups = Library.merge(session_groups, other.session_groups),
         sessions = Library.merge(sessions, other.sessions))
   }
 
   object Structure {
     val empty: Structure = make(Chapter_Defs.empty, Nil)
 
     def make(chapter_defs: Chapter_Defs, infos: List[Info]): Structure = {
       def add_edges(
         graph: Graph[String, Info],
         kind: String,
         edges: Info => Iterable[String]
       ) : Graph[String, Info] = {
         def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) = {
           if (!g.defined(parent)) {
             error("Bad " + kind + " session " + quote(parent) + " for " +
               quote(name) + Position.here(pos))
           }
 
           try { g.add_edge_acyclic(parent, name) }
           catch {
             case exn: Graph.Cycles[_] =>
               error(cat_lines(exn.cycles.map(cycle =>
                 "Cyclic session dependency of " +
                   cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
           }
         }
         graph.iterator.foldLeft(graph) {
           case (g, (name, (info, _))) =>
             edges(info).foldLeft(g)(add_edge(info.pos, name, _, _))
         }
       }
 
       val info_graph =
         infos.foldLeft(Graph.string[Info]) {
           case (graph, info) =>
             if (graph.defined(info.name)) {
               error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
                 Position.here(graph.get_node(info.name).pos))
             }
             else graph.new_node(info.name, info)
         }
       val build_graph = add_edges(info_graph, "parent", _.parent)
       val imports_graph = add_edges(build_graph, "imports", _.imports)
 
       val session_positions: List[(String, Position.T)] =
         (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList
 
       val session_directories: Map[JFile, String] =
         (for {
           session <- imports_graph.topological_order.iterator
           info = info_graph.get_node(session)
           dir <- info.dirs.iterator
         } yield (info, dir)).foldLeft(Map.empty[JFile, String]) {
             case (dirs, (info, dir)) =>
               val session = info.name
               val canonical_dir = dir.canonical_file
               dirs.get(canonical_dir) match {
                 case Some(session1) =>
                   val info1 = info_graph.get_node(session1)
                   error("Duplicate use of directory " + dir +
                     "\n  for session " + quote(session1) + Position.here(info1.pos) +
                     "\n  vs. session " + quote(session) + Position.here(info.pos))
                 case None => dirs + (canonical_dir -> session)
               }
           }
 
       val global_theories: Map[String, String] =
         (for {
           session <- imports_graph.topological_order.iterator
           info = info_graph.get_node(session)
           thy <- info.global_theories.iterator }
           yield (info, thy)).foldLeft(Thy_Header.bootstrap_global_theories.toMap) {
             case (global, (info, thy)) =>
               val qualifier = info.name
               global.get(thy) match {
                 case Some(qualifier1) if qualifier != qualifier1 =>
                   error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
                 case _ => global + (thy -> qualifier)
               }
           }
 
       new Structure(chapter_defs, session_positions, session_directories,
         global_theories, build_graph, imports_graph)
     }
   }
 
   final class Structure private[Sessions](
     chapter_defs: Chapter_Defs,
     val session_positions: List[(String, Position.T)],
     val session_directories: Map[JFile, String],
     val global_theories: Map[String, String],
     val build_graph: Graph[String, Info],
     val imports_graph: Graph[String, Info]
   ) {
     sessions_structure =>
 
     def bootstrap: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
 
     def dest_session_directories: List[(String, String)] =
       for ((file, session) <- session_directories.toList)
         yield (File.standard_path(file), session)
 
     lazy val known_chapters: List[Chapter_Info] = {
       val chapter_sessions =
         Multi_Map.from(
           for ((_, (info, _)) <- build_graph.iterator)
             yield info.chapter -> info.name)
       val chapters1 =
         (for (entry <- chapter_defs.list.iterator) yield {
           val sessions = chapter_sessions.get_list(entry.name)
           Chapter_Info(entry.name, entry.pos, entry.groups, entry.description, sessions.sorted)
         }).toList
       val chapters2 =
         (for {
           (name, sessions) <- chapter_sessions.iterator_list
           if !chapters1.exists(_.name == name)
         } yield Chapter_Info(name, Position.none, Nil, "", sessions.sorted)).toList.sortBy(_.name)
       chapters1 ::: chapters2
     }
 
     def relevant_chapters: List[Chapter_Info] = known_chapters.filter(_.sessions.nonEmpty)
 
     def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
     def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
 
     def defined(name: String): Boolean = imports_graph.defined(name)
     def apply(name: String): Info = imports_graph.get_node(name)
     def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None
 
     def theory_qualifier(name: String): String =
       global_theories.getOrElse(name, Long_Name.qualifier(name))
     def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory)
 
     def check_sessions(names: List[String]): Unit = {
       val bad_sessions = SortedSet(names.filterNot(defined): _*).toList
       if (bad_sessions.nonEmpty) {
         error("Undefined session(s): " + commas_quote(bad_sessions))
       }
     }
 
     def check_sessions(sel: Selection): Unit =
       check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
 
     private def selected(graph: Graph[String, Info], sel: Selection): List[String] = {
       check_sessions(sel)
 
       val select_group = sel.session_groups.toSet
       val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions)
 
       val selected0 =
         if (sel.all_sessions) graph.keys
         else {
           (for {
             (name, (info, _)) <- graph.iterator
             if info.dir_selected || select_session(name) || info.groups.exists(select_group)
           } yield name).toList
         }
 
       if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
       else selected0
     }
 
     def selection(sel: Selection): Structure = {
       check_sessions(sel)
 
       val excluded = {
         val exclude_group = sel.exclude_session_groups.toSet
         val exclude_group_sessions =
           (for {
             (name, (info, _)) <- imports_graph.iterator
             if imports_graph.get_node(name).groups.exists(exclude_group)
           } yield name).toList
         imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
       }
 
       def restrict(graph: Graph[String, Info]): Graph[String, Info] = {
         val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
         graph.restrict(graph.all_preds(sessions).toSet)
       }
 
       new Structure(chapter_defs, session_positions, session_directories, global_theories,
         restrict(build_graph), restrict(imports_graph))
     }
 
     def selection(session: String): Structure = selection(Selection.session(session))
 
     def selection_deps(
       selection: Selection,
       progress: Progress = new Progress,
       loading_sessions: Boolean = false,
       inlined_files: Boolean = false,
       verbose: Boolean = false
     ): Deps = {
       val deps =
         Sessions.deps(sessions_structure.selection(selection),
           progress = progress, inlined_files = inlined_files, verbose = verbose)
 
       if (loading_sessions) {
         val selection_size = deps.sessions_structure.build_graph.size
         if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...")
       }
 
       deps
     }
 
     def build_hierarchy(session: String): List[String] =
       if (build_graph.defined(session)) build_graph.all_preds(List(session))
       else List(session)
 
     def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
     def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
     def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss)
     def build_topological_order: List[String] = build_graph.topological_order
 
     def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
     def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
     def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
     def imports_topological_order: List[String] = imports_graph.topological_order
 
     def bibtex_entries: List[(String, List[String])] =
       build_topological_order.flatMap(name =>
         apply(name).bibtex_entries match {
           case Nil => None
           case entries => Some(name -> entries.map(_.info))
         })
 
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
   }
 
 
   /* parser */
 
   private val CHAPTER_DEFINITION = "chapter_definition"
   private val CHAPTER = "chapter"
   private val SESSION = "session"
   private val IN = "in"
   private val DESCRIPTION = "description"
   private val DIRECTORIES = "directories"
   private val OPTIONS = "options"
   private val SESSIONS = "sessions"
   private val THEORIES = "theories"
   private val GLOBAL = "global"
   private val DOCUMENT_THEORIES = "document_theories"
   private val DOCUMENT_FILES = "document_files"
   private val EXPORT_FILES = "export_files"
   private val EXPORT_CLASSPATH = "export_classpath"
 
   val root_syntax: Outer_Syntax =
     Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
       GLOBAL + IN +
       (CHAPTER_DEFINITION, Keyword.THY_DECL) +
       (CHAPTER, Keyword.THY_DECL) +
       (SESSION, Keyword.THY_DECL) +
       (DESCRIPTION, Keyword.QUASI_COMMAND) +
       (DIRECTORIES, Keyword.QUASI_COMMAND) +
       (OPTIONS, Keyword.QUASI_COMMAND) +
       (SESSIONS, Keyword.QUASI_COMMAND) +
       (THEORIES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_THEORIES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_FILES, Keyword.QUASI_COMMAND) +
       (EXPORT_FILES, Keyword.QUASI_COMMAND) +
       (EXPORT_CLASSPATH, Keyword.QUASI_COMMAND)
 
   abstract class Entry
   object Chapter_Def {
     def empty(chapter: String): Chapter_Def = Chapter_Def(Position.none, chapter, Nil, "")
   }
   sealed case class Chapter_Def(
     pos: Position.T,
     name: String,
     groups: List[String],
     description: String
   ) extends Entry
   sealed case class Chapter_Entry(name: String) extends Entry
   sealed case class Session_Entry(
     pos: Position.T,
     name: String,
     groups: List[String],
     path: String,
     parent: Option[String],
     description: String,
     options: List[Options.Spec],
     imports: List[String],
     directories: List[String],
     theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
     document_theories: List[(String, Position.T)],
     document_files: List[(String, String)],
     export_files: List[(String, Int, List[String])],
     export_classpath: List[String]
   ) extends Entry {
     def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
       theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
     def document_theories_no_position: List[String] =
       document_theories.map(_._1)
   }
 
   object Chapter_Defs {
     val empty: Chapter_Defs = new Chapter_Defs(Nil)
   }
 
   class Chapter_Defs private(rev_list: List[Chapter_Def]) {
     def list: List[Chapter_Def] = rev_list.reverse
 
     override def toString: String =
       list.map(_.name).mkString("Chapter_Defs(", ", ", ")")
 
     def get(chapter: String): Option[Chapter_Def] =
       rev_list.find(_.name == chapter)
 
     def apply(chapter: String): Chapter_Def =
       get(chapter) getOrElse Chapter_Def.empty(chapter)
 
     def + (entry: Chapter_Def): Chapter_Defs =
       get(entry.name) match {
         case None => new Chapter_Defs(entry :: rev_list)
         case Some(old_entry) =>
           error("Duplicate chapter definition " + quote(entry.name) +
             Position.here(old_entry.pos) + Position.here(entry.pos))
       }
   }
 
   private object Parsers extends Options.Parsers {
     private val groups: Parser[List[String]] =
       ($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)
 
     private val description: Parser[String] =
       ($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")
 
     private val chapter_def: Parser[Chapter_Def] =
       command(CHAPTER_DEFINITION) ~! (position(chapter_name) ~ groups ~ description) ^^
         { case _ ~ ((a, pos) ~ b ~ c) => Chapter_Def(pos, a, b, c) }
 
     private val chapter_entry: Parser[Chapter_Entry] =
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) }
 
     private val session_entry: Parser[Session_Entry] = {
       val option =
         option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
           { case x ~ y => (x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
       val theory_entry =
         position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) }
 
       val theories =
         $$$(THEORIES) ~!
           ((options | success(Nil)) ~ rep1(theory_entry)) ^^
           { case _ ~ (x ~ y) => (x, y) }
 
       val in_path = $$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x }
 
       val document_theories =
         $$$(DOCUMENT_THEORIES) ~! rep1(position(name)) ^^ { case _ ~ x => x }
 
       val document_files =
         $$$(DOCUMENT_FILES) ~!
           ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
 
       val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0)
 
       val export_files =
         $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^
           { case _ ~ (x ~ y ~ z) => (x, y, z) }
 
       val export_classpath =
         $$$(EXPORT_CLASSPATH) ~! (rep1(embedded) | success(List("*:classpath/*.jar"))) ^^
           { case _ ~ x => x }
 
       command(SESSION) ~!
         (position(session_name) ~ groups ~
           (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
           ($$$("=") ~!
             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ description ~
               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(DIRECTORIES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
               rep(theories) ~
               (opt(document_theories) ^^ (x => x.getOrElse(Nil))) ~
               (rep(document_files) ^^ (x => x.flatten)) ~
               rep(export_files) ~
               opt(export_classpath)))) ^^
         { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l ~ m))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l, m.getOrElse(Nil)) }
     }
 
     def parse_root(path: Path): List[Entry] = {
       val toks = Token.explode(root_syntax.keywords, File.read(path))
       val start = Token.Pos.file(path.implode)
       val parser: Parser[Entry] = chapter_def | chapter_entry | session_entry
       parse_all(rep(parser), Token.reader(toks, start)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
     }
   }
 
   def parse_root(path: Path): List[Entry] = Parsers.parse_root(path)
 
   def parse_root_entries(path: Path): List[Session_Entry] =
     for (entry <- Parsers.parse_root(path) if entry.isInstanceOf[Session_Entry])
     yield entry.asInstanceOf[Session_Entry]
 
   def parse_roots(roots: Path): List[String] = {
     for {
       line <- split_lines(File.read(roots))
       if !(line == "" || line.startsWith("#"))
     } yield line
   }
 
 
   /* load sessions from certain directories */
 
   def is_session_dir(dir: Path): Boolean =
     (dir + ROOT).is_file || (dir + ROOTS).is_file
 
   def check_session_dir(dir: Path): Path =
     if (is_session_dir(dir)) File.pwd() + dir.expand
     else error("Bad session root directory (missing ROOT or ROOTS): " + dir.expand.toString)
 
   def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = {
     val default_dirs = Components.directories().filter(is_session_dir)
     for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }
     yield (select, dir.canonical)
   }
 
   def load_structure(
     options: Options,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     infos: List[Info] = Nil
   ): Structure = {
     def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
       load_root(select, dir) ::: load_roots(select, dir)
 
     def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] = {
       val root = dir + ROOT
       if (root.is_file) List((select, root)) else Nil
     }
 
     def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] = {
       val roots = dir + ROOTS
       if (roots.is_file) {
         for {
           entry <- parse_roots(roots)
           dir1 =
             try { check_session_dir(dir + Path.explode(entry)) }
             catch {
               case ERROR(msg) =>
                 error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
             }
           res <- load_dir(select, dir1)
         } yield res
       }
       else Nil
     }
 
     val raw_roots: List[(Boolean, Path)] =
       for {
         (select, dir) <- directories(dirs, select_dirs)
         res <- load_dir(select, check_session_dir(dir))
       } yield res
 
     val unique_roots: List[(Boolean, Path, List[Entry])] =
       raw_roots.foldLeft(Map.empty[JFile, (Boolean, Path, List[Entry])]) {
         case (m, (select, path)) =>
           val file = path.canonical_file
           m.get(file) match {
             case None =>
               val entries = parse_root(path)
               m + (file -> (select, path.dir, entries))
             case Some((select1, dir1, entries1)) =>
               m + (file -> (select1 || select, dir1, entries1))
           }
       }.valuesIterator.toList
 
     val chapter_defs: Chapter_Defs =
       unique_roots.foldLeft(Chapter_Defs.empty) {
         case (defs1, (_, _, entries)) =>
           entries.foldLeft(defs1) {
             case ((defs2, entry: Chapter_Def)) => defs2 + entry
             case ((defs2, _)) => defs2
           }
       }
 
     val info_roots = {
       var chapter = UNSORTED
       val info_roots = new mutable.ListBuffer[Info]
       for ((select, dir, entries) <- unique_roots) {
         entries.foreach {
           case entry: Chapter_Entry => chapter = entry.name
           case entry: Session_Entry =>
             info_roots += make_info(chapter_defs, options, select, dir, chapter, entry)
           case _ =>
         }
         chapter = UNSORTED
       }
       info_roots.toList
     }
 
     Structure.make(chapter_defs, info_roots ::: infos)
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions",
     Scala_Project.here,
     { args =>
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
       var requirements = false
       var exclude_session_groups: List[String] = Nil
       var all_sessions = false
       var build_graph = false
       var dirs: List[Path] = Nil
       var session_groups: List[String] = Nil
       var exclude_sessions: List[String] = Nil
 
       val getopts = Getopts("""
 Usage: isabelle sessions [OPTIONS] [SESSIONS ...]
 
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -R           refer to requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -b           follow session build dependencies (default: source imports)
     -d DIR       include session directory
     -g NAME      select session group NAME
     -x NAME      exclude session NAME and all descendants
 
   Explore the structure of Isabelle sessions and print result names in
   topological order (on stdout).
 """,
         "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
         "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
         "R" -> (_ => requirements = true),
         "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
         "a" -> (_ => all_sessions = true),
         "b" -> (_ => build_graph = true),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "g:" -> (arg => session_groups = session_groups ::: List(arg)),
         "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
       val sessions = getopts(args)
 
       val options = Options.init()
 
       val selection =
         Selection(requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions,
           exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions,
           session_groups = session_groups, sessions = sessions)
       val sessions_structure =
         load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
 
       val order =
         if (build_graph) sessions_structure.build_topological_order
         else sessions_structure.imports_topological_order
       for (name <- order) Output.writeln(name, stdout = true)
     })
 
 
 
   /** heap file with SHA1 digest **/
 
   private val sha1_prefix = "SHA1:"
 
   def read_heap_digest(heap: Path): Option[String] = {
     if (heap.is_file) {
       using(FileChannel.open(heap.java_path, StandardOpenOption.READ)) { file =>
         val len = file.size
         val n = sha1_prefix.length + SHA1.digest_length
         if (len >= n) {
           file.position(len - n)
 
           val buf = ByteBuffer.allocate(n)
           var i = 0
           var m = 0
           while ({
             m = file.read(buf)
             if (m != -1) i += m
             m != -1 && n > i
           }) ()
 
           if (i == n) {
             val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
             val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
             if (prefix == sha1_prefix) Some(s) else None
           }
           else None
         }
         else None
       }
     }
     else None
   }
 
   def write_heap_digest(heap: Path): String =
     read_heap_digest(heap) match {
       case None =>
         val s = SHA1.digest(heap).toString
         File.append(heap, sha1_prefix + s)
         s
       case Some(s) => s
     }
 
 
 
   /** persistent store **/
 
   object Session_Info {
     val session_name = SQL.Column.string("session_name").make_primary_key
 
     // Build_Log.Session_Info
     val session_timing = SQL.Column.bytes("session_timing")
     val command_timings = SQL.Column.bytes("command_timings")
     val theory_timings = SQL.Column.bytes("theory_timings")
     val ml_statistics = SQL.Column.bytes("ml_statistics")
     val task_statistics = SQL.Column.bytes("task_statistics")
     val errors = SQL.Column.bytes("errors")
     val build_log_columns =
       List(session_name, session_timing, command_timings, theory_timings,
         ml_statistics, task_statistics, errors)
 
     // Build.Session_Info
     val sources = SQL.Column.string("sources")
     val input_heaps = SQL.Column.string("input_heaps")
     val output_heap = SQL.Column.string("output_heap")
     val return_code = SQL.Column.int("return_code")
     val uuid = SQL.Column.string("uuid")
     val build_columns = List(sources, input_heaps, output_heap, return_code, uuid)
 
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
 
     val augment_table: PostgreSQL.Source =
       "ALTER TABLE IF EXISTS " + table.ident +
       " ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql)
   }
 
   def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
     new Store(options, cache)
 
   class Store private[Sessions](val options: Options, val cache: Term.Cache) {
     store =>
 
     override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
 
 
     /* directories */
 
     val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER")
     val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
 
     def system_heaps: Boolean = options.bool("system_heaps")
 
     val output_dir: Path =
       if (system_heaps) system_output_dir else user_output_dir
 
     val input_dirs: List[Path] =
       if (system_heaps) List(system_output_dir)
       else List(user_output_dir, system_output_dir)
 
     def presentation_dir: Path =
       if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
       else Path.explode("$ISABELLE_BROWSER_INFO")
 
 
     /* file names */
 
     def heap(name: String): Path = Path.basic(name)
     def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
     def log(name: String): Path = Path.basic("log") + Path.basic(name)
     def log_gz(name: String): Path = log(name).ext("gz")
 
     def output_heap(name: String): Path = output_dir + heap(name)
     def output_database(name: String): Path = output_dir + database(name)
     def output_log(name: String): Path = output_dir + log(name)
     def output_log_gz(name: String): Path = output_dir + log_gz(name)
 
     def prepare_output_dir(): Unit = Isabelle_System.make_directory(output_dir + Path.basic("log"))
 
 
     /* heap */
 
     def find_heap(name: String): Option[Path] =
       input_dirs.map(_ + heap(name)).find(_.is_file)
 
     def find_heap_digest(name: String): Option[String] =
       find_heap(name).flatMap(read_heap_digest)
 
     def the_heap(name: String): Path =
       find_heap(name) getOrElse
         error("Missing heap image for session " + quote(name) + " -- expected in:\n" +
           cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
 
 
     /* database */
 
     def find_database(name: String): Option[Path] =
       input_dirs.map(_ + database(name)).find(_.is_file)
 
     def database_server: Boolean = options.bool("build_database_server")
 
     def open_database_server(): SQL.Database =
       PostgreSQL.open_database(
         user = options.string("build_database_user"),
         password = options.string("build_database_password"),
         database = options.string("build_database_name"),
         host = options.string("build_database_host"),
         port = options.int("build_database_port"),
         ssh =
           options.proper_string("build_database_ssh_host").map(ssh_host =>
             SSH.open_session(options,
               host = ssh_host,
               user = options.string("build_database_ssh_user"),
               port = options.int("build_database_ssh_port"))),
         ssh_close = true)
 
     def try_open_database(
       name: String,
       output: Boolean = false,
       server: Boolean = database_server
     ): Option[SQL.Database] = {
       def check(db: SQL.Database): Option[SQL.Database] =
         if (output || session_info_exists(db)) Some(db) else { db.close(); None }
 
       if (server) check(open_database_server())
       else if (output) Some(SQLite.open_database(output_database(name)))
       else {
         (for {
           dir <- input_dirs.view
           path = dir + database(name) if path.is_file
           db <- check(SQLite.open_database(path))
         } yield db).headOption
       }
     }
 
     def error_database(name: String): Nothing =
       error("Missing build database for session " + quote(name))
 
     def open_database(name: String, output: Boolean = false): SQL.Database =
       try_open_database(name, output = output) getOrElse error_database(name)
 
     def clean_output(name: String): (Boolean, Boolean) = {
       val relevant_db =
         database_server && {
           try_open_database(name) match {
             case Some(db) =>
               try {
                 db.transaction {
                   val relevant_db = session_info_defined(db, name)
                   init_session_info(db, name)
                   relevant_db
                 }
               } finally { db.close() }
             case None => false
           }
         }
 
       val del =
         for {
           dir <-
             (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir))
           file <- List(heap(name), database(name), log(name), log_gz(name))
           path = dir + file if path.is_file
         } yield path.file.delete
 
       val relevant = relevant_db || del.nonEmpty
       val ok = del.forall(b => b)
       (relevant, ok)
     }
 
 
     /* SQL database content */
 
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
       db.using_statement(Session_Info.table.select(List(column),
         Session_Info.session_name.where_equal(name))) { stmt =>
         val res = stmt.execute_query()
         if (!res.next()) Bytes.empty else res.bytes(column)
       }
 
     def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
       Properties.uncompress(read_bytes(db, name, column), cache = cache)
 
 
     /* session info */
 
     def init_session_info(db: SQL.Database, name: String): Unit = {
       db.transaction {
         db.create_table(Session_Info.table)
         db.using_statement(
           Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute())
         if (db.isInstanceOf[PostgreSQL.Database]) {
           db.using_statement(Session_Info.augment_table)(_.execute())
         }
 
         db.create_table(Export.Data.table)
         db.using_statement(
           Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute())
 
         db.create_table(Document_Build.Data.table)
         db.using_statement(
           Document_Build.Data.table.delete(
             Document_Build.Data.session_name.where_equal(name)))(_.execute())
       }
     }
 
     def session_info_exists(db: SQL.Database): Boolean = {
       val tables = db.tables
       tables.contains(Session_Info.table.name) &&
       tables.contains(Export.Data.table.name)
     }
 
     def session_info_defined(db: SQL.Database, name: String): Boolean =
       session_info_exists(db) && {
         db.using_statement(
           Session_Info.table.select(List(Session_Info.session_name),
             Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
       }
 
     def write_session_info(
       db: SQL.Database,
       name: String,
       build_log: Build_Log.Session_Info,
       build: Build.Session_Info
     ): Unit = {
       db.transaction {
         val table = Session_Info.table
         db.using_statement(table.insert()) { stmt =>
           stmt.string(1) = name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
           stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.compress)
           stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.compress)
           stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.compress)
           stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.compress)
           stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.compress)
           stmt.string(8) = build.sources
           stmt.string(9) = cat_lines(build.input_heaps)
           stmt.string(10) = build.output_heap getOrElse ""
           stmt.int(11) = build.return_code
           stmt.string(12) = build.uuid
           stmt.execute()
         }
       }
     }
 
     def read_session_timing(db: SQL.Database, name: String): Properties.T =
       Properties.decode(read_bytes(db, name, Session_Info.session_timing), cache = cache)
 
     def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.command_timings)
 
     def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.theory_timings)
 
     def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.ml_statistics)
 
     def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.task_statistics)
 
     def read_theories(db: SQL.Database, name: String): List[String] =
       read_theory_timings(db, name).flatMap(Markup.Name.unapply)
 
     def read_errors(db: SQL.Database, name: String): List[String] =
       Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache)
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = {
       if (db.tables.contains(Session_Info.table.name)) {
         db.using_statement(Session_Info.table.select(Nil,
           Session_Info.session_name.where_equal(name))) { stmt =>
           val res = stmt.execute_query()
           if (!res.next()) None
           else {
             val uuid =
               try { Option(res.string(Session_Info.uuid)).getOrElse("") }
               catch { case _: SQLException => "" }
             Some(
               Build.Session_Info(
                 res.string(Session_Info.sources),
                 split_lines(res.string(Session_Info.input_heaps)),
                 res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
                 res.int(Session_Info.return_code),
                 uuid))
           }
         }
       }
       else None
     }
   }
 }
diff --git a/src/Pure/Tools/spell_checker.scala b/src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala
+++ b/src/Pure/Tools/spell_checker.scala
@@ -1,278 +1,280 @@
 /*  Title:      Pure/Tools/spell_checker.scala
     Author:     Makarius
 
 Spell checker with completion, based on JOrtho (see
 https://sourceforge.net/projects/jortho).
 */
 
 package isabelle
 
 
 import java.lang.Class
 import java.util.{List => JList}
 
 import scala.collection.mutable
 import scala.annotation.tailrec
 import scala.collection.immutable.SortedMap
 
 
 object Spell_Checker {
   /* words within text */
 
   def marked_words(
     base: Text.Offset,
     text: String,
     mark: Text.Info[String] => Boolean
   ) : List[Text.Info[String]] = {
     val result = new mutable.ListBuffer[Text.Info[String]]
     var offset = 0
 
     def apostrophe(c: Int): Boolean =
       c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
 
     @tailrec def scan(pred: Int => Boolean): Unit = {
       if (offset < text.length) {
         val c = text.codePointAt(offset)
         if (pred(c)) {
           offset += Character.charCount(c)
           scan(pred)
         }
       }
     }
 
     while (offset < text.length) {
       scan(c => !Character.isLetter(c))
       val start = offset
       scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
       val stop = offset
       if (stop - start >= 2) {
         val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop))
         if (mark(info)) result += info
       }
     }
     result.toList
   }
 
   def current_word(rendering: Rendering, range: Text.Range): Option[Text.Info[String]] = {
     for {
       spell_range <- rendering.spell_checker_point(range)
       text <- rendering.get_text(spell_range)
       info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
     } yield info
   }
 
 
   /* dictionaries */
 
   class Dictionary private[Spell_Checker](val path: Path) {
     val lang: String = path.drop_ext.file_name
     val user_path: Path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
     override def toString: String = lang
   }
 
   private object Decl {
     def apply(name: String, include: Boolean): String =
       if (include) name else "-" + name
 
     def unapply(decl: String): Option[(String, Boolean)] = {
       val decl1 = decl.trim
       if (decl1 == "" || decl1.startsWith("#")) None
       else
         Library.try_unprefix("-", decl1.trim) match {
           case None => Some((decl1, true))
           case Some(decl2) => Some((decl2, false))
         }
     }
   }
 
-  def dictionaries: List[Dictionary] =
+  lazy val dictionaries: List[Dictionary] =
     for {
       path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
       if path.is_file
     } yield new Dictionary(path)
 
+  def get_dictionary(lang: String): Option[Dictionary] = dictionaries.find(_.lang == lang)
+
 
   /* create spell checker */
 
   def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
 
   private sealed case class Update(include: Boolean, permanent: Boolean)
 }
 
 
 class Spell_Checker private(dictionary: Spell_Checker.Dictionary) {
   override def toString: String = dictionary.toString
 
 
   /* main dictionary content */
 
   private var dict = new Object
   private var updates = SortedMap.empty[String, Spell_Checker.Update]
 
   private def included_iterator(): Iterator[String] =
     for {
       (word, upd) <- updates.iterator
       if upd.include
     } yield word
 
   private def excluded(word: String): Boolean =
     updates.get(word) match {
       case Some(upd) => !upd.include
       case None => false
     }
 
   private def load(): Unit = {
     val main_dictionary = split_lines(File.read_gzip(dictionary.path))
 
     val permanent_updates =
       if (dictionary.user_path.is_file)
         for {
           Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
         } yield (word, Spell_Checker.Update(include, true))
       else Nil
 
     updates =
       updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
         permanent_updates
 
     val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
     val factory = Untyped.constructor(factory_class).newInstance()
 
     val add = Untyped.method(factory_class, "add", classOf[String])
 
     for {
       word <- main_dictionary.iterator ++ included_iterator()
       if !excluded(word)
     } add.invoke(factory, word)
 
     dict = Untyped.method(factory_class, "create").invoke(factory)
   }
   load()
 
   private def save(): Unit = {
     val permanent_decls =
       (for {
         (word, upd) <- updates.iterator
         if upd.permanent
       } yield Spell_Checker.Decl(word, upd.include)).toList
 
     if (permanent_decls.nonEmpty || dictionary.user_path.is_file) {
       val header = """# User updates for spell-checker dictionary
 #
 #   * each line contains at most one word
 #   * extra blanks are ignored
 #   * lines starting with "#" are stripped
 #   * lines starting with "-" indicate excluded words
 #
 #:mode=text:encoding=UTF-8:
 
 """
       Isabelle_System.make_directory(dictionary.user_path.expand.dir)
       File.write(dictionary.user_path, header + cat_lines(permanent_decls))
     }
   }
 
   def update(word: String, include: Boolean, permanent: Boolean): Unit = {
     updates += (word -> Spell_Checker.Update(include, permanent))
 
     if (include) {
       if (permanent) save()
       Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
     }
     else { save(); load() }
   }
 
   def reset(): Unit = {
     updates = SortedMap.empty
     load()
   }
 
   def reset_enabled(): Int =
     updates.valuesIterator.count(upd => !upd.permanent)
 
 
   /* check known words */
 
   def contains(word: String): Boolean =
     Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]).
       invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
 
   def check(word: String): Boolean =
     word match {
       case Word.Case(c) if c != Word.Lowercase =>
         contains(word) || contains(Word.lowercase(word))
       case _ =>
         contains(word)
     }
 
   def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] =
     Spell_Checker.marked_words(base, text, info => !check(info.info))
 
 
   /* completion: suggestions for unknown words */
 
   private def suggestions(word: String): Option[List[String]] = {
     val res =
       Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
         invoke(dict, word).asInstanceOf[JList[AnyRef]].toArray.toList.map(_.toString)
     if (res.isEmpty) None else Some(res)
   }
 
   def complete(word: String): List[String] =
     if (check(word)) Nil
     else {
       val word_case = Word.Case.unapply(word)
       def recover_case(s: String) =
         word_case match {
           case Some(c) => Word.Case(c, s)
           case None => s
         }
       val result =
         word_case match {
           case Some(c) if c != Word.Lowercase =>
             suggestions(word) orElse suggestions(Word.lowercase(word))
           case _ =>
             suggestions(word)
         }
       result.getOrElse(Nil).map(recover_case)
     }
 
   def completion(rendering: Rendering, caret: Text.Offset): Option[Completion.Result] = {
     val caret_range = rendering.before_caret_range(caret)
     for {
       word <- Spell_Checker.current_word(rendering, caret_range)
       words = complete(word.info)
       if words.nonEmpty
       descr = "(from dictionary " + quote(dictionary.toString) + ")"
       items =
         words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
     } yield Completion.Result(word.range, word.info, false, items)
   }
 }
 
 class Spell_Checker_Variable {
   private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None)
   private var current_spell_checker = no_spell_checker
 
   def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 }
 
   def update(options: Options): Unit = synchronized {
     if (options.bool("spell_checker")) {
       val lang = options.string("spell_checker_dictionary")
       if (current_spell_checker._1 != lang) {
-        Spell_Checker.dictionaries.find(_.lang == lang) match {
+        Spell_Checker.get_dictionary(lang) match {
           case Some(dictionary) =>
             val spell_checker =
               Exn.capture { Spell_Checker(dictionary) } match {
                 case Exn.Res(spell_checker) => Some(spell_checker)
                 case Exn.Exn(_) => None
               }
             current_spell_checker = (lang, spell_checker)
           case None =>
             current_spell_checker = no_spell_checker
         }
       }
     }
     else current_spell_checker = no_spell_checker
   }
 }
diff --git a/src/Tools/jEdit/src/document_dockable.scala b/src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala
+++ b/src/Tools/jEdit/src/document_dockable.scala
@@ -1,271 +1,278 @@
 /*  Title:      Tools/jEdit/src/document_dockable.scala
     Author:     Makarius
 
 Dockable window for document build support.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter}
 
 import scala.swing.{ScrollPane, TextArea, Label, TabbedPane, BorderPanel, Component}
 
 import org.gjt.sp.jedit.{jEdit, View}
 
 
 object Document_Dockable {
   /* document output */
 
   def document_name: String = "document"
   def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output")
   def document_output(): Path = document_output_dir() + Path.basic(document_name)
 
   def view_document(): Unit = {
     val path = Document_Dockable.document_output().pdf
     if (path.is_file) Isabelle_System.pdf_viewer(path)
   }
 
   class Log_Progress extends Progress {
     def show(text: String): Unit = {}
 
     private val syslog = PIDE.session.make_syslog()
 
     private def update(text: String = syslog.content()): Unit = GUI_Thread.require { show(text) }
     private val delay =
       Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { update() }
 
     override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
     override def theory(theory: Progress.Theory): Unit = echo(theory.message)
 
     def load(): Unit = {
       val path = document_output().log
       val text = if (path.is_file) File.read(path) else ""
       GUI_Thread.later { delay.revoke(); update(text) }
     }
 
     update()
   }
 
 
   /* state */
 
   object Status extends Enumeration {
     val WAITING = Value("waiting")
     val RUNNING = Value("running")
     val FINISHED = Value("finished")
   }
 
   sealed case class Result(output: List[XML.Tree] = Nil) {
     def failed: Boolean = output.exists(Protocol.is_error)
   }
 
   object State {
     def empty(): State = State()
     def finish(result: Result): State = State(output = result.output)
   }
 
   sealed case class State(
     progress: Log_Progress = new Log_Progress,
     process: Future[Unit] = Future.value(()),
     output: List[XML.Tree] = Nil,
     status: Status.Value = Status.FINISHED)
 }
 
 class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
   GUI_Thread.require {}
 
 
   /* component state -- owned by GUI thread */
 
   private val current_state = Synchronized(Document_Dockable.State.empty())
 
   private val process_indicator = new Process_Indicator
   private val pretty_text_area = new Pretty_Text_Area(view)
   private val message_pane = new TabbedPane
 
   private def show_state(): Unit = GUI_Thread.later {
     val st = current_state.value
 
     pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output)
 
     st.status match {
       case Document_Dockable.Status.WAITING =>
         process_indicator.update("Waiting for PIDE document content ...", 5)
       case Document_Dockable.Status.RUNNING =>
         process_indicator.update("Running document build process ...", 15)
       case Document_Dockable.Status.FINISHED =>
         process_indicator.update(null, 0)
     }
   }
 
   private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later {
     message_pane.selection.page = page
   }
 
 
   /* text area with zoom/resize */
 
   override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
   private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
   private def handle_resize(): Unit = GUI_Thread.require { pretty_text_area.zoom(zoom) }
 
   private val delay_resize: Delay =
     Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
     override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })
 
 
   /* progress log */
 
   private val log_area =
     new TextArea {
       editable = false
       font = GUI.copy_font((new Label).font)
     }
   private val scroll_log_area = new ScrollPane(log_area)
 
   def init_progress(): Document_Dockable.Log_Progress =
     new Document_Dockable.Log_Progress {
       override def show(text: String): Unit =
         if (text != log_area.text) {
           log_area.text = text
           val vertical = scroll_log_area.peer.getVerticalScrollBar
           vertical.setValue(vertical.getMaximum)
         }
     }
 
 
   /* document build process */
 
   private def cancel(): Unit =
     current_state.change { st => st.process.cancel(); st }
 
   private def init_state(): Unit =
     current_state.change { _ => Document_Dockable.State(progress = init_progress()) }
 
   private def build_document(): Unit = {
     current_state.change { st =>
       if (st.process.is_finished) {
         val progress = init_progress()
         val process =
           Future.thread[Unit](name = "document_build") {
             show_page(log_page)
             val res =
               Exn.capture {
                 progress.echo("Start " + Date.now())
                 for (i <- 1 to 200) {
                   progress.echo("message " + i)
                   Time.seconds(0.1).sleep()
                 }
                 progress.echo("Stop " + Date.now())
               }
             val msg =
               res match {
                 case Exn.Res(_) => Protocol.make_message(XML.string("OK"))
                 case Exn.Exn(exn) => Protocol.error_message(XML.string(Exn.message(exn)))
               }
             val result = Document_Dockable.Result(output = List(msg))
             current_state.change(_ => Document_Dockable.State.finish(result))
             show_state()
             show_page(output_page)
           }
         st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING)
       }
       else st
     }
     show_state()
   }
 
 
   /* controls */
 
-  private val document_session: GUI.Selector[String] =
-    new GUI.Selector(JEdit_Sessions.sessions_structure().build_topological_order.sorted) {
+  private val document_session: GUI.Selector[String] = {
+    val sessions = JEdit_Sessions.sessions_structure()
+    val all_sessions = sessions.build_topological_order.sorted
+    val doc_sessions = all_sessions.filter(name => sessions(name).doc_group)
+    new GUI.Selector(
+      doc_sessions.map(GUI.Selector.item) ::: List(GUI.Selector.separator) :::
+      all_sessions.map(GUI.Selector.item)
+    ) {
       val title = "Session"
     }
+  }
 
   private val build_button =
     new GUI.Button("<html><b>Build</b></html>") {
       tooltip = "Build document"
       override def clicked(): Unit = build_document()
     }
 
   private val cancel_button =
     new GUI.Button("Cancel") {
       tooltip = "Cancel build process"
       override def clicked(): Unit = cancel()
     }
 
   private val view_button =
     new GUI.Button("View") {
       tooltip = "View document"
       override def clicked(): Unit = Document_Dockable.view_document()
     }
 
   private val controls =
     Wrap_Panel(List(document_session, process_indicator.component, build_button,
       view_button, cancel_button))
 
   add(controls.peer, BorderLayout.NORTH)
 
   override def focusOnDefaultComponent(): Unit = build_button.requestFocus()
 
 
   /* message pane with pages */
 
   private val output_controls =
     Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
 
   private val output_page =
     new TabbedPane.Page("Output", new BorderPanel {
       layout(output_controls) = BorderPanel.Position.North
       layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
     }, "Output from build process")
 
   private val load_button =
     new GUI.Button("Load") {
       tooltip = "Load final log file"
       override def clicked(): Unit = current_state.value.progress.load()
     }
 
   private val log_controls =
     Wrap_Panel(List(load_button))
 
   private val log_page =
     new TabbedPane.Page("Log", new BorderPanel {
       layout(log_controls) = BorderPanel.Position.North
       layout(scroll_log_area) = BorderPanel.Position.Center
     }, "Raw log of build process")
 
   message_pane.pages ++= List(log_page, output_page)
 
   set_content(message_pane)
 
 
   /* main */
 
   private val main =
     Session.Consumer[Session.Global_Options](getClass.getName) {
       case _: Session.Global_Options =>
         GUI_Thread.later { handle_resize() }
     }
 
   override def init(): Unit = {
     init_state()
     PIDE.session.global_options += main
     handle_resize()
   }
 
   override def exit(): Unit = {
     PIDE.session.global_options -= main
     delay_resize.revoke()
   }
 }
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,143 +1,143 @@
 /*  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._
 
 
 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 = PIDE.options.value,
     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 = 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 sealed case class Logic_Entry(name: String = "", description: String = "") {
-    override def toString: String = proper_string(description) getOrElse name
-  }
-
   def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
-    val default_entry = Logic_Entry(description = "default (" + logic_name(options.value) + ")")
+    val default_entry =
+      GUI.Selector.Item("", description = "default (" + logic_name(options.value) + ")")
 
     val session_entries = {
       val sessions = sessions_structure(options = options.value)
-      val (main_sessions, other_sessions) =
-        sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main"))
-      (main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name))
+      val all_sessions = sessions.imports_topological_order
+      val main_sessions = all_sessions.filter(name => sessions(name).main_group)
+
+      main_sessions.map(GUI.Selector.item) ::: List(GUI.Selector.separator) :::
+      all_sessions.map(GUI.Selector.item)
     }
 
-    new GUI.Selector[Logic_Entry](default_entry :: session_entries)
-    with JEdit_Options.Entry {
+    new GUI.Selector(default_entry :: session_entries) with JEdit_Options.Entry {
       name = jedit_logic_option
       tooltip = "Logic session name (change requires restart)"
       val title = "Logic"
       def load(): Unit = {
         val logic = options.string(jedit_logic_option)
-        entries.find(_.name == logic) match {
+        entries.find { case GUI.Selector.Item(item, _) => item == logic case _ => false } match {
           case Some(entry) => selection.item = entry
           case None =>
         }
       }
-      def save(): Unit = options.string(jedit_logic_option) = selection.item.name
+      def save(): Unit =
+        for (item <- selection.item.get_item) options.string(jedit_logic_option) = item
+
       override def changed(): Unit = if (autosave) save()
 
       load()
     }
   }
 
 
   /* 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_base.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): Unit = {
     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.start(session, options, sessions_structure, store,
       logic = PIDE.resources.session_base.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,104 +1,105 @@
 /*  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 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(): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val option_name = "spell_checker_dictionary"
     val opt = PIDE.options.value.check_name(option_name)
 
-    new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with JEdit_Options.Entry {
+    new GUI.Selector(Spell_Checker.dictionaries.map(GUI.Selector.Item(_))) with JEdit_Options.Entry {
       name = option_name
       tooltip = GUI.tooltip_lines(opt.print_default)
       val title = opt.title()
       def load(): Unit = {
         val lang = PIDE.options.string(option_name)
-        entries.find(_.lang == lang) match {
-          case Some(entry) => selection.item = entry
+        Spell_Checker.get_dictionary(lang) match {
+          case Some(dict) => selection.item = GUI.Selector.Item(dict)
           case None =>
         }
       }
-      def save(): Unit = PIDE.options.string(option_name) = selection.item.lang
+      def save(): Unit =
+        for (item <- selection.item.get_item) PIDE.options.string(option_name) = item.lang
 
       load()
     }
   }
 }
diff --git a/src/Tools/jEdit/src/monitor_dockable.scala b/src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala
+++ b/src/Tools/jEdit/src/monitor_dockable.scala
@@ -1,122 +1,123 @@
 /*  Title:      Tools/jEdit/src/monitor_dockable.scala
     Author:     Makarius
 
 Monitor for runtime statistics.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.BorderLayout
 
 import scala.collection.immutable.Queue
 import scala.swing.TextField
 import scala.swing.event.ValueChanged
 
 import org.jfree.chart.ChartPanel
 import org.jfree.data.xy.XYSeriesCollection
 
 import org.gjt.sp.jedit.View
 
 
 class Monitor_Dockable(view: View, position: String) extends Dockable(view, position) {
   /* chart data -- owned by GUI thread */
 
   private var statistics = Queue.empty[Properties.T]
   private var statistics_length = 0
 
   private def add_statistics(stats: Properties.T): Unit = {
     statistics = statistics.appended(stats)
     statistics_length += 1
     limit_data.text match {
       case Value.Int(limit) =>
         while (statistics_length > limit) {
           statistics = statistics.dequeue._2
           statistics_length -= 1
         }
       case _ =>
     }
   }
   private def clear_statistics(): Unit = {
     statistics = Queue.empty
     statistics_length = 0
   }
 
   private var data_name = ML_Statistics.all_fields.head._1
   private val chart = ML_Statistics.empty.chart(null, Nil)
   private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
 
   private def update_chart(): Unit = {
     ML_Statistics.all_fields.find(_._1 == data_name) match {
       case None =>
       case Some((_, fields)) => ML_Statistics(statistics.toList).update_data(data, fields)
     }
   }
 
   private val input_delay =
     Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart() }
 
   private val update_delay =
     Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart() }
 
 
   /* controls */
 
-  private val select_data = new GUI.Selector[String](ML_Statistics.all_fields.map(_._1)) {
-    tooltip = "Select visualized data collection"
-    override def changed(): Unit = { data_name = selection.item; update_chart() }
-  }
+  private val select_data =
+    new GUI.Selector(ML_Statistics.all_fields.map { case (a, _) => GUI.Selector.item(a) }) {
+      tooltip = "Select visualized data collection"
+      override def changed(): Unit = { data_name = selection.item.toString; update_chart() }
+    }
 
   private val limit_data = new TextField("200", 5) {
     tooltip = "Limit for accumulated data"
     verifier = {
       case Value.Int(x) => x > 0
       case _ => false
     }
     reactions += { case ValueChanged(_) => input_delay.invoke() }
   }
 
   private val reset_data = new GUI.Button("Reset") {
     tooltip = "Reset accumulated data"
     override def clicked(): Unit = { clear_statistics(); update_chart() }
   }
 
   private val full_gc = new GUI.Button("GC") {
     tooltip = "Full garbage collection of ML heap"
     override def clicked(): Unit = PIDE.session.protocol_command("ML_Heap.full_gc")
   }
 
   private val share_common_data = new GUI.Button("Sharing") {
     tooltip = "Share common data of ML heap"
     override def clicked(): Unit = PIDE.session.protocol_command("ML_Heap.share_common_data")
   }
 
   private val controls =
     Wrap_Panel(List(select_data, limit_data, reset_data, full_gc, share_common_data))
 
 
   /* layout */
 
   set_content(new ChartPanel(chart))
   add(controls.peer, BorderLayout.NORTH)
 
 
   /* main */
 
   private val main =
     Session.Consumer[Session.Runtime_Statistics](getClass.getName) {
       stats =>
         add_statistics(stats.props)
         update_delay.invoke()
     }
 
   override def init(): Unit = {
     PIDE.session.runtime_statistics += main
   }
 
   override def exit(): Unit = {
     PIDE.session.runtime_statistics -= main
   }
 }