merged
authorwenzelm
Mon May 13 16:40:59 2013 +0200 (2013-05-13)
changeset 519614ccc75f17bb7
parent 51957 68c163598f07
parent 51960 61ac1efe02c3
child 51962 016cb7d8f297
merged
     1.1 --- a/etc/options	Mon May 13 15:22:19 2013 +0200
     1.2 +++ b/etc/options	Mon May 13 16:40:59 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 15:22:19 2013 +0200
     2.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy	Mon May 13 16:40:59 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 15:22:19 2013 +0200
     3.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Mon May 13 16:40:59 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/HOL/Tools/Function/lexicographic_order.ML	Mon May 13 15:22:19 2013 +0200
     4.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon May 13 16:40:59 2013 +0200
     4.3 @@ -120,22 +120,21 @@
     4.4  
     4.5  (** Error reporting **)
     4.6  
     4.7 -fun pr_goals ctxt st =
     4.8 -  Pretty.string_of
     4.9 -    (Goal_Display.pretty_goal
    4.10 -      {main = Config.get ctxt Goal_Display.show_main_goal, limit = false} ctxt st)
    4.11 -
    4.12  fun row_index i = chr (i + 97)  (* FIXME not scalable wrt. chr range *)
    4.13  fun col_index j = string_of_int (j + 1)  (* FIXME not scalable wrt. table layout *)
    4.14  
    4.15  fun pr_unprovable_cell _ ((i,j), Less _) = []
    4.16    | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
    4.17 -      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
    4.18 +      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
    4.19 +       Goal_Display.string_of_goal ctxt st]
    4.20    | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
    4.21 -      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less ^
    4.22 -       "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq]
    4.23 +      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
    4.24 +       Goal_Display.string_of_goal ctxt st_less ^
    4.25 +       "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^
    4.26 +       Goal_Display.string_of_goal ctxt st_leq]
    4.27    | pr_unprovable_cell ctxt ((i,j), False st) =
    4.28 -      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
    4.29 +      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
    4.30 +       Goal_Display.string_of_goal ctxt st]
    4.31  
    4.32  fun pr_unprovable_subgoals ctxt table =
    4.33    table
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Mon May 13 15:22:19 2013 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon May 13 16:40:59 2013 +0200
     5.3 @@ -975,7 +975,7 @@
     5.4    Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
     5.5      (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
     5.6        Toplevel.keep (fn state =>
     5.7 -       (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
     5.8 +       (case limit of NONE => () | SOME n => Options.default_put_int "goals_limit" n;
     5.9          Toplevel.quiet := false;
    5.10          Print_Mode.with_modes modes (Toplevel.print_state true) state))));
    5.11  
     6.1 --- a/src/Pure/Isar/proof_display.ML	Mon May 13 15:22:19 2013 +0200
     6.2 +++ b/src/Pure/Isar/proof_display.ML	Mon May 13 16:40:59 2013 +0200
     6.3 @@ -105,8 +105,7 @@
     6.4  end;
     6.5  
     6.6  fun string_of_goal ctxt goal =
     6.7 -  Pretty.string_of (Pretty.chunks
     6.8 -    [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]);
     6.9 +  Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
    6.10  
    6.11  
    6.12  (* goal facts *)
     7.1 --- a/src/Pure/ProofGeneral/preferences.ML	Mon May 13 15:22:19 2013 +0200
     7.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Mon May 13 16:40:59 2013 +0200
     7.3 @@ -159,9 +159,9 @@
     7.4      "Print terms eta-contracted"];
     7.5  
     7.6  val advanced_display_preferences =
     7.7 - [nat_pref Goal_Display.goals_limit_default
     7.8 + [options_pref "goals_limit"
     7.9      "goals-limit"
    7.10 -    "Setting for maximum number of goals printed",
    7.11 +    "Setting for maximum number of subgoals to be printed",
    7.12    print_depth_pref,
    7.13    options_pref "show_question_marks"
    7.14      "show-question-marks"
     8.1 --- a/src/Pure/Thy/thy_output.ML	Mon May 13 15:22:19 2013 +0200
     8.2 +++ b/src/Pure/Thy/thy_output.ML	Mon May 13 16:40:59 2013 +0200
     8.3 @@ -612,7 +612,8 @@
     8.4  
     8.5  fun goal_state name main = antiquotation name (Scan.succeed ())
     8.6    (fn {state, context = ctxt, ...} => fn () => output ctxt
     8.7 -    [Goal_Display.pretty_goal {main = main, limit = true} ctxt (proof_state state)]);
     8.8 +    [Goal_Display.pretty_goal
     8.9 +      (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
    8.10  
    8.11  in
    8.12  
     9.1 --- a/src/Pure/goal.ML	Mon May 13 15:22:19 2013 +0200
     9.2 +++ b/src/Pure/goal.ML	Mon May 13 16:40:59 2013 +0200
     9.3 @@ -97,8 +97,7 @@
     9.4  fun check_finished ctxt th =
     9.5    if Thm.no_prems th then th
     9.6    else
     9.7 -    raise THM ("Proof failed.\n" ^
     9.8 -      Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]);
     9.9 +    raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]);
    9.10  
    9.11  fun finish ctxt = check_finished ctxt #> conclude;
    9.12  
    10.1 --- a/src/Pure/goal_display.ML	Mon May 13 15:22:19 2013 +0200
    10.2 +++ b/src/Pure/goal_display.ML	Mon May 13 16:40:59 2013 +0200
    10.3 @@ -7,10 +7,8 @@
    10.4  
    10.5  signature GOAL_DISPLAY =
    10.6  sig
    10.7 -  val goals_limit_default: int Unsynchronized.ref
    10.8    val goals_limit_raw: Config.raw
    10.9    val goals_limit: int Config.T
   10.10 -  val goals_total: bool Config.T
   10.11    val show_main_goal_default: bool Unsynchronized.ref
   10.12    val show_main_goal_raw: Config.raw
   10.13    val show_main_goal: bool Config.T
   10.14 @@ -20,18 +18,16 @@
   10.15    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   10.16    val pretty_goals: Proof.context -> thm -> Pretty.T list
   10.17    val pretty_goals_without_context: thm -> Pretty.T list
   10.18 -  val pretty_goal: {main: bool, limit: bool} -> Proof.context -> thm -> Pretty.T
   10.19 +  val pretty_goal: Proof.context -> thm -> Pretty.T
   10.20 +  val string_of_goal: Proof.context -> thm -> string
   10.21  end;
   10.22  
   10.23  structure Goal_Display: GOAL_DISPLAY =
   10.24  struct
   10.25  
   10.26 -val goals_limit_default = Unsynchronized.ref 10;
   10.27 -val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
   10.28 +val goals_limit_raw = Config.declare_option "goals_limit";
   10.29  val goals_limit = Config.int goals_limit_raw;
   10.30  
   10.31 -val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
   10.32 -
   10.33  val show_main_goal_default = Unsynchronized.ref false;
   10.34  val show_main_goal_raw =
   10.35    Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
   10.36 @@ -91,7 +87,6 @@
   10.37      val show_consts = Config.get ctxt show_consts
   10.38      val show_main_goal = Config.get ctxt show_main_goal;
   10.39      val goals_limit = Config.get ctxt goals_limit;
   10.40 -    val goals_total = Config.get ctxt goals_total;
   10.41  
   10.42      val prt_sort = Syntax.pretty_sort ctxt;
   10.43      val prt_typ = Syntax.pretty_typ ctxt;
   10.44 @@ -134,8 +129,7 @@
   10.45       (if ngoals = 0 then [Pretty.str "No subgoals!"]
   10.46        else if ngoals > goals_limit then
   10.47          pretty_subgoals (take goals_limit As) @
   10.48 -        (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   10.49 -         else [])
   10.50 +        [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   10.51        else pretty_subgoals As) @
   10.52      pretty_ffpairs tpairs @
   10.53      (if show_consts then pretty_consts prop else []) @
   10.54 @@ -148,12 +142,8 @@
   10.55      Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
   10.56    in pretty_goals ctxt th end;
   10.57  
   10.58 -fun pretty_goal {main, limit} ctxt th =
   10.59 -  Pretty.chunks (pretty_goals
   10.60 -    (ctxt
   10.61 -      |> Config.put show_main_goal main
   10.62 -      |> not limit ? Config.put goals_limit (Thm.nprems_of th)
   10.63 -      |> Config.put goals_total false) th);
   10.64 +val pretty_goal = Pretty.chunks oo pretty_goals;
   10.65 +val string_of_goal = Pretty.string_of oo pretty_goal;
   10.66  
   10.67  end;
   10.68