# HG changeset patch
# User wenzelm
# Date 1677238840 -3600
# Node ID 8d6ba14f9d22fa87a9c25e4ab4ad9b51d2eb56eb
# Parent  a10fa21128548283a3b37fefa45b313060a75098
clarified signature: more operations;

diff -r a10fa2112854 -r 8d6ba14f9d22 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Fri Feb 24 11:45:39 2023 +0100
+++ b/src/Pure/System/options.scala	Fri Feb 24 12:40:40 2023 +0100
@@ -406,10 +406,19 @@
   }
 
 
+  /* changed options */
+
+  def changed(defaults: Options = Options.init(prefs = "")): List[String] =
+    (for {
+      (name, opt2) <- options.iterator
+      opt1 = defaults.get(name)
+      if opt1.isEmpty || opt1.get.value != opt2.value
+    } yield (name, opt2.value)).toList.sortBy(_._1).map({ case (x, y) => Properties.Eq(x, y) })
+
+
   /* save preferences */
 
-  def save_prefs(file: Path = Options.PREFS): Unit = {
-    val defaults: Options = Options.init(prefs = "")
+  def save_prefs(file: Path = Options.PREFS, defaults: Options = Options.init(prefs = "")): Unit = {
     val changed =
       (for {
         (name, opt2) <- options.iterator