src/Pure/Isar/method.ML
changeset 55742 a989bdaf8121
parent 55709 4e5a83a46ded
child 55761 213b9811f59f
     1.1 --- a/src/Pure/Isar/method.ML	Tue Feb 25 12:53:08 2014 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Feb 25 14:34:18 2014 +0100
     1.3 @@ -46,9 +46,8 @@
     1.4    val raw_tactic: string * Position.T -> Proof.context -> method
     1.5    type src = Args.src
     1.6    datatype text =
     1.7 +    Source of src |
     1.8      Basic of Proof.context -> method |
     1.9 -    Source of src |
    1.10 -    Source_i of src |
    1.11      Then of text list |
    1.12      Orelse of text list |
    1.13      Try of text |
    1.14 @@ -61,11 +60,10 @@
    1.15    val done_text: text
    1.16    val sorry_text: bool -> text
    1.17    val finish_text: text option * bool -> text
    1.18 -  val print_methods: theory -> unit
    1.19 -  val check: theory -> xstring * Position.T -> string
    1.20 -  val intern: theory -> xstring -> string
    1.21 -  val method: theory -> src -> Proof.context -> method
    1.22 -  val method_i: theory -> src -> Proof.context -> method
    1.23 +  val print_methods: Proof.context -> unit
    1.24 +  val the_method: Proof.context -> src -> Proof.context -> method
    1.25 +  val check_name: Proof.context -> xstring * Position.T -> string
    1.26 +  val check_source: Proof.context -> src -> src
    1.27    val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    1.28    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
    1.29    val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
    1.30 @@ -284,9 +282,8 @@
    1.31  type src = Args.src;
    1.32  
    1.33  datatype text =
    1.34 +  Source of src |
    1.35    Basic of Proof.context -> method |
    1.36 -  Source of src |
    1.37 -  Source_i of src |
    1.38    Then of text list |
    1.39    Orelse of text list |
    1.40    Try of text |
    1.41 @@ -314,10 +311,11 @@
    1.42    fun merge data : T = Name_Space.merge_tables data;
    1.43  );
    1.44  
    1.45 -fun print_methods thy =
    1.46 +val get_methods = Methods.get o Proof_Context.theory_of;
    1.47 +
    1.48 +fun print_methods ctxt =
    1.49    let
    1.50 -    val ctxt = Proof_Context.init_global thy;
    1.51 -    val meths = Methods.get thy;
    1.52 +    val meths = get_methods ctxt;
    1.53      fun prt_meth (name, (_, "")) = Pretty.mark_str name
    1.54        | prt_meth (name, (_, comment)) =
    1.55            Pretty.block
    1.56 @@ -330,25 +328,26 @@
    1.57  fun add_method name meth comment thy = thy
    1.58    |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
    1.59  
    1.60 -
    1.61 -(* get methods *)
    1.62 -
    1.63 -fun check thy = #1 o Name_Space.check (Context.Theory thy) (Methods.get thy);
    1.64 -
    1.65 -val intern = Name_Space.intern o #1 o Methods.get;
    1.66 -
    1.67 -fun method_i thy =
    1.68 -  let
    1.69 -    val (space, tab) = Methods.get thy;
    1.70 -    fun meth src =
    1.71 +fun the_method ctxt =
    1.72 +  let val (_, tab) = get_methods ctxt in
    1.73 +    fn src =>
    1.74        let val ((name, _), pos) = Args.dest_src src in
    1.75          (case Symtab.lookup tab name of
    1.76 -          NONE => error ("Unknown proof method: " ^ quote name ^ Position.here pos)
    1.77 -        | SOME (mth, _) => (Position.report pos (Name_Space.markup space name); mth src))
    1.78 -      end;
    1.79 -  in meth end;
    1.80 +          NONE => error ("Undefined method: " ^ quote name ^ Position.here pos)
    1.81 +        | SOME (method, _) => method src)
    1.82 +      end
    1.83 +  end;
    1.84 +
    1.85 +
    1.86 +(* check *)
    1.87  
    1.88 -fun method thy = method_i thy o Args.map_name (intern thy);
    1.89 +fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
    1.90 +
    1.91 +fun check_source ctxt src =
    1.92 +  let
    1.93 +    val ((xname, toks), pos) = Args.dest_src src;
    1.94 +    val name = check_name ctxt (xname, pos);
    1.95 +  in Args.src ((name, toks), pos) end;
    1.96  
    1.97  
    1.98  (* method setup *)
    1.99 @@ -406,7 +405,6 @@
   1.100  
   1.101  fun meth4 x =
   1.102   (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
   1.103 -  (* FIXME implicit "cartouche" method (experimental, undocumented) *)
   1.104    Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
   1.105      Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) ||
   1.106    Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x