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,413 +1,443 @@
 /*  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.event.{KeyAdapter, KeyEvent, ItemListener, ItemEvent}
 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}
+  JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities}
 
 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() }
   }
 
 
   /* list selector */
 
   object Selector {
     sealed abstract class Entry[A] {
       def get_item: Option[A] =
         this match {
-          case Item(item, _) => Some(item)
+          case item: Item[_] => Some(item.item)
           case _ => None
         }
     }
-    case class Item[A](item: A, description: String = "") extends Entry[A] {
+    case class Item[A](item: A, description: String = "", batch: Int = 0) extends Entry[A] {
       override def toString: String = proper_string(description) getOrElse item.toString
     }
-    case class Separator[A](name: String = "") extends Entry[A] {
+    case class Separator[A](name: String = "", batch: Int = 0) extends Entry[A] {
       override def toString: String = "<b>" + name + "</b>"
     }
 
-    def item(name: String): Item[String] = Item(name)
-    def separator: Separator[String] = Separator()
+    def item(name: String, batch: Int = 0): Item[String] = Item(name, batch = batch)
+    def separator(batch: Int = 0): Separator[String] = Separator(batch = batch)
   }
 
   class Selector[A](val entries: List[Selector.Entry[A]])
   extends ComboBox[Selector.Entry[A]](entries) {
     def changed(): Unit = {}
 
+    override lazy val peer: JComboBox[Selector.Entry[A]] =
+      new JComboBox[Selector.Entry[A]](ComboBox.newConstantModel(entries)) with SuperMixin {
+        private var key_released = false
+        private var sep_selected = false
+
+        addKeyListener(new KeyAdapter {
+          override def keyPressed(e: KeyEvent): Unit = { key_released = false }
+          override def keyReleased(e: KeyEvent): Unit = { key_released = true }
+        })
+
+        override def setSelectedIndex(i: Int): Unit = {
+          getItemAt(i) match {
+            case _: Selector.Separator[_] =>
+              if (key_released) { sep_selected = true }
+              else {
+                val k = getSelectedIndex()
+                val j = if (i > k) i + 1 else i - 1
+                if (0 <= j && j < dataModel.getSize()) super.setSelectedIndex(j)
+              }
+            case _ => super.setSelectedIndex(i)
+          }
+        }
+
+        override def setPopupVisible(visible: Boolean): Unit = {
+          if (sep_selected) { sep_selected = false}
+          else super.setPopupVisible(visible)
+        }
+      }
+
     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)
+      .map(GUI.Selector.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 => 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/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,278 +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] = {
     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)
+      doc_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) :::
+      all_sessions.map(GUI.Selector.item(_, batch = 1))
     ) {
       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,146 @@
 /*  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 */
 
   def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val default_entry =
       GUI.Selector.Item("", description = "default (" + logic_name(options.value) + ")")
 
     val session_entries = {
       val sessions = sessions_structure(options = options.value)
       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.sorted.map(GUI.Selector.item)
+      main_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) :::
+      all_sessions.sorted.map(GUI.Selector.item(_, batch = 1))
     }
 
     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 { case GUI.Selector.Item(item, _) => item == logic case _ => false } match {
+        entries.find {
+          case item: GUI.Selector.Item[_] => item.item == logic
+          case _ => false
+        } match {
           case Some(entry) => selection.item = entry
           case None =>
         }
       }
       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)
   }
 }