# HG changeset patch
# User wenzelm
# Date 1689774002 -7200
# Node ID b262ecc983190dd1b31031e7436b46497436e855
# Parent  2ece6509ad6f61e010e045e3db5862d8b61a34a5
more operations for independent "inline" options;

diff -r 2ece6509ad6f -r b262ecc98319 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Jul 19 13:29:18 2023 +0200
+++ b/src/Pure/System/options.scala	Wed Jul 19 15:40:02 2023 +0200
@@ -140,6 +140,7 @@
       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)
@@ -153,6 +154,9 @@
     val option_tag: Parser[String] = atom("option tag", _.is_name)
     val option_tags: Parser[List[String]] =
       $$$(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) }
   }
 
   private object Parsers extends Parsers {
@@ -199,6 +203,17 @@
   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 = {
     var options = empty
     for {
@@ -273,6 +288,8 @@
   options: Map[String, Options.Entry] = Map.empty,
   val section: String = ""
 ) {
+  def defined(name: String): Boolean = options.isDefinedAt(name)
+
   def iterator: Iterator[Options.Entry] = options.valuesIterator
 
   override def toString: String = iterator.mkString("Options(", ",", ")")
@@ -405,7 +422,7 @@
 
   def + (spec: Options.Spec): Options = {
     val name = spec.name
-    if (spec.permissive && !options.isDefinedAt(name)) {
+    if (spec.permissive && !defined(name)) {
       val value = spec.value.getOrElse("")
       val opt =
         Options.Entry(false, Position.none, name, Options.Unknown, value, value, None, Nil, "", "")
diff -r 2ece6509ad6f -r b262ecc98319 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Jul 19 13:29:18 2023 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Jul 19 15:40:02 2023 +0200
@@ -1117,10 +1117,7 @@
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) }
 
     private val session_entry: Parser[Session_Entry] = {
-      val option =
-        option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
-          { case x ~ y => Options.Spec(x, y) }
-      val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
+      val options = $$$("[") ~> rep1sep(option_spec, $$$(",")) <~ $$$("]")
 
       val theory_entry =
         position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) }