equal
deleted
inserted
replaced
122 try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } } |
122 try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } } |
123 catch { case ERROR(msg) => error(msg + Position.File(file_name)) } |
123 catch { case ERROR(msg) => error(msg + Position.File(file_name)) } |
124 } |
124 } |
125 |
125 |
126 def parse_prefs(options: Options, content: String): Options = |
126 def parse_prefs(options: Options, content: String): Options = |
127 parse_file(options, PREFS.base_name, content, syntax = prefs_syntax, parser = prefs_entry) |
127 parse_file(options, PREFS.file_name, content, syntax = prefs_syntax, parser = prefs_entry) |
128 } |
128 } |
129 |
129 |
130 def read_prefs(file: Path = PREFS): String = |
130 def read_prefs(file: Path = PREFS): String = |
131 if (file.is_file) File.read(file) else "" |
131 if (file.is_file) File.read(file) else "" |
132 |
132 |