# HG changeset patch
# User wenzelm
# Date 1677413741 -3600
# Node ID 268bf61631ec23b8a2f51cdadcf90a559614a78f
# Parent  eaf234b0c849c9fd09acc2724625169e166a159e
more robust options in "prefs" format: avoid odd control character;

diff -r eaf234b0c849 -r 268bf61631ec src/Pure/System/options.scala
--- 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)
   }
diff -r eaf234b0c849 -r 268bf61631ec src/Pure/Tools/build_process.scala
--- 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()
       }