# HG changeset patch
# User wenzelm
# Date 1520957701 -3600
# Node ID 46fa8c2c142a893d24e73b10f75caed6715a062e
# Parent  7f82445e8f0e1ef63238eccc0e284ae02ebf12d5
more flexible preferences: avoid hardwired file;
tuned signature;

diff -r 7f82445e8f0e -r 46fa8c2c142a src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Mar 13 17:13:20 2018 +0100
+++ b/src/Pure/System/options.scala	Tue Mar 13 17:15:01 2018 +0100
@@ -68,8 +68,7 @@
   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 +
@@ -110,35 +109,37 @@
       { 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 =
+    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, File.read(file))
+      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)) }
+      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 load(file: Path): Options =
-    Parser.parse_file(options_syntax, Parser.option_entry, empty, file)
+  def read_prefs(file: Path = PREFS): String =
+    if (file.is_file) File.read(file) else ""
 
-  def init_defaults(): Options =
+  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
+    } { options = Parser.parse_file(options, file.implode, File.read(file)) }
+    Options.Parser.parse_prefs(options, prefs)
   }
 
-  def init(): Options = init_defaults().load_prefs()
-
 
   /* encode */
 
@@ -387,17 +388,11 @@
   }
 
 
-  /* user preferences */
+  /* save 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()
+  def save_prefs(file: Path = Options.PREFS)
   {
-    val defaults = Options.init_defaults()
+    val defaults: Options = Options.init(prefs = "")
     val changed =
       (for {
         (name, opt2) <- options.iterator
@@ -409,8 +404,8 @@
       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)
   }
 }