# HG changeset patch # User wenzelm # Date 1678701746 -3600 # Node ID f458547b4f0fda819726df15e3d1a79fafcd3b28 # Parent 25993910f21214de1063379ade51d6e975d38f8c clarified signature (again, see also 8c64e51d9dde and 268bf61631ec); diff -r 25993910f212 -r f458547b4f0f src/Pure/System/options.scala --- a/src/Pure/System/options.scala Mon Mar 13 10:51:10 2023 +0100 +++ b/src/Pure/System/options.scala Mon Mar 13 11:02:26 2023 +0100 @@ -177,7 +177,7 @@ def read_prefs(file: Path = PREFS): String = if (file.is_file) File.read(file) else "" - def init(prefs: String = read_prefs(PREFS), opts: List[String] = Nil): Options = { + def init(prefs: String = read_prefs(file = PREFS), opts: List[String] = Nil): Options = { var options = empty for { dir <- Components.directories() @@ -438,20 +438,34 @@ } + /* changed options */ + + sealed case class Changed(name: String, value: String, unknown: Boolean) { + def print_props: String = Properties.Eq(name, value) + def print_prefs: String = + name + " = " + Outer_Syntax.quote_string(value) + + if_proper(unknown, " (* unknown *)") + "\n" + } + + def changed( + defaults: Options = Options.init0(), + filter: Options.Entry => Boolean = _ => true + ): List[Changed] = { + List.from( + for { + (name, opt2) <- options.iterator + opt1 = defaults.get(name) + if (opt1.isEmpty || opt1.get.value != opt2.value) && filter(opt2) + } yield Changed(name, opt2.value, opt1.isEmpty)) + } + + /* preferences */ def make_prefs( defaults: Options = Options.init0(), filter: Options.Entry => Boolean = _ => true - ): String = { - (for { - (name, opt2) <- options.iterator - opt1 = defaults.get(name) - if (opt1.isEmpty || opt1.get.value != opt2.value) && filter(opt2) - } yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else "")) - .toList.sortBy(_._1) - .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString - } + ): String = changed(defaults = defaults, filter = filter).map(_.print_prefs).mkString def save_prefs(file: Path = Options.PREFS, defaults: Options = Options.init0()): Unit = { val prefs = make_prefs(defaults = defaults)