option "goals_limit", with more uniform description;
authorwenzelm
Mon May 13 13:23:13 2013 +0200 (2013-05-13)
changeset 5196061ac1efe02c3
parent 51959 18d758e38d85
child 51961 4ccc75f17bb7
option "goals_limit", with more uniform description;
etc/options
src/Doc/IsarRef/Document_Preparation.thy
src/Doc/IsarRef/Inner_Syntax.thy
src/Pure/Isar/isar_syn.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/goal_display.ML
     1.1 --- a/etc/options	Mon May 13 13:01:10 2013 +0200
     1.2 +++ b/etc/options	Mon May 13 13:23:13 2013 +0200
     1.3 @@ -14,6 +14,9 @@
     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  
     2.1 --- a/src/Doc/IsarRef/Document_Preparation.thy	Mon May 13 13:01:10 2013 +0200
     2.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy	Mon May 13 13:23:13 2013 +0200
     2.3 @@ -358,7 +358,7 @@
     2.4    or indentation for pretty printing of display material.
     2.5  
     2.6    \item @{antiquotation_option_def goals_limit}~@{text "= nat"}
     2.7 -  determines the maximum number of goals to be printed (for goal-based
     2.8 +  determines the maximum number of subgoals to be printed (for goal-based
     2.9    antiquotation).
    2.10  
    2.11    \item @{antiquotation_option_def source}~@{text "= bool"} prints the
     3.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy	Mon May 13 13:01:10 2013 +0200
     3.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Mon May 13 13:23:13 2013 +0200
     3.3 @@ -213,7 +213,7 @@
     3.4    might look at terms more discretely.
     3.5  
     3.6    \item @{attribute goals_limit} controls the maximum number of
     3.7 -  subgoals to be shown in goal output.
     3.8 +  subgoals to be printed.
     3.9  
    3.10    \item @{attribute show_main_goal} controls whether the main result
    3.11    to be proven should be displayed.  This information might be
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Mon May 13 13:01:10 2013 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon May 13 13:23:13 2013 +0200
     4.3 @@ -975,7 +975,7 @@
     4.4    Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
     4.5      (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
     4.6        Toplevel.keep (fn state =>
     4.7 -       (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
     4.8 +       (case limit of NONE => () | SOME n => Options.default_put_int "goals_limit" n;
     4.9          Toplevel.quiet := false;
    4.10          Print_Mode.with_modes modes (Toplevel.print_state true) state))));
    4.11  
     5.1 --- a/src/Pure/ProofGeneral/preferences.ML	Mon May 13 13:01:10 2013 +0200
     5.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Mon May 13 13:23:13 2013 +0200
     5.3 @@ -159,9 +159,9 @@
     5.4      "Print terms eta-contracted"];
     5.5  
     5.6  val advanced_display_preferences =
     5.7 - [nat_pref Goal_Display.goals_limit_default
     5.8 + [options_pref "goals_limit"
     5.9      "goals-limit"
    5.10 -    "Setting for maximum number of goals printed",
    5.11 +    "Setting for maximum number of subgoals to be printed",
    5.12    print_depth_pref,
    5.13    options_pref "show_question_marks"
    5.14      "show-question-marks"
     6.1 --- a/src/Pure/goal_display.ML	Mon May 13 13:01:10 2013 +0200
     6.2 +++ b/src/Pure/goal_display.ML	Mon May 13 13:23:13 2013 +0200
     6.3 @@ -7,7 +7,6 @@
     6.4  
     6.5  signature GOAL_DISPLAY =
     6.6  sig
     6.7 -  val goals_limit_default: int Unsynchronized.ref
     6.8    val goals_limit_raw: Config.raw
     6.9    val goals_limit: int Config.T
    6.10    val show_main_goal_default: bool Unsynchronized.ref
    6.11 @@ -26,8 +25,7 @@
    6.12  structure Goal_Display: GOAL_DISPLAY =
    6.13  struct
    6.14  
    6.15 -val goals_limit_default = Unsynchronized.ref 10;
    6.16 -val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
    6.17 +val goals_limit_raw = Config.declare_option "goals_limit";
    6.18  val goals_limit = Config.int goals_limit_raw;
    6.19  
    6.20  val show_main_goal_default = Unsynchronized.ref false;