retain goal display options when printing error messages, to avoid breakdown for huge goals;
authorwenzelm
Mon May 13 12:40:17 2013 +0200 (2013-05-13)
changeset 51958bca32217b304
parent 51953 ae755fd6c883
child 51959 18d758e38d85
retain goal display options when printing error messages, to avoid breakdown for huge goals;
src/HOL/Tools/Function/lexicographic_order.ML
src/Pure/Isar/proof_display.ML
src/Pure/Thy/thy_output.ML
src/Pure/goal.ML
src/Pure/goal_display.ML
     1.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon May 13 06:50:37 2013 +0200
     1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon May 13 12:40:17 2013 +0200
     1.3 @@ -120,22 +120,21 @@
     1.4  
     1.5  (** Error reporting **)
     1.6  
     1.7 -fun pr_goals ctxt st =
     1.8 -  Pretty.string_of
     1.9 -    (Goal_Display.pretty_goal
    1.10 -      {main = Config.get ctxt Goal_Display.show_main_goal, limit = false} ctxt st)
    1.11 -
    1.12  fun row_index i = chr (i + 97)  (* FIXME not scalable wrt. chr range *)
    1.13  fun col_index j = string_of_int (j + 1)  (* FIXME not scalable wrt. table layout *)
    1.14  
    1.15  fun pr_unprovable_cell _ ((i,j), Less _) = []
    1.16    | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
    1.17 -      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
    1.18 +      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
    1.19 +       Goal_Display.string_of_goal ctxt st]
    1.20    | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
    1.21 -      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less ^
    1.22 -       "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq]
    1.23 +      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
    1.24 +       Goal_Display.string_of_goal ctxt st_less ^
    1.25 +       "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^
    1.26 +       Goal_Display.string_of_goal ctxt st_leq]
    1.27    | pr_unprovable_cell ctxt ((i,j), False st) =
    1.28 -      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
    1.29 +      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
    1.30 +       Goal_Display.string_of_goal ctxt st]
    1.31  
    1.32  fun pr_unprovable_subgoals ctxt table =
    1.33    table
     2.1 --- a/src/Pure/Isar/proof_display.ML	Mon May 13 06:50:37 2013 +0200
     2.2 +++ b/src/Pure/Isar/proof_display.ML	Mon May 13 12:40:17 2013 +0200
     2.3 @@ -105,8 +105,7 @@
     2.4  end;
     2.5  
     2.6  fun string_of_goal ctxt goal =
     2.7 -  Pretty.string_of (Pretty.chunks
     2.8 -    [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]);
     2.9 +  Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
    2.10  
    2.11  
    2.12  (* goal facts *)
     3.1 --- a/src/Pure/Thy/thy_output.ML	Mon May 13 06:50:37 2013 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Mon May 13 12:40:17 2013 +0200
     3.3 @@ -612,7 +612,8 @@
     3.4  
     3.5  fun goal_state name main = antiquotation name (Scan.succeed ())
     3.6    (fn {state, context = ctxt, ...} => fn () => output ctxt
     3.7 -    [Goal_Display.pretty_goal {main = main, limit = true} ctxt (proof_state state)]);
     3.8 +    [Goal_Display.pretty_goal
     3.9 +      (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
    3.10  
    3.11  in
    3.12  
     4.1 --- a/src/Pure/goal.ML	Mon May 13 06:50:37 2013 +0200
     4.2 +++ b/src/Pure/goal.ML	Mon May 13 12:40:17 2013 +0200
     4.3 @@ -97,8 +97,7 @@
     4.4  fun check_finished ctxt th =
     4.5    if Thm.no_prems th then th
     4.6    else
     4.7 -    raise THM ("Proof failed.\n" ^
     4.8 -      Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]);
     4.9 +    raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]);
    4.10  
    4.11  fun finish ctxt = check_finished ctxt #> conclude;
    4.12  
     5.1 --- a/src/Pure/goal_display.ML	Mon May 13 06:50:37 2013 +0200
     5.2 +++ b/src/Pure/goal_display.ML	Mon May 13 12:40:17 2013 +0200
     5.3 @@ -20,7 +20,8 @@
     5.4    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
     5.5    val pretty_goals: Proof.context -> thm -> Pretty.T list
     5.6    val pretty_goals_without_context: thm -> Pretty.T list
     5.7 -  val pretty_goal: {main: bool, limit: bool} -> Proof.context -> thm -> Pretty.T
     5.8 +  val pretty_goal: Proof.context -> thm -> Pretty.T
     5.9 +  val string_of_goal: Proof.context -> thm -> string
    5.10  end;
    5.11  
    5.12  structure Goal_Display: GOAL_DISPLAY =
    5.13 @@ -148,12 +149,10 @@
    5.14      Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
    5.15    in pretty_goals ctxt th end;
    5.16  
    5.17 -fun pretty_goal {main, limit} ctxt th =
    5.18 -  Pretty.chunks (pretty_goals
    5.19 -    (ctxt
    5.20 -      |> Config.put show_main_goal main
    5.21 -      |> not limit ? Config.put goals_limit (Thm.nprems_of th)
    5.22 -      |> Config.put goals_total false) th);
    5.23 +fun pretty_goal ctxt th =
    5.24 +  Pretty.chunks (pretty_goals (Config.put goals_total false ctxt) th);
    5.25 +
    5.26 +val string_of_goal = Pretty.string_of oo pretty_goal;
    5.27  
    5.28  end;
    5.29