# HG changeset patch # User wenzelm # Date 1368734521 -7200 # Node ID 16c4e428a1d422cbad1af328c96433af587dcb3e # Parent a354c83dee438884870779283269ac1b2093e34b# Parent 286629271d65a1764b95afeda986102fcb9f6d6d merged diff -r a354c83dee43 -r 16c4e428a1d4 etc/options --- a/etc/options Thu May 16 21:55:12 2013 +0200 +++ b/etc/options Thu May 16 22:02:01 2013 +0200 @@ -14,22 +14,6 @@ option document_graph : bool = false -- "generate session graph image for document" -option goals_limit : int = 10 - -- "maximum number of subgoals to be printed" - -option show_question_marks : bool = true - -- "show leading question mark of schematic variables" - -option names_long : bool = false - -- "show fully qualified names" -option names_short : bool = false - -- "show base names only" -option names_unique : bool = true - -- "show partially qualified names, as required for unique name resolution" - -option pretty_margin : int = 76 - -- "right margin / page width of pretty printer in Isabelle/ML" - option thy_output_display : bool = false -- "indicate output as multi-line display-style material" option thy_output_break : bool = false @@ -40,8 +24,41 @@ -- "indentation for pretty printing of display material" option thy_output_source : bool = false -- "print original source text rather than internal representation" +option thy_output_modes : string = "" + -- "additional print modes for document output (separated by commas)" +section "Prover Output" + +option show_types : bool = false + -- "show type constraints when printing terms" +option show_sorts : bool = false + -- "show sort constraints when printing types" +option show_brackets : bool = false + -- "show extra brackets when printing terms/types" +option show_question_marks : bool = true + -- "show leading question mark of schematic variables" + +option show_consts : bool = false + -- "show constants with types when printing proof state" +option show_main_goal : bool = false + -- "show main goal when printing proof state" +option goals_limit : int = 10 + -- "maximum number of subgoals to be printed" + +option names_long : bool = false + -- "show fully qualified names" +option names_short : bool = false + -- "show base names only" +option names_unique : bool = true + -- "show partially qualified names, as required for unique name resolution" + +option eta_contract : bool = true + -- "print terms in eta-contracted form" + +option pretty_margin : int = 76 + -- "right margin / page width of pretty printer in Isabelle/ML" + option print_mode : string = "" -- "additional print modes for prover output (separated by commas)" diff -r a354c83dee43 -r 16c4e428a1d4 src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Thu May 16 21:55:12 2013 +0200 +++ b/src/HOL/Prolog/prolog.ML Thu May 16 22:02:01 2013 +0200 @@ -2,7 +2,7 @@ Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) *) -Goal_Display.show_main_goal_default := true; +Options.default_put_bool @{option show_main_goal} true; structure Prolog = struct diff -r a354c83dee43 -r 16c4e428a1d4 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu May 16 21:55:12 2013 +0200 +++ b/src/Pure/Isar/attrib.ML Thu May 16 22:02:01 2013 +0200 @@ -57,8 +57,16 @@ (Context.generic -> string) -> string Config.T * (theory -> theory) val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T + val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T - val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T + val option_bool: string -> bool Config.T * (theory -> theory) + val option_int: string -> int Config.T * (theory -> theory) + val option_real: string -> real Config.T * (theory -> theory) + val option_string: string -> string Config.T * (theory -> theory) + val setup_option_bool: string -> bool Config.T + val setup_option_int: string -> int Config.T + val setup_option_real: string -> real Config.T + val setup_option_string: string -> string Config.T end; structure Attrib: ATTRIB = @@ -476,19 +484,19 @@ fun declare make coerce binding default = let val name = Binding.name_of binding; - val config_value = Config.declare_generic {global = false} name (make o default); + val config_value = Config.declare name (make o default); val config = coerce config_value; in (config, register binding config_value) end; in +fun register_config config = register (Binding.name (Config.name_of config)) config; + val config_bool = declare Config.Bool Config.bool; val config_int = declare Config.Int Config.int; val config_real = declare Config.Real Config.real; val config_string = declare Config.String Config.string; -fun register_config config = register (Binding.name (Config.name_of config)) config; - end; @@ -512,6 +520,36 @@ end; +(* system options *) + +local + +fun declare_option coerce name = + let + val config = Config.declare_option name; + in (coerce config, register_config config) end; + +fun setup_option coerce name = + let + val config = Config.declare_option name; + val _ = Context.>> (Context.map_theory (register_config config)); + in coerce config end; + +in + +val option_bool = declare_option Config.bool; +val option_int = declare_option Config.int; +val option_real = declare_option Config.real; +val option_string = declare_option Config.string; + +val setup_option_bool = setup_option Config.bool; +val setup_option_int = setup_option Config.int; +val setup_option_real = setup_option Config.real; +val setup_option_string = setup_option Config.string; + +end; + + (* theory setup *) val _ = Context.>> (Context.map_theory diff -r a354c83dee43 -r 16c4e428a1d4 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu May 16 21:55:12 2013 +0200 +++ b/src/Pure/Syntax/printer.ML Thu May 16 22:02:01 2013 +0200 @@ -20,11 +20,8 @@ signature PRINTER = sig include BASIC_PRINTER - val show_brackets_default: bool Unsynchronized.ref val show_brackets_raw: Config.raw - val show_types_default: bool Unsynchronized.ref val show_types_raw: Config.raw - val show_sorts_default: bool Unsynchronized.ref val show_sorts_raw: Config.raw val show_markup_default: bool Unsynchronized.ref val show_markup_raw: Config.raw @@ -53,17 +50,13 @@ (** options for printing **) -val show_brackets_default = Unsynchronized.ref false; -val show_brackets_raw = - Config.declare "show_brackets" (fn _ => Config.Bool (! show_brackets_default)); +val show_brackets_raw = Config.declare_option "show_brackets"; val show_brackets = Config.bool show_brackets_raw; -val show_types_default = Unsynchronized.ref false; -val show_types_raw = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default)); +val show_types_raw = Config.declare_option "show_types"; val show_types = Config.bool show_types_raw; -val show_sorts_default = Unsynchronized.ref false; -val show_sorts_raw = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default)); +val show_sorts_raw = Config.declare_option "show_sorts"; val show_sorts = Config.bool show_sorts_raw; val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true)); diff -r a354c83dee43 -r 16c4e428a1d4 src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Thu May 16 21:55:12 2013 +0200 +++ b/src/Pure/Syntax/syntax_trans.ML Thu May 16 22:02:01 2013 +0200 @@ -28,7 +28,6 @@ val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast - val eta_contract_default: bool Unsynchronized.ref val eta_contract_raw: Config.raw val mark_bound_abs: string * typ -> term val mark_bound_body: string * typ -> term @@ -303,8 +302,7 @@ | t' => Abs (a, T, t')) | eta_abs t = t; -val eta_contract_default = Unsynchronized.ref true; -val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default)); +val eta_contract_raw = Config.declare_option "eta_contract"; val eta_contract = Config.bool eta_contract_raw; fun eta_contr ctxt tm = diff -r a354c83dee43 -r 16c4e428a1d4 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu May 16 21:55:12 2013 +0200 +++ b/src/Pure/Thy/thy_output.ML Thu May 16 22:02:01 2013 +0200 @@ -6,16 +6,12 @@ signature THY_OUTPUT = sig - val display_default: bool Unsynchronized.ref - val quotes_default: bool Unsynchronized.ref - val indent_default: int Unsynchronized.ref - val source_default: bool Unsynchronized.ref - val break_default: bool Unsynchronized.ref val display: bool Config.T val quotes: bool Config.T val indent: int Config.T val source: bool Config.T val break: bool Config.T + val modes: string Config.T val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory val intern_command: theory -> xstring -> string @@ -29,7 +25,6 @@ val boolean: string -> bool val integer: string -> int datatype markup = Markup | MarkupEnv | Verbatim - val modes: string list Unsynchronized.ref val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit @@ -48,19 +43,14 @@ structure Thy_Output: THY_OUTPUT = struct -(** global options **) +(** options **) -val display_default = Unsynchronized.ref false; -val quotes_default = Unsynchronized.ref false; -val indent_default = Unsynchronized.ref 0; -val source_default = Unsynchronized.ref false; -val break_default = Unsynchronized.ref false; - -val display = Attrib.setup_config_bool (Binding.name "thy_output_display") (fn _ => ! display_default); -val quotes = Attrib.setup_config_bool (Binding.name "thy_output_quotes") (fn _ => ! quotes_default); -val indent = Attrib.setup_config_int (Binding.name "thy_output_indent") (fn _ => ! indent_default); -val source = Attrib.setup_config_bool (Binding.name "thy_output_source") (fn _ => ! source_default); -val break = Attrib.setup_config_bool (Binding.name "thy_output_break") (fn _ => ! break_default); +val display = Attrib.setup_option_bool "thy_output_display"; +val break = Attrib.setup_option_bool "thy_output_break"; +val quotes = Attrib.setup_option_bool "thy_output_quotes"; +val indent = Attrib.setup_option_int "thy_output_indent"; +val source = Attrib.setup_option_bool "thy_output_source"; +val modes = Attrib.setup_option_string "thy_output_modes"; structure Wrappers = Proof_Data @@ -179,8 +169,6 @@ (* eval_antiquote *) -val modes = Unsynchronized.ref ([]: string list); - fun eval_antiq lex state (ss, (pos, _)) = let val (opts, src) = Token.read_antiq lex antiq (ss, pos); @@ -188,7 +176,8 @@ val preview_ctxt = fold option opts (Toplevel.presentation_context_of state); val print_ctxt = Context_Position.set_visible false preview_ctxt; val _ = cmd preview_ctxt; - in Print_Mode.with_modes (! modes @ Latex.modes) (fn () => cmd print_ctxt) () end; + val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes; + in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end; fun eval_antiquote lex state (txt, pos) = let diff -r a354c83dee43 -r 16c4e428a1d4 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Thu May 16 21:55:12 2013 +0200 +++ b/src/Pure/Tools/build.ML Thu May 16 22:02:01 2013 +0200 @@ -93,11 +93,6 @@ |> no_document options ? Present.no_document |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty") |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs") - |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display") - |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes") - |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent") - |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source") - |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break") |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin") |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing"); diff -r a354c83dee43 -r 16c4e428a1d4 src/Pure/Tools/proof_general_pure.ML --- a/src/Pure/Tools/proof_general_pure.ML Thu May 16 21:55:12 2013 +0200 +++ b/src/Pure/Tools/proof_general_pure.ML Thu May 16 22:02:01 2013 +0200 @@ -8,23 +8,23 @@ (* display *) val _ = - ProofGeneral.preference_bool ProofGeneral.category_display + ProofGeneral.preference_option ProofGeneral.category_display NONE - Printer.show_types_default + @{option show_types} "show-types" "Include types in display of Isabelle terms"; val _ = - ProofGeneral.preference_bool ProofGeneral.category_display + ProofGeneral.preference_option ProofGeneral.category_display NONE - Printer.show_sorts_default + @{option show_sorts} "show-sorts" - "Include sorts in display of Isabelle terms"; + "Include sorts in display of Isabelle types"; val _ = - ProofGeneral.preference_bool ProofGeneral.category_display + ProofGeneral.preference_option ProofGeneral.category_display NONE - Goal_Display.show_consts_default + @{option show_consts} "show-consts" "Show types of consts in Isabelle goal display"; @@ -36,23 +36,23 @@ "Show fully qualified names in Isabelle terms"; val _ = - ProofGeneral.preference_bool ProofGeneral.category_display + ProofGeneral.preference_option ProofGeneral.category_display NONE - Printer.show_brackets_default + @{option show_brackets} "show-brackets" "Show full bracketing in Isabelle terms"; val _ = - ProofGeneral.preference_bool ProofGeneral.category_display + ProofGeneral.preference_option ProofGeneral.category_display NONE - Goal_Display.show_main_goal_default + @{option show_main_goal} "show-main-goal" "Show main goal in proof state display"; val _ = - ProofGeneral.preference_bool ProofGeneral.category_display + ProofGeneral.preference_option ProofGeneral.category_display NONE - Syntax_Trans.eta_contract_default + @{option eta_contract} "eta-contract" "Print terms eta-contracted"; diff -r a354c83dee43 -r 16c4e428a1d4 src/Pure/config.ML --- a/src/Pure/config.ML Thu May 16 21:55:12 2013 +0200 +++ b/src/Pure/config.ML Thu May 16 22:02:01 2013 +0200 @@ -24,7 +24,6 @@ val get_generic: Context.generic -> 'a T -> 'a val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic val put_generic: 'a T -> 'a -> Context.generic -> Context.generic - val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> raw val declare_global: string -> (Context.generic -> value) -> raw val declare: string -> (Context.generic -> value) -> raw val declare_option: string -> raw @@ -110,7 +109,7 @@ fun merge data = Inttab.merge (K true) data; ); -fun declare_generic {global} name default = +fun declare_generic global name default = let val id = serial (); @@ -136,8 +135,8 @@ | map_value f context = update_value f context; in Config {name = name, get_value = get_value, map_value = map_value} end; -val declare_global = declare_generic {global = true}; -val declare = declare_generic {global = false}; +val declare_global = declare_generic true; +val declare = declare_generic false; fun declare_option name = let diff -r a354c83dee43 -r 16c4e428a1d4 src/Pure/display.ML --- a/src/Pure/display.ML Thu May 16 21:55:12 2013 +0200 +++ b/src/Pure/display.ML Thu May 16 22:02:01 2013 +0200 @@ -7,7 +7,6 @@ signature BASIC_DISPLAY = sig - val show_consts_default: bool Unsynchronized.ref val show_consts: bool Config.T val show_hyps_raw: Config.raw val show_hyps: bool Config.T @@ -34,7 +33,6 @@ (** options **) -val show_consts_default = Goal_Display.show_consts_default; val show_consts = Goal_Display.show_consts; val show_hyps_raw = Config.declare "show_hyps" (fn _ => Config.Bool false); diff -r a354c83dee43 -r 16c4e428a1d4 src/Pure/goal_display.ML --- a/src/Pure/goal_display.ML Thu May 16 21:55:12 2013 +0200 +++ b/src/Pure/goal_display.ML Thu May 16 22:02:01 2013 +0200 @@ -9,10 +9,8 @@ sig val goals_limit_raw: Config.raw val goals_limit: int Config.T - val show_main_goal_default: bool Unsynchronized.ref val show_main_goal_raw: Config.raw val show_main_goal: bool Config.T - val show_consts_default: bool Unsynchronized.ref val show_consts_raw: Config.raw val show_consts: bool Config.T val pretty_flexpair: Proof.context -> term * term -> Pretty.T @@ -28,13 +26,10 @@ val goals_limit_raw = Config.declare_option "goals_limit"; val goals_limit = Config.int goals_limit_raw; -val show_main_goal_default = Unsynchronized.ref false; -val show_main_goal_raw = - Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default)); +val show_main_goal_raw = Config.declare_option "show_main_goal"; val show_main_goal = Config.bool show_main_goal_raw; -val show_consts_default = Unsynchronized.ref false; -val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default)); +val show_consts_raw = Config.declare_option "show_consts"; val show_consts = Config.bool show_consts_raw; fun pretty_flexpair ctxt (t, u) = Pretty.block