src/Pure/Isar/method.ML
changeset 26472 9afdd61cf528
parent 26463 9283b4185fdf
child 26762 78ed28528ca6
     1.1 --- a/src/Pure/Isar/method.ML	Fri Mar 28 22:39:42 2008 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Mar 28 22:39:43 2008 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4    val drule: int -> thm list -> method
     1.5    val frule: int -> thm list -> method
     1.6    val iprover_tac: Proof.context -> int option -> int -> tactic
     1.7 -  val set_tactic: (Proof.context -> thm list -> tactic) -> unit
     1.8 +  val set_tactic: (Proof.context -> thm list -> tactic) -> Proof.context -> Proof.context
     1.9    val tactic: string * Position.T -> Proof.context -> method
    1.10    type src
    1.11    datatype text =
    1.12 @@ -350,14 +350,21 @@
    1.13  
    1.14  (* ML tactics *)
    1.15  
    1.16 -val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
    1.17 -fun set_tactic f = tactic_ref := f;
    1.18 +structure TacticData = ProofDataFun
    1.19 +(
    1.20 +  type T = Proof.context -> thm list -> tactic;
    1.21 +  fun init _ = undefined;
    1.22 +);
    1.23 +
    1.24 +val set_tactic = TacticData.put;
    1.25  
    1.26 -fun ml_tactic (txt, pos) ctxt = NAMED_CRITICAL "ML" (fn () =>
    1.27 -  (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos
    1.28 -    ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
    1.29 -      ^ txt ^ "\nin Method.set_tactic tactic end");
    1.30 -    Context.setmp_thread_data (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
    1.31 +fun ml_tactic (txt, pos) ctxt =
    1.32 +  let
    1.33 +    val ctxt' = ctxt |> Context.proof_map
    1.34 +      (ML_Context.expression Position.none
    1.35 +        "fun tactic (ctxt: Proof.context) (facts: thm list) : tactic"
    1.36 +        "Context.map_proof (Method.set_tactic tactic)" txt);
    1.37 +  in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt' ctxt) end;
    1.38  
    1.39  fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
    1.40  fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
    1.41 @@ -447,11 +454,10 @@
    1.42  (* method_setup *)
    1.43  
    1.44  fun method_setup name (txt, pos) cmt =
    1.45 -  ML_Context.expression pos
    1.46 +  Context.theory_map (ML_Context.expression pos
    1.47      "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
    1.48      "Context.map_theory (Method.add_method method)"
    1.49 -    ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")")
    1.50 -  |> Context.theory_map;
    1.51 +    ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")"));
    1.52  
    1.53  
    1.54