more system options as context-sensitive config options;
authorwenzelm
Thu May 16 21:48:01 2013 +0200 (2013-05-16)
changeset 52043286629271d65
parent 52042 aae07a3ff536
child 52044 16c4e428a1d4
more system options as context-sensitive config options;
etc/options
src/HOL/Prolog/prolog.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax_trans.ML
src/Pure/Tools/proof_general_pure.ML
src/Pure/display.ML
src/Pure/goal_display.ML
     1.1 --- a/etc/options	Thu May 16 21:09:58 2013 +0200
     1.2 +++ b/etc/options	Thu May 16 21:48:01 2013 +0200
     1.3 @@ -14,22 +14,6 @@
     1.4  option document_graph : bool = false
     1.5    -- "generate session graph image for document"
     1.6  
     1.7 -option goals_limit : int = 10
     1.8 -  -- "maximum number of subgoals to be printed"
     1.9 -
    1.10 -option show_question_marks : bool = true
    1.11 -  -- "show leading question mark of schematic variables"
    1.12 -
    1.13 -option names_long : bool = false
    1.14 -  -- "show fully qualified names"
    1.15 -option names_short : bool = false
    1.16 -  -- "show base names only"
    1.17 -option names_unique : bool = true
    1.18 -  -- "show partially qualified names, as required for unique name resolution"
    1.19 -
    1.20 -option pretty_margin : int = 76
    1.21 -  -- "right margin / page width of pretty printer in Isabelle/ML"
    1.22 -
    1.23  option thy_output_display : bool = false
    1.24    -- "indicate output as multi-line display-style material"
    1.25  option thy_output_break : bool = false
    1.26 @@ -43,6 +27,38 @@
    1.27  option thy_output_modes : string = ""
    1.28    -- "additional print modes for document output (separated by commas)"
    1.29  
    1.30 +
    1.31 +section "Prover Output"
    1.32 +
    1.33 +option show_types : bool = false
    1.34 +  -- "show type constraints when printing terms"
    1.35 +option show_sorts : bool = false
    1.36 +  -- "show sort constraints when printing types"
    1.37 +option show_brackets : bool = false
    1.38 +  -- "show extra brackets when printing terms/types"
    1.39 +option show_question_marks : bool = true
    1.40 +  -- "show leading question mark of schematic variables"
    1.41 +
    1.42 +option show_consts : bool = false
    1.43 +  -- "show constants with types when printing proof state"
    1.44 +option show_main_goal : bool = false
    1.45 +  -- "show main goal when printing proof state"
    1.46 +option goals_limit : int = 10
    1.47 +  -- "maximum number of subgoals to be printed"
    1.48 +
    1.49 +option names_long : bool = false
    1.50 +  -- "show fully qualified names"
    1.51 +option names_short : bool = false
    1.52 +  -- "show base names only"
    1.53 +option names_unique : bool = true
    1.54 +  -- "show partially qualified names, as required for unique name resolution"
    1.55 +
    1.56 +option eta_contract : bool = true
    1.57 +  -- "print terms in eta-contracted form"
    1.58 +
    1.59 +option pretty_margin : int = 76
    1.60 +  -- "right margin / page width of pretty printer in Isabelle/ML"
    1.61 +
    1.62  option print_mode : string = ""
    1.63    -- "additional print modes for prover output (separated by commas)"
    1.64  
     2.1 --- a/src/HOL/Prolog/prolog.ML	Thu May 16 21:09:58 2013 +0200
     2.2 +++ b/src/HOL/Prolog/prolog.ML	Thu May 16 21:48:01 2013 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     2.5  *)
     2.6  
     2.7 -Goal_Display.show_main_goal_default := true;
     2.8 +Options.default_put_bool @{option show_main_goal} true;
     2.9  
    2.10  structure Prolog =
    2.11  struct
     3.1 --- a/src/Pure/Syntax/printer.ML	Thu May 16 21:09:58 2013 +0200
     3.2 +++ b/src/Pure/Syntax/printer.ML	Thu May 16 21:48:01 2013 +0200
     3.3 @@ -20,11 +20,8 @@
     3.4  signature PRINTER =
     3.5  sig
     3.6    include BASIC_PRINTER
     3.7 -  val show_brackets_default: bool Unsynchronized.ref
     3.8    val show_brackets_raw: Config.raw
     3.9 -  val show_types_default: bool Unsynchronized.ref
    3.10    val show_types_raw: Config.raw
    3.11 -  val show_sorts_default: bool Unsynchronized.ref
    3.12    val show_sorts_raw: Config.raw
    3.13    val show_markup_default: bool Unsynchronized.ref
    3.14    val show_markup_raw: Config.raw
    3.15 @@ -53,17 +50,13 @@
    3.16  
    3.17  (** options for printing **)
    3.18  
    3.19 -val show_brackets_default = Unsynchronized.ref false;
    3.20 -val show_brackets_raw =
    3.21 -  Config.declare "show_brackets" (fn _ => Config.Bool (! show_brackets_default));
    3.22 +val show_brackets_raw = Config.declare_option "show_brackets";
    3.23  val show_brackets = Config.bool show_brackets_raw;
    3.24  
    3.25 -val show_types_default = Unsynchronized.ref false;
    3.26 -val show_types_raw = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default));
    3.27 +val show_types_raw = Config.declare_option "show_types";
    3.28  val show_types = Config.bool show_types_raw;
    3.29  
    3.30 -val show_sorts_default = Unsynchronized.ref false;
    3.31 -val show_sorts_raw = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
    3.32 +val show_sorts_raw = Config.declare_option "show_sorts";
    3.33  val show_sorts = Config.bool show_sorts_raw;
    3.34  
    3.35  val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
     4.1 --- a/src/Pure/Syntax/syntax_trans.ML	Thu May 16 21:09:58 2013 +0200
     4.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Thu May 16 21:48:01 2013 +0200
     4.3 @@ -28,7 +28,6 @@
     4.4    val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
     4.5    val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
     4.6    val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
     4.7 -  val eta_contract_default: bool Unsynchronized.ref
     4.8    val eta_contract_raw: Config.raw
     4.9    val mark_bound_abs: string * typ -> term
    4.10    val mark_bound_body: string * typ -> term
    4.11 @@ -303,8 +302,7 @@
    4.12        | t' => Abs (a, T, t'))
    4.13    | eta_abs t = t;
    4.14  
    4.15 -val eta_contract_default = Unsynchronized.ref true;
    4.16 -val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
    4.17 +val eta_contract_raw = Config.declare_option "eta_contract";
    4.18  val eta_contract = Config.bool eta_contract_raw;
    4.19  
    4.20  fun eta_contr ctxt tm =
     5.1 --- a/src/Pure/Tools/proof_general_pure.ML	Thu May 16 21:09:58 2013 +0200
     5.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Thu May 16 21:48:01 2013 +0200
     5.3 @@ -8,23 +8,23 @@
     5.4  (* display *)
     5.5  
     5.6  val _ =
     5.7 -  ProofGeneral.preference_bool ProofGeneral.category_display
     5.8 +  ProofGeneral.preference_option ProofGeneral.category_display
     5.9      NONE
    5.10 -    Printer.show_types_default
    5.11 +    @{option show_types}
    5.12      "show-types"
    5.13      "Include types in display of Isabelle terms";
    5.14  
    5.15  val _ =
    5.16 -  ProofGeneral.preference_bool ProofGeneral.category_display
    5.17 +  ProofGeneral.preference_option ProofGeneral.category_display
    5.18      NONE
    5.19 -    Printer.show_sorts_default
    5.20 +    @{option show_sorts}
    5.21      "show-sorts"
    5.22 -    "Include sorts in display of Isabelle terms";
    5.23 +    "Include sorts in display of Isabelle types";
    5.24  
    5.25  val _ =
    5.26 -  ProofGeneral.preference_bool ProofGeneral.category_display
    5.27 +  ProofGeneral.preference_option ProofGeneral.category_display
    5.28      NONE
    5.29 -    Goal_Display.show_consts_default
    5.30 +    @{option show_consts}
    5.31      "show-consts"
    5.32      "Show types of consts in Isabelle goal display";
    5.33  
    5.34 @@ -36,23 +36,23 @@
    5.35      "Show fully qualified names in Isabelle terms";
    5.36  
    5.37  val _ =
    5.38 -  ProofGeneral.preference_bool ProofGeneral.category_display
    5.39 +  ProofGeneral.preference_option ProofGeneral.category_display
    5.40      NONE
    5.41 -    Printer.show_brackets_default
    5.42 +    @{option show_brackets}
    5.43      "show-brackets"
    5.44      "Show full bracketing in Isabelle terms";
    5.45  
    5.46  val _ =
    5.47 -  ProofGeneral.preference_bool ProofGeneral.category_display
    5.48 +  ProofGeneral.preference_option ProofGeneral.category_display
    5.49      NONE
    5.50 -    Goal_Display.show_main_goal_default
    5.51 +    @{option show_main_goal}
    5.52      "show-main-goal"
    5.53      "Show main goal in proof state display";
    5.54  
    5.55  val _ =
    5.56 -  ProofGeneral.preference_bool ProofGeneral.category_display
    5.57 +  ProofGeneral.preference_option ProofGeneral.category_display
    5.58      NONE
    5.59 -    Syntax_Trans.eta_contract_default
    5.60 +    @{option eta_contract}
    5.61      "eta-contract"
    5.62      "Print terms eta-contracted";
    5.63  
     6.1 --- a/src/Pure/display.ML	Thu May 16 21:09:58 2013 +0200
     6.2 +++ b/src/Pure/display.ML	Thu May 16 21:48:01 2013 +0200
     6.3 @@ -7,7 +7,6 @@
     6.4  
     6.5  signature BASIC_DISPLAY =
     6.6  sig
     6.7 -  val show_consts_default: bool Unsynchronized.ref
     6.8    val show_consts: bool Config.T
     6.9    val show_hyps_raw: Config.raw
    6.10    val show_hyps: bool Config.T
    6.11 @@ -34,7 +33,6 @@
    6.12  
    6.13  (** options **)
    6.14  
    6.15 -val show_consts_default = Goal_Display.show_consts_default;
    6.16  val show_consts = Goal_Display.show_consts;
    6.17  
    6.18  val show_hyps_raw = Config.declare "show_hyps" (fn _ => Config.Bool false);
     7.1 --- a/src/Pure/goal_display.ML	Thu May 16 21:09:58 2013 +0200
     7.2 +++ b/src/Pure/goal_display.ML	Thu May 16 21:48:01 2013 +0200
     7.3 @@ -9,10 +9,8 @@
     7.4  sig
     7.5    val goals_limit_raw: Config.raw
     7.6    val goals_limit: int Config.T
     7.7 -  val show_main_goal_default: bool Unsynchronized.ref
     7.8    val show_main_goal_raw: Config.raw
     7.9    val show_main_goal: bool Config.T
    7.10 -  val show_consts_default: bool Unsynchronized.ref
    7.11    val show_consts_raw: Config.raw
    7.12    val show_consts: bool Config.T
    7.13    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    7.14 @@ -28,13 +26,10 @@
    7.15  val goals_limit_raw = Config.declare_option "goals_limit";
    7.16  val goals_limit = Config.int goals_limit_raw;
    7.17  
    7.18 -val show_main_goal_default = Unsynchronized.ref false;
    7.19 -val show_main_goal_raw =
    7.20 -  Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
    7.21 +val show_main_goal_raw = Config.declare_option "show_main_goal";
    7.22  val show_main_goal = Config.bool show_main_goal_raw;
    7.23  
    7.24 -val show_consts_default = Unsynchronized.ref false;
    7.25 -val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
    7.26 +val show_consts_raw = Config.declare_option "show_consts";
    7.27  val show_consts = Config.bool show_consts_raw;
    7.28  
    7.29  fun pretty_flexpair ctxt (t, u) = Pretty.block