# HG changeset patch
# User wenzelm
# Date 1678530242 -3600
# Node ID bc1248c5d15982b1711a672fd5d672aac7586816
# Parent  b4ef44ce08edc72e0780b67062306c34b2a593ee
clarified signature;

diff -r b4ef44ce08ed -r bc1248c5d159 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Mar 11 11:14:24 2023 +0100
+++ b/src/Pure/System/options.scala	Sat Mar 11 11:24:02 2023 +0100
@@ -49,7 +49,7 @@
   val TAG_UPDATE = "update"
   val TAG_CONNECTION = "connection"
 
-  case class Opt(
+  case class Entry(
     public: Boolean,
     pos: Position.T,
     name: String,
@@ -234,32 +234,32 @@
 
 
 final class Options private(
-  options: Map[String, Options.Opt] = Map.empty,
+  options: Map[String, Options.Entry] = Map.empty,
   val section: String = ""
 ) {
-  def opt_iterator: Iterator[(String, Options.Opt)] = options.iterator
+  def iterator: Iterator[Options.Entry] = options.valuesIterator
 
-  override def toString: String = opt_iterator.mkString("Options(", ",", ")")
+  override def toString: String = iterator.mkString("Options(", ",", ")")
 
-  private def print_opt(opt: Options.Opt): String =
+  private def print_entry(opt: Options.Entry): String =
     if (opt.public) "public " + opt.print else opt.print
 
-  def print: String = cat_lines(opt_iterator.toList.sortBy(_._1).map(p => print_opt(p._2)))
+  def print: String = cat_lines(iterator.toList.sortBy(_.name).map(print_entry))
 
   def description(name: String): String = check_name(name).description
 
 
   /* check */
 
-  def get(name: String): Option[Options.Opt] = options.get(name)
+  def get(name: String): Option[Options.Entry] = options.get(name)
 
-  def check_name(name: String): Options.Opt =
+  def check_name(name: String): Options.Entry =
     get(name) match {
       case Some(opt) if !opt.unknown => opt
       case _ => error("Unknown option " + quote(name))
     }
 
-  private def check_type(name: String, typ: Options.Type): Options.Opt = {
+  private def check_type(name: String, typ: Options.Type): Options.Entry = {
     val opt = check_name(name)
     if (opt.typ == typ) opt
     else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print)
@@ -363,7 +363,7 @@
             case Some(s) => Some(s.getOrElse(value))
           }
         val opt =
-          Options.Opt(
+          Options.Entry(
             public, pos, name, typ, value, value, standard_value, tags, description, section)
         (new Options(options + (name -> opt), section)).check_value(name)
     }
@@ -373,7 +373,7 @@
     if (options.isDefinedAt(name)) this + (name, value)
     else {
       val opt =
-        Options.Opt(false, Position.none, name, Options.Unknown, value, value, None, Nil, "", "")
+        Options.Entry(false, Position.none, name, Options.Unknown, value, value, None, Nil, "", "")
       new Options(options + (name -> opt), section)
     }
   }
@@ -407,7 +407,7 @@
   def set_section(new_section: String): Options =
     new Options(options, new_section)
 
-  def sections: List[(String, List[Options.Opt])] =
+  def sections: List[(String, List[Options.Entry])] =
     options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) })
 
 
@@ -437,7 +437,7 @@
 
   def make_prefs(
     defaults: Options = Options.init(prefs = ""),
-    filter: Options.Opt => Boolean = _ => true
+    filter: Options.Entry => Boolean = _ => true
   ): String = {
     (for {
       (name, opt2) <- options.iterator
diff -r b4ef44ce08ed -r bc1248c5d159 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Sat Mar 11 11:14:24 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat Mar 11 11:24:02 2023 +0100
@@ -115,14 +115,14 @@
 
     protected val components: List[(String, List[Entry])] =
       options.make_components(predefined,
-        (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
+        (for (opt <- options.value.iterator if opt.public) yield opt.name).toSet)
   }
 
   class Isabelle_Rendering_Options extends Isabelle_Options("isabelle-rendering") {
     private val predefined =
       (for {
-        (name, opt) <- PIDE.options.value.opt_iterator
-        if name.endsWith("_color") && opt.section == "Rendering of Document Content"
+        opt <- PIDE.options.value.iterator
+        if opt.name.endsWith("_color") && opt.section == "Rendering of Document Content"
       } yield PIDE.options.make_color_component(opt)).toList
 
     assert(predefined.nonEmpty)
@@ -135,7 +135,7 @@
 class JEdit_Options(init_options: Options) extends Options_Variable(init_options) {
   def color_value(s: String): Color = Color_Value(string(s))
 
-  def make_color_component(opt: Options.Opt): JEdit_Options.Entry = {
+  def make_color_component(opt: Options.Entry): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val opt_name = opt.name
@@ -154,7 +154,7 @@
     component
   }
 
-  def make_component(opt: Options.Opt): JEdit_Options.Entry = {
+  def make_component(opt: Options.Entry): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val opt_name = opt.name
@@ -202,7 +202,7 @@
     predefined: List[JEdit_Options.Entry],
     filter: String => Boolean
   ) : List[(String, List[JEdit_Options.Entry])] = {
-    def mk_component(opt: Options.Opt): List[JEdit_Options.Entry] =
+    def mk_component(opt: Options.Entry): List[JEdit_Options.Entry] =
       predefined.find(opt.name == _.name) match {
         case Some(c) => List(c)
         case None => if (filter(opt.name)) List(make_component(opt)) else Nil