# HG changeset patch
# User wenzelm
# Date 1699445699 -3600
# Node ID e97fa2edf4b2ccf053b0daba2052d168207ead97
# Parent  90756ad4d8d7963dce9168ffc07d439164c6ecf4
clarified signature;

diff -r 90756ad4d8d7 -r e97fa2edf4b2 src/Pure/System/benchmark.scala
--- a/src/Pure/System/benchmark.scala	Wed Nov 08 13:00:24 2023 +0100
+++ b/src/Pure/System/benchmark.scala	Wed Nov 08 13:14:59 2023 +0100
@@ -14,7 +14,7 @@
     ssh: SSH.System = SSH.Local,
     isabelle_home: Path = Path.current,
   ): String = {
-    val options = Options.Spec("build_hostname", Some(host.name)) :: host.options
+    val options = Options.Spec.eq("build_hostname", host.name) :: host.options
     ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " benchmark" +
       Options.Spec.bash_strings(options, bg = true)
   }
diff -r 90756ad4d8d7 -r e97fa2edf4b2 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Nov 08 13:00:24 2023 +0100
+++ b/src/Pure/System/options.scala	Wed Nov 08 13:14:59 2023 +0100
@@ -22,9 +22,12 @@
       }
     }
 
+    def eq(a: String, b: String, permissive: Boolean = false): Spec =
+      Spec(a, value = Some(b), permissive = permissive)
+
     def make(s: String): Spec =
       s match {
-        case Properties.Eq(a, b) => Spec(a, Some(b))
+        case Properties.Eq(a, b) => eq(a, b)
         case _ => Spec(s)
       }
 
@@ -61,7 +64,7 @@
   }
 
   sealed case class Change(name: String, value: String, unknown: Boolean) {
-    def spec: Spec = Spec(name, Some(value))
+    def spec: Spec = Spec.eq(name, value)
 
     def print_prefs: String =
       name + " = " + Outer_Syntax.quote_string(value) +
@@ -190,7 +193,7 @@
       $$$(FOR) ~! rep(option_tag) ^^ { case _ ~ x => x } | success(Nil)
     val option_spec: Parser[Spec] =
       option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
-        { case x ~ y => Options.Spec(x, y) }
+        { case x ~ y => Options.Spec(x, value = y) }
   }
 
   private object Parsers extends Parsers {
@@ -210,7 +213,7 @@
     val prefs_entry: Parser[Options => Options] = {
       option_name ~ ($$$("=") ~! option_value) ^^
       { case a ~ (_ ~ b) => (options: Options) =>
-          options + Options.Spec(a, Some(b), permissive = true) }
+          options + Options.Spec.eq(a, b, permissive = true) }
     }
 
     def parse_file(
@@ -328,7 +331,7 @@
   def description(name: String): String = check_name(name).description
 
   def spec(name: String): Options.Spec =
-    Options.Spec(name, Some(check_name(name).value))
+    Options.Spec.eq(name, check_name(name).value)
 
 
   /* check */
@@ -529,7 +532,7 @@
 
   def value: Options = synchronized { _options }
   def change(f: Options => Options): Unit = synchronized { _options = f(_options) }
-  def += (name: String, x: String): Unit = change(options => options + Options.Spec(name, Some(x)))
+  def += (name: String, x: String): Unit = change(options => options + Options.Spec.eq(name, x))
 
   val bool: Options.Access_Variable[Boolean] =
     new Options.Access_Variable[Boolean](this, _.bool)
diff -r 90756ad4d8d7 -r e97fa2edf4b2 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Nov 08 13:00:24 2023 +0100
+++ b/src/Pure/Tools/build.scala	Wed Nov 08 13:14:59 2023 +0100
@@ -582,8 +582,7 @@
     quiet: Boolean = false,
     verbose: Boolean = false
   ): String = {
-    val options =
-      build_options ::: Options.Spec("build_hostname", Some(host.name)) :: host.options
+    val options = build_options ::: Options.Spec.eq("build_hostname", host.name) :: host.options
     ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " build_worker" +
       if_proper(build_id, " -B " + Bash.string(build_id)) +
       if_proper(afp_root, " -A " + ssh.bash_path(afp_root.get)) +
diff -r 90756ad4d8d7 -r e97fa2edf4b2 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Wed Nov 08 13:00:24 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Wed Nov 08 13:14:59 2023 +0100
@@ -186,7 +186,7 @@
           }
         text_area.peer.setInputVerifier({
             case text: JTextComponent =>
-              try { value + Options.Spec(opt_name, Some(text.getText)); true }
+              try { value + Options.Spec.eq(opt_name, text.getText); true }
               catch { case ERROR(_) => false }
             case _ => true
           })