# HG changeset patch
# User wenzelm
# Date 1699369142 -3600
# Node ID 81dab48582c6bc8f4612a47a1bcca2e2f174acc0
# Parent  d305af09fbadb6b5734fc72efeabe4d266aadc02
clarified modules;

diff -r d305af09fbad -r 81dab48582c6 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Nov 07 12:06:59 2023 +0100
+++ b/src/Pure/System/options.scala	Tue Nov 07 15:59:02 2023 +0100
@@ -11,6 +11,17 @@
   val empty: Options = new Options()
 
   object Spec {
+    val syntax: Outer_Syntax = Outer_Syntax.empty + "=" + ","
+
+    def parse(content: String): List[Spec] = {
+      val parser = Parsers.repsep(Parsers.option_spec, Parsers.$$$(","))
+      val reader = Token.reader(Token.explode(syntax.keywords, content), Token.Pos.none)
+      Parsers.parse_all(parser, reader) match {
+        case Parsers.Success(result, _) => result
+        case bad => error(bad.toString)
+      }
+    }
+
     def make(s: String): Spec =
       s match {
         case Properties.Eq(a, b) => Spec(a, Some(b))
@@ -25,7 +36,7 @@
         case Value.Boolean(_) => s
         case Value.Long(_) => s
         case Value.Double(_) => s
-        case _ => Token.quote_name(specs_syntax.keywords, s)
+        case _ => Token.quote_name(syntax.keywords, s)
       }
 
     def print(name: String, value: String): String = Properties.Eq(name, print_value(value))
@@ -158,7 +169,6 @@
       STANDARD + FOR
 
   val prefs_syntax: Outer_Syntax = Outer_Syntax.empty + "="
-  val specs_syntax: Outer_Syntax = prefs_syntax + ","
 
   trait Parsers extends Parse.Parsers {
     val option_name: Parser[String] = atom("option name", _.is_name)
@@ -221,15 +231,6 @@
   def read_prefs(file: Path = PREFS): String =
     if (file.is_file) File.read(file) else ""
 
-  def parse_specs(content: String): List[Spec] = {
-    val parser = Parsers.repsep(Parsers.option_spec, Parsers.$$$(","))
-    val reader = Token.reader(Token.explode(specs_syntax.keywords, content), Token.Pos.none)
-    Parsers.parse_all(parser, reader) match {
-      case Parsers.Success(result, _) => result
-      case bad => error(bad.toString)
-    }
-  }
-
   def inline(content: String): Options = Parsers.parse_file(empty, "inline", content)
 
   def init(prefs: String = read_prefs(file = PREFS), specs: List[Spec] = Nil): Options = {
diff -r d305af09fbad -r 81dab48582c6 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Tue Nov 07 12:06:59 2023 +0100
+++ b/src/Pure/Tools/build_cluster.scala	Tue Nov 07 15:59:02 2023 +0100
@@ -66,7 +66,7 @@
               else error("Missing \":\" after host name")
             str.substring(l)
           }
-          val (specs1, specs2) = Options.parse_specs(rest).partition(is_parameter)
+          val (specs1, specs2) = Options.Spec.parse(rest).partition(is_parameter)
           (parameters ++ specs1, { test_options ++ specs2; specs2 })
         }
         catch {