# HG changeset patch # User wenzelm # Date 1181685698 -7200 # Node ID 23a8345f89f57f0328dcf303f4d04ac83c46ed1f # Parent 86e3729405448c537cea80e1468bc10717b17ce3 Basic text: include position; assumption/close: refer to non-atomic assumptions as well, implicit use of prems now considered legacy feature; diff -r 86e372940544 -r 23a8345f89f5 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue Jun 12 23:39:02 2007 +0200 +++ b/src/Pure/Isar/method.ML Wed Jun 13 00:01:38 2007 +0200 @@ -54,7 +54,7 @@ val tactic: string -> Proof.context -> method type src datatype text = - Basic of (Proof.context -> method) | + Basic of (Proof.context -> method) * Position.T | Source of src | Source_i of src | Then of text list | @@ -68,7 +68,7 @@ val this_text: text val done_text: text val sorry_text: bool -> text - val finish_text: text option * bool -> text + val finish_text: text option * bool -> Position.T -> text exception METHOD_FAIL of (string * Position.T) * exn val method: theory -> src -> Proof.context -> method val method_i: theory -> src -> Proof.context -> method @@ -215,29 +215,31 @@ local -fun asm_tac ths = - fold_rev (curry op APPEND') - (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths) (K no_tac); - fun cond_rtac cond rule = SUBGOAL (fn (prop, i) => if cond (Logic.strip_assums_concl prop) then Tactic.rtac rule i else no_tac); -fun assm_tac ctxt = +fun assm_tac warn_tac ctxt = assume_tac APPEND' - asm_tac (Assumption.prems_of ctxt) APPEND' + Goal.assume_rule_tac ctxt APPEND' + (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K warn_tac) APPEND' cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND' cond_rtac (can Logic.dest_term) Drule.termI; -fun assumption_tac ctxt [] = assm_tac ctxt - | assumption_tac _ [fact] = asm_tac [fact] - | assumption_tac _ _ = K no_tac; +fun legacy_tac ctxt st = + (legacy_feature ("implicit use of prems at end of proof" ^ ContextPosition.str_of ctxt); + all_tac st); in -fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt); +fun assumption ctxt = METHOD (HEADGOAL o + (fn [] => assm_tac all_tac ctxt + | [fact] => solve_tac [fact] + | _ => K no_tac)); + fun close immed ctxt = METHOD (K - (FILTER Thm.no_prems ((if immed then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac))); + (FILTER Thm.no_prems + ((if immed then ALLGOALS (assm_tac (legacy_tac ctxt) ctxt) else all_tac) THEN flexflex_tac))); end; @@ -356,7 +358,7 @@ type src = Args.src; datatype text = - Basic of (Proof.context -> method) | + Basic of (Proof.context -> method) * Position.T | Source of src | Source_i of src | Then of text list | @@ -365,15 +367,15 @@ Repeat1 of text | SelectGoals of int * text; -val primitive_text = Basic o K o SIMPLE_METHOD o PRIMITIVE; -val succeed_text = Basic (K succeed); +fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r)), Position.none); +val succeed_text = Basic (K succeed, Position.none); val default_text = Source (Args.src (("default", []), Position.none)); -val this_text = Basic (K this); -val done_text = Basic (K (SIMPLE_METHOD all_tac)); -val sorry_text = Basic o cheating; +val this_text = Basic (K this, Position.none); +val done_text = Basic (K (SIMPLE_METHOD all_tac), Position.none); +fun sorry_text int = Basic (cheating int, Position.none); -fun finish_text (NONE, immed) = Basic (close immed) - | finish_text (SOME txt, immed) = Then [txt, Basic (close immed)]; +fun finish_text (NONE, immed) pos = Basic (close immed, pos) + | finish_text (SOME txt, immed) pos = Then [txt, Basic (close immed, pos)]; (* method definitions *)