# HG changeset patch # User wenzelm # Date 1368733681 -7200 # Node ID 286629271d65a1764b95afeda986102fcb9f6d6d # Parent aae07a3ff53686b364c2b93571f1d48fd518bebb more system options as context-sensitive config options; diff -r aae07a3ff536 -r 286629271d65 etc/options --- a/etc/options Thu May 16 21:09:58 2013 +0200 +++ b/etc/options Thu May 16 21:48: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 @@ -43,6 +27,38 @@ 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 aae07a3ff536 -r 286629271d65 src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Thu May 16 21:09:58 2013 +0200 +++ b/src/HOL/Prolog/prolog.ML Thu May 16 21:48: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 aae07a3ff536 -r 286629271d65 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu May 16 21:09:58 2013 +0200 +++ b/src/Pure/Syntax/printer.ML Thu May 16 21:48: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 aae07a3ff536 -r 286629271d65 src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Thu May 16 21:09:58 2013 +0200 +++ b/src/Pure/Syntax/syntax_trans.ML Thu May 16 21:48: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 aae07a3ff536 -r 286629271d65 src/Pure/Tools/proof_general_pure.ML --- a/src/Pure/Tools/proof_general_pure.ML Thu May 16 21:09:58 2013 +0200 +++ b/src/Pure/Tools/proof_general_pure.ML Thu May 16 21:48: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 aae07a3ff536 -r 286629271d65 src/Pure/display.ML --- a/src/Pure/display.ML Thu May 16 21:09:58 2013 +0200 +++ b/src/Pure/display.ML Thu May 16 21:48: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 aae07a3ff536 -r 286629271d65 src/Pure/goal_display.ML --- a/src/Pure/goal_display.ML Thu May 16 21:09:58 2013 +0200 +++ b/src/Pure/goal_display.ML Thu May 16 21:48: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