equal
deleted
inserted
replaced
352 |
352 |
353 val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic); |
353 val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic); |
354 fun set_tactic f = tactic_ref := f; |
354 fun set_tactic f = tactic_ref := f; |
355 |
355 |
356 fun ml_tactic (txt, pos) ctxt = NAMED_CRITICAL "ML" (fn () => |
356 fun ml_tactic (txt, pos) ctxt = NAMED_CRITICAL "ML" (fn () => |
357 (ML_Context.use_mltext false pos |
357 (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos |
358 ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n" |
358 ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n" |
359 ^ txt ^ "\nin Method.set_tactic tactic end") (SOME (Context.Proof ctxt)); |
359 ^ txt ^ "\nin Method.set_tactic tactic end"); |
360 Context.setmp_thread_data (SOME (Context.Proof ctxt)) (! tactic_ref ctxt))); |
360 Context.setmp_thread_data (SOME (Context.Proof ctxt)) (! tactic_ref ctxt))); |
361 |
361 |
362 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt); |
362 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt); |
363 fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt); |
363 fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt); |
364 |
364 |
445 |
445 |
446 |
446 |
447 (* method_setup *) |
447 (* method_setup *) |
448 |
448 |
449 fun method_setup name (txt, pos) cmt = |
449 fun method_setup name (txt, pos) cmt = |
450 ML_Context.use_let pos |
450 ML_Context.expression pos |
451 "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string" |
451 "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string" |
452 "Context.map_theory (Method.add_method method)" |
452 "Context.map_theory (Method.add_method method)" |
453 ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")") |
453 ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")") |
454 |> Context.theory_map; |
454 |> Context.theory_map; |
455 |
455 |