src/Pure/Isar/method.ML
changeset 22118 16639b216295
parent 22086 cf6019fece63
child 22134 ab01073210e4
     1.1 --- a/src/Pure/Isar/method.ML	Fri Jan 19 22:08:26 2007 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Jan 19 22:08:27 2007 +0100
     1.3 @@ -12,7 +12,6 @@
     1.4    type method
     1.5    val trace_rules: bool ref
     1.6    val print_methods: theory -> unit
     1.7 -  val Method: bstring -> (Args.src -> Proof.context -> method) -> string -> unit
     1.8  end;
     1.9  
    1.10  signature METHOD =
    1.11 @@ -110,6 +109,7 @@
    1.12      (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
    1.13    val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.14      (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
    1.15 +  val parse: OuterLex.token list -> text * OuterLex.token list
    1.16  end;
    1.17  
    1.18  structure Method: METHOD =
    1.19 @@ -341,14 +341,14 @@
    1.20  fun set_tactic f = tactic_ref := f;
    1.21  
    1.22  fun tactic txt ctxt = METHOD (fn facts =>
    1.23 -  (Context.use_mltext
    1.24 +  (ML_Context.use_mltext
    1.25      ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic = \
    1.26         \let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\
    1.27         \  and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n"
    1.28         ^ txt ^
    1.29         "\nend in Method.set_tactic tactic end")
    1.30      false NONE;
    1.31 -    Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts));
    1.32 +    ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts));
    1.33  
    1.34  
    1.35  
    1.36 @@ -438,16 +438,12 @@
    1.37  
    1.38  val add_method = add_methods o Library.single;
    1.39  
    1.40 -fun Method name meth cmt = Context.>> (add_method (name, meth, cmt));
    1.41 -
    1.42  
    1.43  (* method_setup *)
    1.44  
    1.45  fun method_setup (name, txt, cmt) =
    1.46 -  Context.use_let
    1.47 -    "val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\
    1.48 -    \val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\
    1.49 -    \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
    1.50 +  ML_Context.use_let
    1.51 +    "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
    1.52      "Context.map_theory (Method.add_method method)"
    1.53      ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")")
    1.54    |> Context.theory_map;
    1.55 @@ -581,6 +577,33 @@
    1.56    ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);
    1.57  
    1.58  
    1.59 +(* outer parser *)
    1.60 +
    1.61 +local
    1.62 +
    1.63 +structure T = OuterLex;
    1.64 +structure P = OuterParse;
    1.65 +
    1.66 +fun is_symid_meth s =
    1.67 +  s <> "|" andalso s <> "?" andalso s <> "+" andalso T.is_sid s;
    1.68 +
    1.69 +fun meth4 x =
    1.70 + (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
    1.71 +  P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
    1.72 +and meth3 x =
    1.73 + (meth4 --| P.$$$ "?" >> Try ||
    1.74 +  meth4 --| P.$$$ "+" >> Repeat1 ||
    1.75 +  meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
    1.76 +  meth4) x
    1.77 +and meth2 x =
    1.78 + (P.position (P.xname -- P.args1 is_symid_meth false) >> (Source o Args.src) ||
    1.79 +  meth3) x
    1.80 +and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
    1.81 +and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
    1.82 +
    1.83 +in val parse = meth3 end;
    1.84 +
    1.85 +
    1.86  (*final declarations of this structure!*)
    1.87  val unfold = unfold_meth;
    1.88  val fold = fold_meth;