# HG changeset patch
# User wenzelm
# Date 1668019341 -3600
# Node ID e228be7cd3751c4b1d8445b0b26854861a20fa38
# Parent  2c37c10d6884f8c1a62ffb2d43bea834dca83add
clarified GUI.Selector, with support for separator as pseudo-entry;
clarified signature;

diff -r 2c37c10d6884 -r e228be7cd375 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Wed Nov 09 14:20:52 2022 +0100
+++ b/src/Pure/GUI/gui.scala	Wed Nov 09 19:42:21 2022 +0100
@@ -13,7 +13,9 @@
 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}
 
 
@@ -127,9 +129,45 @@
     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() }
   }
@@ -141,8 +179,9 @@
 
   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 {
@@ -161,7 +200,8 @@
       }
     }
 
-    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 _ =>
diff -r 2c37c10d6884 -r e228be7cd375 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Nov 09 14:20:52 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 09 19:42:21 2022 +0100
@@ -507,6 +507,9 @@
 
     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)
 
diff -r 2c37c10d6884 -r e228be7cd375 src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Wed Nov 09 14:20:52 2022 +0100
+++ b/src/Pure/Tools/spell_checker.scala	Wed Nov 09 19:42:21 2022 +0100
@@ -85,12 +85,14 @@
     }
   }
 
-  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 */
 
@@ -260,7 +262,7 @@
     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 {
diff -r 2c37c10d6884 -r e228be7cd375 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 09 14:20:52 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 09 19:42:21 2022 +0100
@@ -187,10 +187,17 @@
 
   /* 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>") {
diff -r 2c37c10d6884 -r e228be7cd375 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 09 14:20:52 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 09 19:42:21 2022 +0100
@@ -69,35 +69,35 @@
 
   /* 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()
diff -r 2c37c10d6884 -r e228be7cd375 src/Tools/jEdit/src/jedit_spell_checker.scala
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Wed Nov 09 14:20:52 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Wed Nov 09 19:42:21 2022 +0100
@@ -85,18 +85,19 @@
     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 -r 2c37c10d6884 -r e228be7cd375 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Wed Nov 09 14:20:52 2022 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Wed Nov 09 19:42:21 2022 +0100
@@ -64,10 +64,11 @@
 
   /* 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"