# 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) } }