--- 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...
--- 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
--- 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)
}
-