1.1 --- a/src/Pure/Isar/proof.ML Thu Sep 06 12:30:11 2007 +0200
1.2 +++ b/src/Pure/Isar/proof.ML Thu Sep 06 12:30:41 2007 +0200
1.3 @@ -28,6 +28,7 @@
1.4 val assert_backward: state -> state
1.5 val assert_no_chain: state -> state
1.6 val enter_forward: state -> state
1.7 + val goal_message: (unit -> Pretty.T) -> state -> state
1.8 val get_goal: state -> context * (thm list * thm)
1.9 val schematic_goal: state -> bool
1.10 val show_main_goal: bool ref
1.11 @@ -137,6 +138,7 @@
1.12 and goal =
1.13 Goal of
1.14 {statement: string * term list list, (*goal kind and statement, starting with vars*)
1.15 + messages: (unit -> Pretty.T) list, (*persistent messages (hints etc.)*)
1.16 using: thm list, (*goal facts*)
1.17 goal: thm, (*subgoals ==> statement*)
1.18 before_qed: Method.text option,
1.19 @@ -144,8 +146,8 @@
1.20 (thm list list -> state -> state Seq.seq) *
1.21 (thm list list -> context -> context)};
1.22
1.23 -fun make_goal (statement, using, goal, before_qed, after_qed) =
1.24 - Goal {statement = statement, using = using, goal = goal,
1.25 +fun make_goal (statement, messages, using, goal, before_qed, after_qed) =
1.26 + Goal {statement = statement, messages = messages, using = using, goal = goal,
1.27 before_qed = before_qed, after_qed = after_qed};
1.28
1.29 fun make_node (context, facts, mode, goal) =
1.30 @@ -274,19 +276,22 @@
1.31
1.32 fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) =
1.33 let
1.34 - val Goal {statement, using, goal, before_qed, after_qed} = goal;
1.35 - val goal' = make_goal (g (statement, using, goal, before_qed, after_qed));
1.36 + val Goal {statement, messages, using, goal, before_qed, after_qed} = goal;
1.37 + val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed));
1.38 in State (make_node (f context, facts, mode, SOME goal'), nodes) end
1.39 | map_goal f g (State (nd, node :: nodes)) =
1.40 let val State (node', nodes') = map_goal f g (State (node, nodes))
1.41 in map_context f (State (nd, node' :: nodes')) end
1.42 | map_goal _ _ state = state;
1.43
1.44 -fun set_goal goal = map_goal I (fn (statement, using, _, before_qed, after_qed) =>
1.45 - (statement, using, goal, before_qed, after_qed));
1.46 +fun set_goal goal = map_goal I (fn (statement, messages, using, _, before_qed, after_qed) =>
1.47 + (statement, messages, using, goal, before_qed, after_qed));
1.48
1.49 -fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) =>
1.50 - (statement, using, goal, before_qed, after_qed));
1.51 +fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) =>
1.52 + (statement, msg :: messages, using, goal, before_qed, after_qed));
1.53 +
1.54 +fun using_facts using = map_goal I (fn (statement, messages, _, goal, before_qed, after_qed) =>
1.55 + (statement, messages, using, goal, before_qed, after_qed));
1.56
1.57 local
1.58 fun find i state =
1.59 @@ -334,13 +339,14 @@
1.60 (case filter_out (equal "") strs of [] => ""
1.61 | strs' => enclose " (" ")" (commas strs'));
1.62
1.63 - fun prt_goal (SOME (ctxt, (i, {statement = _, using, goal, before_qed, after_qed}))) =
1.64 + fun prt_goal (SOME (ctxt, (i, {messages, using, goal, before_qed, after_qed, ...}))) =
1.65 pretty_facts "using " ctxt
1.66 (if mode <> Backward orelse null using then NONE else SOME using) @
1.67 [Pretty.str ("goal" ^
1.68 description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
1.69 pretty_goals_local ctxt Markup.subgoal
1.70 - (true, ! show_main_goal) (! Display.goals_limit) goal
1.71 + (true, ! show_main_goal) (! Display.goals_limit) goal @
1.72 + (map (fn msg => msg ()) (rev messages))
1.73 | prt_goal NONE = [];
1.74
1.75 val prt_ctxt =
1.76 @@ -380,7 +386,8 @@
1.77
1.78 fun apply_method current_context pos meth_fun state =
1.79 let
1.80 - val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state;
1.81 + val (goal_ctxt, (_, {statement, messages, using, goal, before_qed, after_qed})) =
1.82 + find_goal state;
1.83 val ctxt = ContextPosition.put pos (if current_context then context_of state else goal_ctxt);
1.84 val meth = meth_fun ctxt;
1.85 in
1.86 @@ -389,7 +396,7 @@
1.87 |> map_goal
1.88 (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #>
1.89 ProofContext.add_cases true meth_cases)
1.90 - (K (statement, using, goal', before_qed, after_qed)))
1.91 + (K (statement, messages, using, goal', before_qed, after_qed)))
1.92 end;
1.93
1.94 fun select_goals n meth state =
1.95 @@ -645,11 +652,11 @@
1.96 |> map_context_result
1.97 (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
1.98 |> (fn (named_facts, state') =>
1.99 - state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) =>
1.100 + state' |> map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) =>
1.101 let
1.102 val ctxt = context_of state';
1.103 val ths = maps snd named_facts;
1.104 - in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
1.105 + in (statement, messages, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
1.106
1.107 fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
1.108 fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths);
1.109 @@ -798,7 +805,7 @@
1.110 in
1.111 goal_state
1.112 |> map_context (init_context #> Variable.set_body true)
1.113 - |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed')))
1.114 + |> put_goal (SOME (make_goal ((kind, propss'), [], [], goal, before_qed, after_qed')))
1.115 |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
1.116 |> map_context (ProofContext.auto_bind_goal props)
1.117 |> chaining ? (`the_facts #-> using_facts)
1.118 @@ -812,8 +819,7 @@
1.119
1.120 fun generic_qed state =
1.121 let
1.122 - val (goal_ctxt, {statement = (_, stmt), using = _, goal, before_qed = _, after_qed}) =
1.123 - current_goal state;
1.124 + val (goal_ctxt, {statement = (_, stmt), goal, after_qed, ...}) = current_goal state;
1.125 val outer_state = state |> close_block;
1.126 val outer_ctxt = context_of outer_state;
1.127