# HG changeset patch # User wenzelm # Date 1189074641 -7200 # Node ID e2332d1ff6c77e706312551e5fde137bdaab80a6 # Parent f13c59e40617a14147afc4c56b90f276fec8b8a0 added goal_message; diff -r f13c59e40617 -r e2332d1ff6c7 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Sep 06 12:30:11 2007 +0200 +++ b/src/Pure/Isar/proof.ML Thu Sep 06 12:30:41 2007 +0200 @@ -28,6 +28,7 @@ val assert_backward: state -> state val assert_no_chain: state -> state val enter_forward: state -> state + val goal_message: (unit -> Pretty.T) -> state -> state val get_goal: state -> context * (thm list * thm) val schematic_goal: state -> bool val show_main_goal: bool ref @@ -137,6 +138,7 @@ and goal = Goal of {statement: string * term list list, (*goal kind and statement, starting with vars*) + messages: (unit -> Pretty.T) list, (*persistent messages (hints etc.)*) using: thm list, (*goal facts*) goal: thm, (*subgoals ==> statement*) before_qed: Method.text option, @@ -144,8 +146,8 @@ (thm list list -> state -> state Seq.seq) * (thm list list -> context -> context)}; -fun make_goal (statement, using, goal, before_qed, after_qed) = - Goal {statement = statement, using = using, goal = goal, +fun make_goal (statement, messages, using, goal, before_qed, after_qed) = + Goal {statement = statement, messages = messages, using = using, goal = goal, before_qed = before_qed, after_qed = after_qed}; fun make_node (context, facts, mode, goal) = @@ -274,19 +276,22 @@ fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) = let - val Goal {statement, using, goal, before_qed, after_qed} = goal; - val goal' = make_goal (g (statement, using, goal, before_qed, after_qed)); + val Goal {statement, messages, using, goal, before_qed, after_qed} = goal; + val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed)); in State (make_node (f context, facts, mode, SOME goal'), nodes) end | map_goal f g (State (nd, node :: nodes)) = let val State (node', nodes') = map_goal f g (State (node, nodes)) in map_context f (State (nd, node' :: nodes')) end | map_goal _ _ state = state; -fun set_goal goal = map_goal I (fn (statement, using, _, before_qed, after_qed) => - (statement, using, goal, before_qed, after_qed)); +fun set_goal goal = map_goal I (fn (statement, messages, using, _, before_qed, after_qed) => + (statement, messages, using, goal, before_qed, after_qed)); -fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) => - (statement, using, goal, before_qed, after_qed)); +fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => + (statement, msg :: messages, using, goal, before_qed, after_qed)); + +fun using_facts using = map_goal I (fn (statement, messages, _, goal, before_qed, after_qed) => + (statement, messages, using, goal, before_qed, after_qed)); local fun find i state = @@ -334,13 +339,14 @@ (case filter_out (equal "") strs of [] => "" | strs' => enclose " (" ")" (commas strs')); - fun prt_goal (SOME (ctxt, (i, {statement = _, using, goal, before_qed, after_qed}))) = + fun prt_goal (SOME (ctxt, (i, {messages, using, goal, before_qed, after_qed, ...}))) = pretty_facts "using " ctxt (if mode <> Backward orelse null using then NONE else SOME using) @ [Pretty.str ("goal" ^ description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ pretty_goals_local ctxt Markup.subgoal - (true, ! show_main_goal) (! Display.goals_limit) goal + (true, ! show_main_goal) (! Display.goals_limit) goal @ + (map (fn msg => msg ()) (rev messages)) | prt_goal NONE = []; val prt_ctxt = @@ -380,7 +386,8 @@ fun apply_method current_context pos meth_fun state = let - val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state; + val (goal_ctxt, (_, {statement, messages, using, goal, before_qed, after_qed})) = + find_goal state; val ctxt = ContextPosition.put pos (if current_context then context_of state else goal_ctxt); val meth = meth_fun ctxt; in @@ -389,7 +396,7 @@ |> map_goal (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #> ProofContext.add_cases true meth_cases) - (K (statement, using, goal', before_qed, after_qed))) + (K (statement, messages, using, goal', before_qed, after_qed))) end; fun select_goals n meth state = @@ -645,11 +652,11 @@ |> map_context_result (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args))) |> (fn (named_facts, state') => - state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) => + state' |> map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => let val ctxt = context_of state'; val ths = maps snd named_facts; - in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); + in (statement, messages, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths); @@ -798,7 +805,7 @@ in goal_state |> map_context (init_context #> Variable.set_body true) - |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed'))) + |> put_goal (SOME (make_goal ((kind, propss'), [], [], goal, before_qed, after_qed'))) |> map_context (ProofContext.add_cases false (AutoBind.cases thy props)) |> map_context (ProofContext.auto_bind_goal props) |> chaining ? (`the_facts #-> using_facts) @@ -812,8 +819,7 @@ fun generic_qed state = let - val (goal_ctxt, {statement = (_, stmt), using = _, goal, before_qed = _, after_qed}) = - current_goal state; + val (goal_ctxt, {statement = (_, stmt), goal, after_qed, ...}) = current_goal state; val outer_state = state |> close_block; val outer_ctxt = context_of outer_state;