diff --git a/Admin/etc/options b/Admin/etc/options --- a/Admin/etc/options +++ b/Admin/etc/options @@ -1,25 +1,25 @@ (* :mode=isabelle-options: *) section "Admin tools" option isabelle_components_server : string = "lxbroy10.informatik.tu-muenchen.de" -- "user@host for SSH connection" option isabelle_components_dir : string = "/p/home/isabelle/components" -- "webspace for ISABELLE_COMPONENT_REPOSITORY" option isabelle_components_contrib_dir : string = "/p/home/isabelle/contrib" -- "unpacked components for remote build services" -option build_host_linux_arm : string = "" +option build_host_linux_arm : string = "" for build connection -- "SSH user@host for remote build of heaps" -option build_host_linux : string = "" +option build_host_linux : string = "" for build connection -- "SSH user@host for remote build of heaps" -option build_host_macos : string = "" +option build_host_macos : string = "" for build connection -- "SSH user@host for remote build of heaps" -option build_host_windows : string = "" +option build_host_windows : string = "" for build connection -- "SSH user@host for remote build of heaps" diff --git a/etc/options b/etc/options --- a/etc/options +++ b/etc/options @@ -1,404 +1,404 @@ (* :mode=isabelle-options: *) section "Document Preparation" -option browser_info : bool = false +option browser_info : bool = false for build -- "generate theory browser information" -option document : string = "" (standard "true") +option document : string = "" (standard "true") for build -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")" -option document_output : string = "" (standard "output") +option document_output : string = "" (standard "output") for build -- "document output directory" -option document_echo : bool = false +option document_echo : bool = false for build -- "inform about document file names during session presentation" -option document_variants : string = "document" +option document_variants : string = "document" for build document -- "alternative document variants (separated by colons)" -option document_tags : string = "" +option document_tags : string = "" for document -- "default command tags (separated by commas)" -option document_bibliography : bool = false +option document_bibliography : bool = false for document -- "explicitly enable use of bibtex (default: according to presence of root.bib)" -option document_build : string = "lualatex" (standard "build") +option document_build : string = "lualatex" (standard "build") for document -- "document build engine (e.g. build, lualatex, pdflatex)" -option document_logo : string = "" (standard "_") +option document_logo : string = "" (standard "_") for document -- "generate named instance of Isabelle logo (underscore means unnamed variant)" -option document_heading_prefix : string = "isamarkup" (standard) +option document_heading_prefix : string = "isamarkup" (standard) for document -- "prefix for LaTeX macros generated from 'chapter', 'section' etc." -option document_comment_latex : bool = false +option document_comment_latex : bool = false for document -- "use regular LaTeX version of comment.sty, instead of historic plain TeX version" -option document_cite_commands : string = "cite,nocite,citet,citep" +option document_cite_commands : string = "cite,nocite,citet,citep" for document -- "antiquotation commands to determine the structure of bibliography" -option thy_output_display : bool = false +option thy_output_display : bool = false for content -- "indicate output as multi-line display-style material" -option thy_output_break : bool = false +option thy_output_break : bool = false for content -- "control line breaks in non-display material" -option thy_output_cartouche : bool = false +option thy_output_cartouche : bool = false for content -- "indicate if the output should be delimited as cartouche" -option thy_output_quotes : bool = false +option thy_output_quotes : bool = false for content -- "indicate if the output should be delimited via double quotes" -option thy_output_margin : int = 76 +option thy_output_margin : int = 76 for content -- "right margin / page width for printing of display material" -option thy_output_indent : int = 0 +option thy_output_indent : int = 0 for content -- "indentation for pretty printing of display material" -option thy_output_source : bool = false +option thy_output_source : bool = false for content -- "print original source text rather than internal representation" -option thy_output_source_cartouche : bool = false +option thy_output_source_cartouche : bool = false for content -- "print original source text rather than internal representation, preserve cartouches" -option thy_output_modes : string = "" +option thy_output_modes : string = "" for content -- "additional print modes for document output (separated by commas)" section "Prover Output" -option show_types : bool = false +option show_types : bool = false for content -- "show type constraints when printing terms" -option show_sorts : bool = false +option show_sorts : bool = false for content -- "show sort constraints when printing types" -option show_brackets : bool = false +option show_brackets : bool = false for content -- "show extra brackets when printing terms/types" -option show_question_marks : bool = true +option show_question_marks : bool = true for content -- "show leading question mark of schematic variables" -option show_consts : bool = false +option show_consts : bool = false for content -- "show constants with types when printing proof state" -option show_main_goal : bool = false +option show_main_goal : bool = false for content -- "show main goal when printing proof state" -option goals_limit : int = 10 +option goals_limit : int = 10 for content -- "maximum number of subgoals to be printed" -option show_states : bool = false +option show_states : bool = false for content -- "show toplevel states even if outside of interactive mode" -option names_long : bool = false +option names_long : bool = false for content -- "show fully qualified names" -option names_short : bool = false +option names_short : bool = false for content -- "show base names only" -option names_unique : bool = true +option names_unique : bool = true for content -- "show partially qualified names, as required for unique name resolution" -option eta_contract : bool = true +option eta_contract : bool = true for content -- "print terms in eta-contracted form" -option print_mode : string = "" +option print_mode : string = "" for content -- "additional print modes for prover output (separated by commas)" section "Parallel Processing and Timing" -public option threads : int = 0 +public option threads : int = 0 for build -- "maximum number of worker threads for prover process (0 = hardware max.)" option threads_trace : int = 0 -- "level of tracing information for multithreading" option threads_stack_limit : real = 0.25 -- "maximum stack size for worker threads (in giga words, 0 = unlimited)" -public option parallel_limit : int = 0 +public option parallel_limit : int = 0 for build -- "approximative limit for parallel tasks (0 = unlimited)" -public option parallel_print : bool = true +public option parallel_print : bool = true for build -- "parallel and asynchronous printing of results" -public option parallel_proofs : int = 1 +public option parallel_proofs : int = 1 for build -- "level of parallel proof checking: 0, 1, 2" -option parallel_subproofs_threshold : real = 0.01 +option parallel_subproofs_threshold : real = 0.01 for build -- "lower bound of timing estimate for forked nested proofs (seconds)" -option command_timing_threshold : real = 0.1 +option command_timing_threshold : real = 0.1 for build -- "default threshold for persistent command timing (seconds)" -public option timeout_scale : real = 1.0 +public option timeout_scale : real = 1.0 for build -- "scale factor for timeout in Isabelle/ML and session build" section "Detail of Proof Checking" -option record_proofs : int = -1 +option record_proofs : int = -1 for content -- "set level of proofterm recording: 0, 1, 2, negative means unchanged" -option quick_and_dirty : bool = false +option quick_and_dirty : bool = false for content -- "if true then some tools will OMIT some proofs" -option skip_proofs : bool = false +option skip_proofs : bool = false for content -- "skip over proofs (implicit 'sorry')" -option strict_facts : bool = false +option strict_facts : bool = false for content -- "force lazy facts when defined in context" section "Global Session Parameters" -option condition : string = "" +option condition : string = "" for content -- "required environment variables for subsequent theories (separated by commas)" -option timeout : real = 0 +option timeout : real = 0 for build -- "timeout for session build job (seconds > 0)" -option timeout_build : bool = true +option timeout_build : bool = true for build -- "observe timeout for session build" option process_policy : string = "" -- "command prefix for underlying process, notably ML with NUMA policy" -option process_output_tail : int = 40 +option process_output_tail : int = 40 for build -- "build process output tail shown to user (in lines, 0 = unlimited)" -option profiling : string = "" (standard "time") +option profiling : string = "" (standard "time") for build -- "ML profiling (possible values: time, time_thread, allocations)" -option system_log : string = "" (standard "-") +option system_log : string = "" (standard "-") for build -- "output for system messages (log file or \"-\" for console progress)" -option system_heaps : bool = false +option system_heaps : bool = false for build -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" section "ML System" -option ML_print_depth : int = 20 +option ML_print_depth : int = 20 for content -- "ML print depth for toplevel pretty-printing" public option ML_exception_trace : bool = false -- "ML exception trace for toplevel command execution" public option ML_exception_debugger : bool = false -- "ML debugger exception trace for toplevel command execution" public option ML_debugger : bool = false -- "ML debugger instrumentation for newly compiled code" -public option ML_system_64 : bool = false +public option ML_system_64 : bool = false for build -- "prefer native 64bit platform (change requires restart)" -public option ML_system_apple : bool = true +public option ML_system_apple : bool = true for build# -- "prefer native Apple/ARM64 platform (change requires restart)" section "Build Process" -option pide_reports : bool = true +option pide_reports : bool = true for content -- "report PIDE markup (in ML)" -option build_pide_reports : bool = true +option build_pide_reports : bool = true for content -- "report PIDE markup (in batch build)" option build_hostname : string = "" -- "alternative hostname for build process (default $ISABELLE_HOSTNAME)" option build_engine : string = "" -- "alternative session build engine" option build_database_test : bool = false -- "expose state of build process via central database" section "Editor Session" public option editor_load_delay : real = 0.5 -- "delay for file load operations (new buffers etc.)" public option editor_input_delay : real = 0.2 -- "delay for user input (text edits, cursor movement etc.)" public option editor_generated_input_delay : real = 1.0 -- "delay for machine-generated input that may outperform user edits" public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" public option editor_consolidate_delay : real = 1.0 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" option editor_prune_size : int = 0 -- "retained size of pruned history (delete old versions)" public option editor_update_delay : real = 0.5 -- "delay for physical GUI updates" public option editor_reparse_limit : int = 10000 -- "maximum amount of reparsed text outside perspective" public option editor_tracing_messages : int = 1000 -- "initial number of tracing messages for each command transaction (0: unbounded)" public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" public option editor_continuous_checking : bool = true -- "continuous checking of proof document (visible and required parts)" public option editor_output_state : bool = false -- "implicit output of proof state" public option editor_document_session : string = "" -- "session for interactive document preparation" public option editor_document_auto : bool = false -- "automatically build document when selected theories are finished" public option editor_document_delay : real = 2.0 -- "delay for document auto build" option editor_execution_delay : real = 0.02 -- "delay for start of execution process after document update (seconds)" option editor_syslog_limit : int = 100 -- "maximum amount of buffered syslog messages" section "Headless Session" option headless_consolidate_delay : real = 15 -- "delay to consolidate status of command evaluation (execution forks)" option headless_prune_delay : real = 60 -- "delay to prune history (delete old versions)" option headless_check_delay : real = 0.5 -- "delay for theory status check during PIDE processing (seconds)" option headless_check_limit : int = 0 -- "maximum number of theory status checks (0 = unlimited)" option headless_nodes_status_delay : real = -1 -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)" option headless_watchdog_timeout : real = 600 -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)" option headless_commit_cleanup_delay : real = 60 -- "delay for cleanup of already imported theories (seconds, 0 = disabled)" option headless_load_limit : real = 5.0 -- "limit in MB for loaded theory files (0 = unlimited)" section "Miscellaneous Tools" public option find_theorems_limit : int = 40 -- "limit of displayed results" public option find_theorems_tactic_limit : int = 5 -- "limit of tactic search for 'solves' criterion" section "Completion" public option completion_limit : int = 40 -- "limit for completion within the formal context" public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" -- "glob patterns to ignore in file-system path completion (separated by colons)" section "Spell Checker" -public option spell_checker : bool = true +public option spell_checker : bool = true for content -- "enable spell-checker for prose words within document text, comments etc." -public option spell_checker_dictionary : string = "en" +public option spell_checker_dictionary : string = "en" for content -- "spell-checker dictionary name" -public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" +public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" for content -- "included markup elements for spell-checker (separated by commas)" -public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text" +public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text" for content -- "excluded markup elements for spell-checker (separated by commas)" section "Secure Shell (OpenSSH)" public option ssh_batch_mode : bool = true -- "enable SSH batch mode (no user interaction)" public option ssh_multiplexing : bool = true -- "enable multiplexing of SSH sessions (ignored on Windows)" public option ssh_compression : bool = true -- "enable SSH compression" public option ssh_alive_interval : real = 30 -- "time interval to keep SSH server connection alive (seconds, ignore value < 0)" public option ssh_alive_count_max : int = 3 -- "maximum number of messages to keep SSH server connection alive (ignore value < 0)" section "Phabricator" option phabricator_version_arcanist : string = "4f70fcffa8a5393e210d64f237ffdaa256256d6a" -- "repository version for arcanist" option phabricator_version_phabricator : string = "193798385bd3a7f72dca255e44f8112f4f8fc155" -- "repository version for phabricator" section "Theory Export" -option export_theory : bool = false +option export_theory : bool = false for content -- "export theory content to Isabelle/Scala" -option export_standard_proofs : bool = false +option export_standard_proofs : bool = false for content -- "export standardized proof terms to Isabelle/Scala (not scalable)" -option export_proofs : bool = false +option export_proofs : bool = false for content -- "export proof terms to Isabelle/Scala" -option prune_proofs : bool = false +option prune_proofs : bool = false for content -- "prune proof terms after export (do not store in Isabelle/ML)" section "Theory update" -option update_inner_syntax_cartouches : bool = false +option update_inner_syntax_cartouches : bool = false for content update -- "update inner syntax (types, terms, etc.) to use cartouches" -option update_mixfix_cartouches : bool = false +option update_mixfix_cartouches : bool = false for content update -- "update mixfix templates to use cartouches instead of double quotes" -option update_control_cartouches : bool = false +option update_control_cartouches : bool = false for content update -- "update antiquotations to use control symbol with cartouche argument" -option update_path_cartouches : bool = false +option update_path_cartouches : bool = false for content update -- "update file-system paths to use cartouches" -option update_cite : bool = false +option update_cite : bool = false for content update -- "update cite commands and antiquotations" section "Build Database" -option build_database_server : bool = false -option build_database_user : string = "" -option build_database_password : string = "" -option build_database_name : string = "" -option build_database_host : string = "" -option build_database_port : int = 0 -option build_database_ssh_host : string = "" -option build_database_ssh_user : string = "" -option build_database_ssh_port : int = 0 +option build_database_server : bool = false for connection +option build_database_user : string = "" for connection +option build_database_password : string = "" for connection +option build_database_name : string = "" for connection +option build_database_host : string = "" for connection +option build_database_port : int = 0 for connection +option build_database_ssh_host : string = "" for connection +option build_database_ssh_user : string = "" for connection +option build_database_ssh_port : int = 0 for connection section "Build Log Database" -option build_log_database_user : string = "" -option build_log_database_password : string = "" -option build_log_database_name : string = "" -option build_log_database_host : string = "" -option build_log_database_port : int = 0 -option build_log_ssh_host : string = "" -option build_log_ssh_user : string = "" -option build_log_ssh_port : int = 0 +option build_log_database_user : string = "" for connection +option build_log_database_password : string = "" for connection +option build_log_database_name : string = "" for connection +option build_log_database_host : string = "" for connection +option build_log_database_port : int = 0 for connection +option build_log_ssh_host : string = "" for connection +option build_log_ssh_user : string = "" for connection +option build_log_ssh_port : int = 0 for connection option build_log_history : int = 30 -- "length of relevant history (in days)" option build_log_transaction_size : int = 1 -- "number of log files for each db update" section "Isabelle/Scala/ML system channel" -option system_channel_address : string = "" -option system_channel_password : string = "" +option system_channel_address : string = "" for connection +option system_channel_password : string = "" for connection section "Bash process execution server" -option bash_process_debugging : bool = false -option bash_process_address : string = "" -option bash_process_password : string = "" +option bash_process_debugging : bool = false for connection +option bash_process_address : string = "" for connection +option bash_process_password : string = "" for connection diff --git a/src/Pure/System/options.scala b/src/Pure/System/options.scala --- a/src/Pure/System/options.scala +++ b/src/Pure/System/options.scala @@ -1,462 +1,482 @@ /* Title: Pure/System/options.scala Author: Makarius System options with external string representation. */ package isabelle object Options { type Spec = (String, Option[String]) val empty: Options = new Options() /* typed access */ abstract class Access[A](val options: Options) { def apply(name: String): A def update(name: String, x: A): Options def change(name: String, f: A => A): Options = update(name, f(apply(name))) } class Access_Variable[A]( val options: Options_Variable, val pure_access: Options => Access[A] ) { def apply(name: String): A = pure_access(options.value)(name) def update(name: String, x: A): Unit = options.change(options => pure_access(options).update(name, x)) def change(name: String, f: A => A): Unit = update(name, f(apply(name))) } /* representation */ sealed abstract class Type { def print: String = Word.lowercase(toString) } case object Bool extends Type case object Int extends Type case object Real extends Type case object String extends Type case object Unknown extends Type + val TAG_CONTENT = "content" + val TAG_DOCUMENT = "document" + val TAG_BUILD = "build" + val TAG_UPDATE = "update" + val TAG_CONNECTION = "connection" + case class Opt( public: Boolean, pos: Position.T, name: String, typ: Type, value: String, default_value: String, standard_value: Option[String], + tags: List[String], description: String, section: String ) { private def print_value(x: String): String = if (typ == Options.String) quote(x) else x private def print_standard: String = standard_value match { case None => "" case Some(s) if s == default_value => " (standard)" case Some(s) => " (standard " + print_value(s) + ")" } private def print(default: Boolean): String = { val x = if (default) default_value else value "option " + name + " : " + typ.print + " = " + print_value(x) + print_standard + if_proper(description, "\n -- " + quote(description)) } def print: String = print(false) def print_default: String = print(true) def title(strip: String = ""): String = { val words = Word.explode('_', name) val words1 = words match { case word :: rest if word == strip => rest case _ => words } Word.implode(words1.map(Word.perhaps_capitalize)) } def title_jedit: String = title("jedit") def unknown: Boolean = typ == Unknown + + def has_tag(tag: String): Boolean = tags.contains(tag) + def is_exported: Boolean = !has_tag(TAG_CONNECTION) } /* parsing */ private val SECTION = "section" private val PUBLIC = "public" private val OPTION = "option" private val STANDARD = "standard" + private val FOR = "for" private val OPTIONS = Path.explode("etc/options") private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences") val options_syntax: Outer_Syntax = Outer_Syntax.empty + ":" + "=" + "--" + "(" + ")" + Symbol.comment + Symbol.comment_decoded + (SECTION, Keyword.DOCUMENT_HEADING) + (PUBLIC, Keyword.BEFORE_COMMAND) + (OPTION, Keyword.THY_DECL) + - STANDARD + STANDARD + FOR val prefs_syntax: Outer_Syntax = Outer_Syntax.empty + "=" trait Parsers extends Parse.Parsers { val option_name: Parser[String] = atom("option name", _.is_name) val option_type: Parser[String] = atom("option type", _.is_name) val option_value: Parser[String] = opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^ { case s ~ n => if (s.isDefined) "-" + n else n } | atom("option value", tok => tok.is_name || tok.is_float) val option_standard: Parser[Option[String]] = $$$("(") ~! $$$(STANDARD) ~ opt(option_value) ~ $$$(")") ^^ { case _ ~ _ ~ a ~ _ => a } + val option_tag: Parser[String] = atom("option tag", _.is_name) + val option_tags: Parser[List[String]] = + $$$(FOR) ~! rep(option_tag) ^^ { case _ ~ x => x } | success(Nil) } private object Parsers extends Parsers { def comment_marker: Parser[String] = $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded) val option_entry: Parser[Options => Options] = { command(SECTION) ~! text ^^ { case _ ~ a => (options: Options) => options.set_section(a) } | opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~ - $$$("=") ~ option_value ~ opt(option_standard) ~ + $$$("=") ~ option_value ~ opt(option_standard) ~ option_tags ~ (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^ - { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e ~ f) => - (options: Options) => options.declare(a.isDefined, pos, b, c, d, e, f) } + { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e ~ f ~ g) => + (options: Options) => options.declare(a.isDefined, pos, b, c, d, e, f, g) } } val prefs_entry: Parser[Options => Options] = { option_name ~ ($$$("=") ~! option_value) ^^ { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) } } 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_name))) match { case Success(result, _) => result case bad => error(bad.toString) } try { ops.foldLeft(options.set_section("")) { case (opts, op) => op(opts) } } catch { case ERROR(msg) => error(msg + Position.here(Position.File(file_name))) } } def parse_prefs(options: Options, content: String): Options = parse_file(options, PREFS.file_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), opts: List[String] = Nil): Options = { var options = empty for { dir <- Components.directories() file = dir + OPTIONS if file.is_file } { options = Parsers.parse_file(options, file.implode, File.read(file)) } opts.foldLeft(Parsers.parse_prefs(options, prefs))(_ + _) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options", Scala_Project.here, { args => var build_options = false var get_option = "" var list_options = false var export_file = "" val getopts = Getopts(""" Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] Options are: -b include $ISABELLE_BUILD_OPTIONS -g OPTION get value of OPTION -l list options -x FILE export options to FILE in YXML format Report Isabelle system options, augmented by MORE_OPTIONS given as arguments NAME=VAL or NAME. """, "b" -> (_ => build_options = true), "g:" -> (arg => get_option = arg), "l" -> (_ => list_options = true), "x:" -> (arg => export_file = arg)) val more_options = getopts(args) if (get_option == "" && !list_options && export_file == "") getopts.usage() val options = { val options0 = Options.init() val options1 = if (build_options) Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _) else options0 more_options.foldLeft(options1)(_ + _) } if (get_option != "") Output.writeln(options.check_name(get_option).value, stdout = true) if (export_file != "") File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) if (get_option == "" && export_file == "") Output.writeln(options.print, stdout = true) }) } final class Options private( options: Map[String, Options.Opt] = Map.empty, val section: String = "" ) { def opt_iterator: Iterator[(String, Options.Opt)] = options.iterator override def toString: String = opt_iterator.mkString("Options(", ",", ")") private def print_opt(opt: Options.Opt): String = if (opt.public) "public " + opt.print else opt.print def print: String = cat_lines(opt_iterator.toList.sortBy(_._1).map(p => print_opt(p._2))) def description(name: String): String = check_name(name).description /* check */ def get(name: String): Option[Options.Opt] = options.get(name) def check_name(name: String): Options.Opt = get(name) match { case Some(opt) if !opt.unknown => opt case _ => error("Unknown option " + quote(name)) } private def check_type(name: String, typ: Options.Type): Options.Opt = { val opt = check_name(name) if (opt.typ == typ) opt else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print) } /* basic operations */ private def put(name: String, typ: Options.Type, value: String): Options = { val opt = check_type(name, typ) new Options(options + (name -> opt.copy(value = value)), section) } private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A = { val opt = check_type(name, typ) parse(opt.value) match { case Some(x) => x case None => error("Malformed value for option " + quote(name) + " : " + typ.print + " =\n" + quote(opt.value)) } } /* internal lookup and update */ val bool: Options.Access[Boolean] = new Options.Access[Boolean](this) { def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply) def update(name: String, x: Boolean): Options = put(name, Options.Bool, Value.Boolean(x)) } val int: Options.Access[Int] = new Options.Access[Int](this) { def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply) def update(name: String, x: Int): Options = put(name, Options.Int, Value.Int(x)) } val real: Options.Access[Double] = new Options.Access[Double](this) { def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply) def update(name: String, x: Double): Options = put(name, Options.Real, Value.Double(x)) } val string: Options.Access[String] = new Options.Access[String](this) { def apply(name: String): String = get(name, Options.String, Some(_)) def update(name: String, x: String): Options = put(name, Options.String, x) } def proper_string(name: String): Option[String] = Library.proper_string(string(name)) def seconds(name: String): Time = Time.seconds(real(name)) /* external updates */ private def check_value(name: String): Options = { val opt = check_name(name) opt.typ match { case Options.Bool => bool(name); this case Options.Int => int(name); this case Options.Real => real(name); this case Options.String => string(name); this case Options.Unknown => this } } def declare( public: Boolean, pos: Position.T, name: String, typ_name: String, value: String, standard: Option[Option[String]], + tags: List[String], description: String ): Options = { get(name) match { case Some(other) => error("Duplicate declaration of option " + quote(name) + Position.here(pos) + Position.here(other.pos)) case None => val typ = typ_name match { case "bool" => Options.Bool case "int" => Options.Int case "real" => Options.Real case "string" => Options.String case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name) + Position.here(pos)) } val standard_value = standard match { case None => None case Some(_) if typ == Options.Bool => error("Illegal standard value for option " + quote(name) + " : " + typ_name + Position.here) case Some(s) => Some(s.getOrElse(value)) } val opt = - Options.Opt(public, pos, name, typ, value, value, standard_value, description, section) + Options.Opt( + public, pos, name, typ, value, value, standard_value, tags, description, section) (new Options(options + (name -> opt), section)).check_value(name) } } def add_permissive(name: String, value: String): Options = { if (options.isDefinedAt(name)) this + (name, value) else { - val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, None, "", "") + val opt = + Options.Opt(false, Position.none, name, Options.Unknown, value, value, None, Nil, "", "") new Options(options + (name -> opt), section) } } def + (name: String, value: String): Options = { val opt = check_name(name) (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name) } def + (name: String, opt_value: Option[String]): Options = { val opt = check_name(name) opt_value orElse opt.standard_value match { case Some(value) => this + (name, value) case None if opt.typ == Options.Bool => this + (name, "true") case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print) } } def + (str: String): Options = str match { case Properties.Eq(a, b) => this + (a, b) case _ => this + (str, None) } def ++ (specs: List[Options.Spec]): Options = specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) } /* sections */ def set_section(new_section: String): Options = new Options(options, new_section) def sections: List[(String, List[Options.Opt])] = options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) }) /* encode */ def encode: XML.Body = { val opts = for ((_, opt) <- options.toList; if !opt.unknown) yield (opt.pos, (opt.name, (opt.typ.print, opt.value))) import XML.Encode.{string => string_, _} list(pair(properties, pair(string_, pair(string_, string_))))(opts) } /* changed options */ def changed(defaults: Options = Options.init(prefs = "")): List[String] = (for { (name, opt2) <- options.iterator opt1 = defaults.get(name) if opt1.isEmpty || opt1.get.value != opt2.value } yield (name, opt2.value)).toList.sortBy(_._1).map({ case (x, y) => Properties.Eq(x, y) }) /* save preferences */ - def make_prefs(defaults: Options = Options.init(prefs = "")): String = { + def make_prefs( + defaults: Options = Options.init(prefs = ""), + filter: Options.Opt => Boolean = _ => true + ): String = { (for { (name, opt2) <- options.iterator opt1 = defaults.get(name) - if opt1.isEmpty || opt1.get.value != opt2.value + if (opt1.isEmpty || opt1.get.value != opt2.value) && filter(opt2) } 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 prefs = make_prefs(defaults = defaults) Isabelle_System.make_directory(file.dir) File.write_backup(file, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs) } } class Options_Variable(init_options: Options) { private var _options = init_options def value: Options = synchronized { _options } def change(f: Options => Options): Unit = synchronized { _options = f(_options) } def += (name: String, x: String): Unit = change(options => options + (name, x)) val bool: Options.Access_Variable[Boolean] = new Options.Access_Variable[Boolean](this, _.bool) val int: Options.Access_Variable[Int] = new Options.Access_Variable[Int](this, _.int) val real: Options.Access_Variable[Double] = new Options.Access_Variable[Double](this, _.real) val string: Options.Access_Variable[String] = new Options.Access_Variable[String](this, _.string) def proper_string(name: String): Option[String] = Library.proper_string(string(name)) def seconds(name: String): Time = value.seconds(name) }