# 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)