# HG changeset patch
# User wenzelm
# Date 1678711405 -3600
# Node ID 809ad223f40694b289cc58052d718c647d8544d7
# Parent  157ad1f976d2134d14b8268a41f4e4b9d89bf060
clarified signature: more explicit types;

diff -r 157ad1f976d2 -r 809ad223f406 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Mar 13 13:20:35 2023 +0100
+++ b/src/Pure/System/options.scala	Mon Mar 13 13:43:25 2023 +0100
@@ -8,9 +8,9 @@
 
 
 object Options {
-  type Spec = (String, Option[String])
+  val empty: Options = new Options()
 
-  val empty: Options = new Options()
+  sealed case class Spec(name: String, value: Option[String] = None)
 
   sealed case class Change(name: String, value: String, unknown: Boolean) {
     def print_props: String = Properties.Eq(name, value)
@@ -421,7 +421,7 @@
     }
 
   def ++ (specs: List[Options.Spec]): Options =
-    specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) }
+    specs.foldLeft(this) { case (x, Options.Spec(y, z)) => x + (y, z) }
 
 
   /* sections */
diff -r 157ad1f976d2 -r 809ad223f406 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Mar 13 13:20:35 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Mar 13 13:43:25 2023 +0100
@@ -1168,7 +1168,7 @@
     private val session_entry: Parser[Session_Entry] = {
       val option =
         option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
-          { case x ~ y => (x, y) }
+          { case x ~ y => Options.Spec(x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
       val theory_entry =
diff -r 157ad1f976d2 -r 809ad223f406 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Mon Mar 13 13:20:35 2023 +0100
+++ b/src/Pure/Tools/update.scala	Mon Mar 13 13:43:25 2023 +0100
@@ -194,7 +194,7 @@
         "l:" -> (arg => base_logics = space_explode(',', arg)),
         "n" -> (_ => no_build = true),
         "o:" -> (arg => options = options + arg),
-        "u:" -> (arg => update_options = update_options ::: List(("update_" + arg, None))),
+        "u:" -> (arg => update_options = update_options ::: List(Options.Spec("update_" + arg))),
         "v" -> (_ => verbose = true),
         "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))