src/Pure/System/options.scala

 
   private val SECTION = "section"
   private val PUBLIC = "public"
   private val OPTION = "option"
   private val OPTIONS = Path.explode("etc/options")
-  private val PREFS_DIR = Path.explode("$ISABELLE_HOME_USER/etc")
-  private val PREFS = PREFS_DIR + Path.basic("preferences")
+  private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
 
   val options_syntax =
     Outer_Syntax.empty + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
       (SECTION, Keyword.DOCUMENT_HEADING) +
       (PUBLIC, Keyword.BEFORE_COMMAND) +

     {
       option_name ~ ($$$("=") ~! option_value) ^^
       { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) }
     }
 
-    def parse_file(syntax: Outer_Syntax, parser: Parser[Options => Options],
-      options: Options, file: Path): Options =
-    {
-      val toks = Token.explode(syntax.keywords, File.read(file))
+    def parse_file(options: Options, file_name: String, content: String,
+      syntax: Outer_Syntax = options_syntax,
+      parser: Parser[Options => Options] = option_entry): Options =
+    {
+      val toks = Token.explode(syntax.keywords, content)
       val ops =
-        parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file.implode))) match {
+        parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file_name))) match {
           case Success(result, _) => result
           case bad => error(bad.toString)
         }
       try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } }
-      catch { case ERROR(msg) => error(msg + Position.here(file.position)) }
-    }
-  }
-
-  def load(file: Path): Options =
-    Parser.parse_file(options_syntax, Parser.option_entry, empty, file)
-
-  def init_defaults(): Options =
+      catch { case ERROR(msg) => error(msg + Position.File(file_name)) }
+    }
+
+    def parse_prefs(options: Options, content: String): Options =
+      parse_file(options, PREFS.base_name, content, syntax = prefs_syntax, parser = prefs_entry)
+  }
+
+  def read_prefs(file: Path = PREFS): String =
+    if (file.is_file) File.read(file) else ""
+
+  def init(prefs: String = read_prefs(PREFS)): Options =
   {
     var options = empty
     for {
       dir <- Isabelle_System.components()
       file = dir + OPTIONS if file.is_file
-    } { options = Parser.parse_file(options_syntax, Parser.option_entry, options, file) }
-    options
-  }
-
-  def init(): Options = init_defaults().load_prefs()
+    } { options = Parser.parse_file(options, file.implode, File.read(file)) }
+    Options.Parser.parse_prefs(options, prefs)
+  }
 
 
   /* encode */
 
   val encode: XML.Encode.T[Options] = (options => options.encode)

     import XML.Encode.{string => string_, _}
     list(pair(properties, pair(string_, pair(string_, string_))))(opts)
   }
 
 
-  /* user preferences */
-
-  def load_prefs(): Options =
-    if (Options.PREFS.is_file)
-      Options.Parser.parse_file(
-        Options.prefs_syntax, Options.Parser.prefs_entry, this, Options.PREFS)
-    else this
-
-  def save_prefs()
-  {
-    val defaults = Options.init_defaults()
+  /* save preferences */
+
+  def save_prefs(file: Path = Options.PREFS)
+  {
+    val defaults: Options = Options.init(prefs = "")
     val changed =
       (for {
         (name, opt2) <- options.iterator
         opt1 = defaults.options.get(name)
         if opt1.isEmpty || opt1.get.value != opt2.value

 
     val prefs =
       changed.sortBy(_._1)
         .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
 
-    Isabelle_System.mkdirs(Options.PREFS_DIR)
-    File.write_backup(Options.PREFS, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs)
+    Isabelle_System.mkdirs(file.dir)
+    File.write_backup(file, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs)
   }
 }
 
 
 class Options_Variable(init_options: Options)