--- a/src/Pure/System/options.scala Sun Feb 26 13:06:19 2023 +0100
+++ b/src/Pure/System/options.scala Sun Feb 26 13:15:41 2023 +0100
@@ -418,18 +418,18 @@
/* save preferences */
+ def make_prefs(defaults: Options = Options.init(prefs = "")): String = {
+ (for {
+ (name, opt2) <- options.iterator
+ opt1 = defaults.get(name)
+ if opt1.isEmpty || opt1.get.value != opt2.value
+ } yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else ""))
+ .toList.sortBy(_._1)
+ .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
+ }
+
def save_prefs(file: Path = Options.PREFS, defaults: Options = Options.init(prefs = "")): Unit = {
- val changed =
- (for {
- (name, opt2) <- options.iterator
- opt1 = defaults.get(name)
- if opt1.isEmpty || opt1.get.value != opt2.value
- } yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else "")).toList
-
- val prefs =
- changed.sortBy(_._1)
- .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
-
+ val prefs = make_prefs(defaults = defaults)
Isabelle_System.make_directory(file.dir)
File.write_backup(file, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs)
}
--- a/src/Pure/Tools/build_process.scala Sun Feb 26 13:06:19 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Sun Feb 26 13:15:41 2023 +0100
@@ -423,7 +423,7 @@
db.using_statement(Config.table.insert()) { stmt =>
stmt.string(1) = instance
stmt.string(2) = Isabelle_System.getenv("ML_IDENTIFIER")
- stmt.string(3) = options.changed(Options.init(prefs = "")).mkString("\u0001")
+ stmt.string(3) = options.make_prefs(Options.init(prefs = ""))
stmt.execute()
}