# HG changeset patch
# User wenzelm
# Date 1660398072 -7200
# Node ID 7d27944d7141a00d07d7c1b8d901732d4f7bf614
# Parent  d750ead045a1461dfb6f3487db19f5ed69abe6de
clarified signature: avoid public representation;

diff -r d750ead045a1 -r 7d27944d7141 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Sat Aug 13 15:09:10 2022 +0200
+++ b/src/Pure/System/components.scala	Sat Aug 13 15:41:12 2022 +0200
@@ -318,7 +318,7 @@
         var options = Options.init()
 
         def show_options: String =
-          cat_lines(relevant_options.map(name => options.options(name).print))
+          cat_lines(relevant_options.flatMap(options.get).map(_.print))
 
         val getopts = Getopts("""
 Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS...
diff -r d750ead045a1 -r 7d27944d7141 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Aug 13 15:09:10 2022 +0200
+++ b/src/Pure/System/options.scala	Sat Aug 13 15:41:12 2022 +0200
@@ -213,23 +213,27 @@
 
 
 final class Options private(
-  val options: Map[String, Options.Opt] = Map.empty,
+  options: Map[String, Options.Opt] = Map.empty,
   val section: String = ""
 ) {
-  override def toString: String = options.iterator.mkString("Options(", ",", ")")
+  def opt_iterator: Iterator[(String, Options.Opt)] = options.iterator
+
+  override def toString: String = opt_iterator.mkString("Options(", ",", ")")
 
   private def print_opt(opt: Options.Opt): String =
     if (opt.public) "public " + opt.print else opt.print
 
-  def print: String = cat_lines(options.toList.sortBy(_._1).map(p => print_opt(p._2)))
+  def print: String = cat_lines(opt_iterator.toList.sortBy(_._1).map(p => print_opt(p._2)))
 
   def description(name: String): String = check_name(name).description
 
 
   /* check */
 
+  def get(name: String): Option[Options.Opt] = options.get(name)
+
   def check_name(name: String): Options.Opt =
-    options.get(name) match {
+    get(name) match {
       case Some(opt) if !opt.unknown => opt
       case _ => error("Unknown option " + quote(name))
     }
@@ -316,7 +320,7 @@
     standard: Option[Option[String]],
     description: String
   ): Options = {
-    options.get(name) match {
+    get(name) match {
       case Some(other) =>
         error("Duplicate declaration of option " + quote(name) + Position.here(pos) +
           Position.here(other.pos))
@@ -405,7 +409,7 @@
     val changed =
       (for {
         (name, opt2) <- options.iterator
-        opt1 = defaults.options.get(name)
+        opt1 = defaults.get(name)
         if opt1.isEmpty || opt1.get.value != opt2.value
       } yield (name, opt2.value, if (opt1.isEmpty) "  (* unknown *)" else "")).toList
 
diff -r d750ead045a1 -r 7d27944d7141 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Sat Aug 13 15:09:10 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Sat Aug 13 15:41:12 2022 +0200
@@ -43,19 +43,18 @@
 
   protected val components =
     options.make_components(predefined,
-      (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
+      (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
 }
 
 
 class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering") {
   private val predefined =
     (for {
-      (name, opt) <- PIDE.options.value.options.toList
+      (name, opt) <- PIDE.options.value.opt_iterator
       if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
-    } yield PIDE.options.make_color_component(opt))
+    } yield PIDE.options.make_color_component(opt)).toList
 
   assert(predefined.nonEmpty)
 
   protected val components = PIDE.options.make_components(predefined, _ => false)
 }
-