# HG changeset patch
# User wenzelm
# Date 1678710035 -3600
# Node ID 157ad1f976d2134d14b8268a41f4e4b9d89bf060
# Parent  f458547b4f0fda819726df15e3d1a79fafcd3b28
clarified signature: prefer static types;

diff -r f458547b4f0f -r 157ad1f976d2 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Mar 13 11:02:26 2023 +0100
+++ b/src/Pure/System/options.scala	Mon Mar 13 13:20:35 2023 +0100
@@ -12,6 +12,13 @@
 
   val empty: Options = new Options()
 
+  sealed case class Change(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"
+  }
+
 
   /* typed access */
 
@@ -440,23 +447,16 @@
 
   /* 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[Options.Change] = {
     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))
+      } yield Options.Change(name, opt2.value, opt1.isEmpty))
   }