pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
authorwenzelm
Fri Sep 03 21:13:53 2010 +0200 (2010-09-03)
changeset 39125f45d332a90e3
parent 39124 9bac2f4cfd6e
child 39126 ee117c5b3b75
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
NEWS
src/HOL/Prolog/prolog.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/proof.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/Thy/thy_output.ML
src/Pure/display.ML
src/Pure/goal.ML
src/Pure/goal_display.ML
src/Pure/tactical.ML
     1.1 --- a/NEWS	Fri Sep 03 20:39:38 2010 +0200
     1.2 +++ b/NEWS	Fri Sep 03 21:13:53 2010 +0200
     1.3 @@ -28,18 +28,21 @@
     1.4  unsynchronized references.  There are both ML Config.T entities and
     1.5  Isar declaration attributes to access these.
     1.6  
     1.7 -  ML:                       Isar:
     1.8 -
     1.9 -  Thy_Output.display        thy_output_display
    1.10 -  Thy_Output.quotes         thy_output_quotes
    1.11 -  Thy_Output.indent         thy_output_indent
    1.12 -  Thy_Output.source         thy_output_source
    1.13 -  Thy_Output.break          thy_output_break
    1.14 -
    1.15 -  show_question_marks       show_question_marks
    1.16 -  show_consts               show_consts
    1.17 -
    1.18 -Note that the corresponding "..._default" references in ML may be only
    1.19 +  ML (Config.T)                 Isar (attribute)
    1.20 +
    1.21 +  Thy_Output.display            thy_output_display
    1.22 +  Thy_Output.quotes             thy_output_quotes
    1.23 +  Thy_Output.indent             thy_output_indent
    1.24 +  Thy_Output.source             thy_output_source
    1.25 +  Thy_Output.break              thy_output_break
    1.26 +
    1.27 +  show_question_marks           show_question_marks
    1.28 +  show_consts                   show_consts
    1.29 +
    1.30 +  Goal_Display.goals_limit      goals_limit
    1.31 +  Goal_Display.show_main_goal   show_main_goal
    1.32 +
    1.33 +Note that corresponding "..._default" references in ML may be only
    1.34  changed globally at the ROOT session setup, but *not* within a theory.
    1.35  
    1.36  
     2.1 --- a/src/HOL/Prolog/prolog.ML	Fri Sep 03 20:39:38 2010 +0200
     2.2 +++ b/src/HOL/Prolog/prolog.ML	Fri Sep 03 21:13:53 2010 +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 -Proof.show_main_goal := true;
     2.8 +Goal_Display.show_main_goal_default := true;
     2.9  
    2.10  structure Prolog =
    2.11  struct
     3.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Sep 03 20:39:38 2010 +0200
     3.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Sep 03 21:13:53 2010 +0200
     3.3 @@ -135,7 +135,8 @@
     3.4  (** Error reporting **)
     3.5  
     3.6  fun pr_goals ctxt st =
     3.7 -  Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
     3.8 +  Goal_Display.pretty_goals
     3.9 +    (Config.put Goal_Display.goals_limit (Thm.nprems_of st) ctxt) st
    3.10    |> Pretty.chunks
    3.11    |> Pretty.string_of
    3.12  
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 03 20:39:38 2010 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 03 21:13:53 2010 +0200
     4.3 @@ -97,7 +97,7 @@
     4.4    if (nprems_of st <= i) then Seq.single st
     4.5    else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :"
     4.6      ^ "\n" ^ Pretty.string_of (Pretty.chunks
     4.7 -      (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
     4.8 +      (Goal_Display.pretty_goals_without_context st)));
     4.9  
    4.10  (** fundamentals **)
    4.11  
     5.1 --- a/src/Pure/Isar/attrib.ML	Fri Sep 03 20:39:38 2010 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 21:13:53 2010 +0200
     5.3 @@ -393,6 +393,8 @@
     5.4  
     5.5  val _ = Context.>> (Context.map_theory
     5.6   (register_config Syntax.show_question_marks_value #>
     5.7 +  register_config Goal_Display.goals_limit_value #>
     5.8 +  register_config Goal_Display.show_main_goal_value #>
     5.9    register_config Goal_Display.show_consts_value #>
    5.10    register_config Unify.trace_bound_value #>
    5.11    register_config Unify.search_bound_value #>
     6.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Sep 03 20:39:38 2010 +0200
     6.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Sep 03 21:13:53 2010 +0200
     6.3 @@ -272,8 +272,10 @@
     6.4    | set_limit r (SOME n) = r := n;
     6.5  
     6.6  fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
     6.7 -  (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
     6.8 -    Print_Mode.with_modes modes (Toplevel.print_state true) state));
     6.9 + (set_limit Goal_Display.goals_limit_default lim1;
    6.10 +  set_limit ProofContext.prems_limit lim2;
    6.11 +  Toplevel.quiet := false;
    6.12 +  Print_Mode.with_modes modes (Toplevel.print_state true) state));
    6.13  
    6.14  val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
    6.15  val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
     7.1 --- a/src/Pure/Isar/proof.ML	Fri Sep 03 20:39:38 2010 +0200
     7.2 +++ b/src/Pure/Isar/proof.ML	Fri Sep 03 21:13:53 2010 +0200
     7.3 @@ -30,7 +30,6 @@
     7.4    val assert_no_chain: state -> state
     7.5    val enter_forward: state -> state
     7.6    val goal_message: (unit -> Pretty.T) -> state -> state
     7.7 -  val show_main_goal: bool Unsynchronized.ref
     7.8    val verbose: bool Unsynchronized.ref
     7.9    val pretty_state: int -> state -> Pretty.T list
    7.10    val pretty_goals: bool -> state -> Pretty.T list
    7.11 @@ -322,7 +321,6 @@
    7.12  
    7.13  (** pretty_state **)
    7.14  
    7.15 -val show_main_goal = Unsynchronized.ref false;
    7.16  val verbose = ProofContext.verbose;
    7.17  
    7.18  fun pretty_facts _ _ NONE = []
    7.19 @@ -351,8 +349,7 @@
    7.20              (if mode <> Backward orelse null using then NONE else SOME using) @
    7.21            [Pretty.str ("goal" ^
    7.22              description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
    7.23 -          Goal_Display.pretty_goals ctxt
    7.24 -            {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @
    7.25 +          Goal_Display.pretty_goals ctxt goal @
    7.26            (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
    7.27        | prt_goal NONE = [];
    7.28  
    7.29 @@ -372,10 +369,12 @@
    7.30    end;
    7.31  
    7.32  fun pretty_goals main state =
    7.33 -  let val (ctxt, (_, goal)) = get_goal state in
    7.34 -    Goal_Display.pretty_goals ctxt
    7.35 -      {total = false, main = main, maxgoals = ! Display.goals_limit} goal
    7.36 -  end;
    7.37 +  let
    7.38 +    val (ctxt, (_, goal)) = get_goal state;
    7.39 +    val ctxt' = ctxt
    7.40 +      |> Config.put Goal_Display.show_main_goal main
    7.41 +      |> Config.put Goal_Display.goals_total false;
    7.42 +  in Goal_Display.pretty_goals ctxt' goal end;
    7.43  
    7.44  
    7.45  
    7.46 @@ -478,8 +477,7 @@
    7.47  
    7.48      val ngoals = Thm.nprems_of goal;
    7.49      val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
    7.50 -      (Goal_Display.pretty_goals ctxt
    7.51 -          {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @
    7.52 +      (Goal_Display.pretty_goals ctxt goal @
    7.53          [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
    7.54  
    7.55      val extra_hyps = Assumption.extra_hyps ctxt goal;
     8.1 --- a/src/Pure/ProofGeneral/preferences.ML	Fri Sep 03 20:39:38 2010 +0200
     8.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Fri Sep 03 21:13:53 2010 +0200
     8.3 @@ -126,7 +126,7 @@
     8.4    bool_pref show_brackets
     8.5      "show-brackets"
     8.6      "Show full bracketing in Isabelle terms",
     8.7 -  bool_pref Proof.show_main_goal
     8.8 +  bool_pref Goal_Display.show_main_goal_default
     8.9      "show-main-goal"
    8.10      "Show main goal in proof state display",
    8.11    bool_pref Syntax.eta_contract
    8.12 @@ -134,7 +134,7 @@
    8.13      "Print terms eta-contracted"];
    8.14  
    8.15  val advanced_display_preferences =
    8.16 - [nat_pref goals_limit
    8.17 + [nat_pref Goal_Display.goals_limit_default
    8.18      "goals-limit"
    8.19      "Setting for maximum number of goals printed",
    8.20    int_pref ProofContext.prems_limit
     9.1 --- a/src/Pure/Thy/thy_output.ML	Fri Sep 03 20:39:38 2010 +0200
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Sep 03 21:13:53 2010 +0200
     9.3 @@ -459,7 +459,7 @@
     9.4  val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
     9.5  val _ = add_option "indent" (Config.put indent o integer);
     9.6  val _ = add_option "source" (Config.put source o boolean);
     9.7 -val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer);
     9.8 +val _ = add_option "goals_limit" (Config.put Goal_Display.goals_limit o integer);
     9.9  
    9.10  
    9.11  (* basic pretty printing *)
    9.12 @@ -582,7 +582,7 @@
    9.13    | _ => error "No proof state");
    9.14  
    9.15  fun goal_state name main_goal = antiquotation name (Scan.succeed ())
    9.16 -  (fn {state, context, ...} => fn () => output context
    9.17 +  (fn {state, context = ctxt, ...} => fn () => output ctxt
    9.18      [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
    9.19  
    9.20  in
    10.1 --- a/src/Pure/display.ML	Fri Sep 03 20:39:38 2010 +0200
    10.2 +++ b/src/Pure/display.ML	Fri Sep 03 21:13:53 2010 +0200
    10.3 @@ -7,7 +7,6 @@
    10.4  
    10.5  signature BASIC_DISPLAY =
    10.6  sig
    10.7 -  val goals_limit: int Unsynchronized.ref
    10.8    val show_consts_default: bool Unsynchronized.ref
    10.9    val show_consts: bool Config.T
   10.10    val show_hyps: bool Unsynchronized.ref
   10.11 @@ -37,7 +36,6 @@
   10.12  
   10.13  (** options **)
   10.14  
   10.15 -val goals_limit = Goal_Display.goals_limit;
   10.16  val show_consts_default = Goal_Display.show_consts_default;
   10.17  val show_consts = Goal_Display.show_consts;
   10.18  
    11.1 --- a/src/Pure/goal.ML	Fri Sep 03 20:39:38 2010 +0200
    11.2 +++ b/src/Pure/goal.ML	Fri Sep 03 21:13:53 2010 +0200
    11.3 @@ -83,7 +83,10 @@
    11.4      0 => ()
    11.5    | n => raise THM ("Proof failed.\n" ^
    11.6        Pretty.string_of (Pretty.chunks
    11.7 -        (Goal_Display.pretty_goals ctxt {total = true, main = true, maxgoals = n} th)) ^
    11.8 +        (Goal_Display.pretty_goals
    11.9 +          (ctxt
   11.10 +            |> Config.put Goal_Display.goals_limit n
   11.11 +            |> Config.put Goal_Display.show_main_goal true) th)) ^
   11.12        "\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th]));
   11.13  
   11.14  fun finish ctxt th = (check_finished ctxt th; conclude th);
    12.1 --- a/src/Pure/goal_display.ML	Fri Sep 03 20:39:38 2010 +0200
    12.2 +++ b/src/Pure/goal_display.ML	Fri Sep 03 21:13:53 2010 +0200
    12.3 @@ -7,22 +7,35 @@
    12.4  
    12.5  signature GOAL_DISPLAY =
    12.6  sig
    12.7 -  val goals_limit: int Unsynchronized.ref
    12.8 +  val goals_limit_default: int Unsynchronized.ref
    12.9 +  val goals_limit_value: Config.value Config.T
   12.10 +  val goals_limit: int Config.T
   12.11 +  val goals_total: bool Config.T
   12.12 +  val show_main_goal_default: bool Unsynchronized.ref
   12.13 +  val show_main_goal_value: Config.value Config.T
   12.14 +  val show_main_goal: bool Config.T
   12.15    val show_consts_default: bool Unsynchronized.ref
   12.16    val show_consts_value: Config.value Config.T
   12.17    val show_consts: bool Config.T
   12.18    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   12.19 -  val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
   12.20 -    thm -> Pretty.T list
   12.21 -  val pretty_goals_without_context: int -> thm -> Pretty.T list
   12.22 +  val pretty_goals: Proof.context -> thm -> Pretty.T list
   12.23 +  val pretty_goals_without_context: thm -> Pretty.T list
   12.24  end;
   12.25  
   12.26  structure Goal_Display: GOAL_DISPLAY =
   12.27  struct
   12.28  
   12.29 -val goals_limit = Unsynchronized.ref 10;     (*max number of goals to print*)
   12.30 +val goals_limit_default = Unsynchronized.ref 10;
   12.31 +val goals_limit_value = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
   12.32 +val goals_limit = Config.int goals_limit_value;
   12.33 +
   12.34 +val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
   12.35  
   12.36 -(*true: show consts with types in proof state output*)
   12.37 +val show_main_goal_default = Unsynchronized.ref false;
   12.38 +val show_main_goal_value =
   12.39 +  Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
   12.40 +val show_main_goal = Config.bool show_main_goal_value;
   12.41 +
   12.42  val show_consts_default = Unsynchronized.ref false;
   12.43  val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
   12.44  val show_consts = Config.bool show_consts_value;
   12.45 @@ -62,10 +75,14 @@
   12.46  
   12.47  in
   12.48  
   12.49 -fun pretty_goals ctxt0 {total, main, maxgoals} state =
   12.50 +fun pretty_goals ctxt0 state =
   12.51    let
   12.52      val ctxt = Config.put show_free_types false ctxt0;
   12.53 +
   12.54      val show_all_types = Config.get ctxt show_all_types;
   12.55 +    val goals_limit = Config.get ctxt goals_limit;
   12.56 +    val goals_total = Config.get ctxt goals_total;
   12.57 +    val show_main_goal = Config.get ctxt show_main_goal;
   12.58  
   12.59      val prt_sort = Syntax.pretty_sort ctxt;
   12.60      val prt_typ = Syntax.pretty_typ ctxt;
   12.61 @@ -105,11 +122,11 @@
   12.62      val ngoals = length As;
   12.63  
   12.64      fun pretty_gs (types, sorts) =
   12.65 -      (if main then [prt_term B] else []) @
   12.66 +      (if show_main_goal then [prt_term B] else []) @
   12.67         (if ngoals = 0 then [Pretty.str "No subgoals!"]
   12.68 -        else if ngoals > maxgoals then
   12.69 -          pretty_subgoals (take maxgoals As) @
   12.70 -          (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   12.71 +        else if ngoals > goals_limit then
   12.72 +          pretty_subgoals (take goals_limit As) @
   12.73 +          (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   12.74             else [])
   12.75          else pretty_subgoals As) @
   12.76        pretty_ffpairs tpairs @
   12.77 @@ -122,9 +139,10 @@
   12.78     (! show_types orelse ! show_sorts orelse show_all_types, ! show_sorts)
   12.79    end;
   12.80  
   12.81 -fun pretty_goals_without_context n th =
   12.82 -  pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th))
   12.83 -    {total = true, main = true, maxgoals = n} th;
   12.84 +fun pretty_goals_without_context th =
   12.85 +  let val ctxt =
   12.86 +    Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
   12.87 +  in pretty_goals ctxt th end;
   12.88  
   12.89  end;
   12.90  
    13.1 --- a/src/Pure/tactical.ML	Fri Sep 03 20:39:38 2010 +0200
    13.2 +++ b/src/Pure/tactical.ML	Fri Sep 03 21:13:53 2010 +0200
    13.3 @@ -191,8 +191,7 @@
    13.4  (*Print the current proof state and pass it on.*)
    13.5  fun print_tac msg st =
    13.6   (tracing (msg ^ "\n" ^
    13.7 -    Pretty.string_of (Pretty.chunks
    13.8 -      (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
    13.9 +    Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context st)));
   13.10    Seq.single st);
   13.11  
   13.12  (*Pause until a line is typed -- if non-empty then fail. *)
   13.13 @@ -231,7 +230,7 @@
   13.14  fun tracify flag tac st =
   13.15    if !flag andalso not (!suppress_tracing) then
   13.16      (tracing (Pretty.string_of (Pretty.chunks
   13.17 -        (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st @
   13.18 +        (Goal_Display.pretty_goals_without_context st @
   13.19            [Pretty.str "** Press RETURN to continue:"])));
   13.20       exec_trace_command flag (tac, st))
   13.21    else tac st;