# HG changeset patch
# User wenzelm
# Date 1393335258 -3600
# Node ID a989bdaf81212e7ef097f5829930a69e7069f2ba
# Parent  b969263fcf0236e26575ac13b2ca45646561c0f2
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
removed obsolete Method.Source_i;
proper context for global data;
tuned messages;

diff -r b969263fcf02 -r a989bdaf8121 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Tue Feb 25 12:53:08 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Tue Feb 25 14:34:18 2014 +0100
@@ -212,7 +212,7 @@
   entity_antiqs (K command_check) "isacommand" "command" #>
   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
-  entity_antiqs (thy_check Method.check) "" "method" #>
+  entity_antiqs (can o Method.check_name) "" "method" #>
   entity_antiqs (thy_check Attrib.check) "" "attribute" #>
   entity_antiqs no_check "" "fact" #>
   entity_antiqs no_check "" "variable" #>
diff -r b969263fcf02 -r a989bdaf8121 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Tue Feb 25 12:53:08 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Tue Feb 25 14:34:18 2014 +0100
@@ -55,9 +55,10 @@
   #> Scan.read Token.stopper Method.parse
   #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
 
-fun apply_named_method_on_first_goal thy =
+fun apply_named_method_on_first_goal ctxt =
   parse_method
-  #> Method.method thy
+  #> Method.check_source ctxt
+  #> Method.the_method ctxt
   #> Method.Basic
   #> curry Method.Select_Goals 1
   #> Proof.refine;
@@ -77,7 +78,7 @@
         ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
          (if all_goals andalso nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
         I (#goal o Proof.goal)
-        (apply_named_method_on_first_goal (Proof.theory_of st) (name ^ attrs)) st
+        (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)) st
     end
   else
     NONE;
diff -r b969263fcf02 -r a989bdaf8121 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Feb 25 12:53:08 2014 +0100
+++ b/src/Pure/General/name_space.ML	Tue Feb 25 14:34:18 2014 +0100
@@ -1,8 +1,8 @@
 (*  Title:      Pure/General/name_space.ML
     Author:     Markus Wenzel, TU Muenchen
 
-Generic name spaces with declared and hidden entries.  Unknown names
-are considered global; no support for absolute addressing.
+Generic name spaces with declared and hidden entries; no support for
+absolute addressing.
 *)
 
 type xstring = string;    (*external names*)
@@ -120,7 +120,7 @@
 
 fun the_entry (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
-    NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
+    NONE => error (undefined kind name)
   | SOME (_, entry) => entry);
 
 fun entry_ord space = int_ord o pairself (#id o the_entry space);
diff -r b969263fcf02 -r a989bdaf8121 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Feb 25 12:53:08 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 25 14:34:18 2014 +0100
@@ -809,7 +809,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
     (Scan.succeed (Toplevel.unknown_theory o
-      Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
+      Toplevel.keep (Method.print_methods o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
diff -r b969263fcf02 -r a989bdaf8121 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Feb 25 12:53:08 2014 +0100
+++ b/src/Pure/Isar/method.ML	Tue Feb 25 14:34:18 2014 +0100
@@ -46,9 +46,8 @@
   val raw_tactic: string * Position.T -> Proof.context -> method
   type src = Args.src
   datatype text =
+    Source of src |
     Basic of Proof.context -> method |
-    Source of src |
-    Source_i of src |
     Then of text list |
     Orelse of text list |
     Try of text |
@@ -61,11 +60,10 @@
   val done_text: text
   val sorry_text: bool -> text
   val finish_text: text option * bool -> text
-  val print_methods: theory -> unit
-  val check: theory -> xstring * Position.T -> string
-  val intern: theory -> xstring -> string
-  val method: theory -> src -> Proof.context -> method
-  val method_i: theory -> src -> Proof.context -> method
+  val print_methods: Proof.context -> unit
+  val the_method: Proof.context -> src -> Proof.context -> method
+  val check_name: Proof.context -> xstring * Position.T -> string
+  val check_source: Proof.context -> src -> src
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
   val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -284,9 +282,8 @@
 type src = Args.src;
 
 datatype text =
+  Source of src |
   Basic of Proof.context -> method |
-  Source of src |
-  Source_i of src |
   Then of text list |
   Orelse of text list |
   Try of text |
@@ -314,10 +311,11 @@
   fun merge data : T = Name_Space.merge_tables data;
 );
 
-fun print_methods thy =
+val get_methods = Methods.get o Proof_Context.theory_of;
+
+fun print_methods ctxt =
   let
-    val ctxt = Proof_Context.init_global thy;
-    val meths = Methods.get thy;
+    val meths = get_methods ctxt;
     fun prt_meth (name, (_, "")) = Pretty.mark_str name
       | prt_meth (name, (_, comment)) =
           Pretty.block
@@ -330,25 +328,26 @@
 fun add_method name meth comment thy = thy
   |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
 
-
-(* get methods *)
-
-fun check thy = #1 o Name_Space.check (Context.Theory thy) (Methods.get thy);
-
-val intern = Name_Space.intern o #1 o Methods.get;
-
-fun method_i thy =
-  let
-    val (space, tab) = Methods.get thy;
-    fun meth src =
+fun the_method ctxt =
+  let val (_, tab) = get_methods ctxt in
+    fn src =>
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup tab name of
-          NONE => error ("Unknown proof method: " ^ quote name ^ Position.here pos)
-        | SOME (mth, _) => (Position.report pos (Name_Space.markup space name); mth src))
-      end;
-  in meth end;
+          NONE => error ("Undefined method: " ^ quote name ^ Position.here pos)
+        | SOME (method, _) => method src)
+      end
+  end;
+
+
+(* check *)
 
-fun method thy = method_i thy o Args.map_name (intern thy);
+fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
+
+fun check_source ctxt src =
+  let
+    val ((xname, toks), pos) = Args.dest_src src;
+    val name = check_name ctxt (xname, pos);
+  in Args.src ((name, toks), pos) end;
 
 
 (* method setup *)
@@ -406,7 +405,6 @@
 
 fun meth4 x =
  (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
-  (* FIXME implicit "cartouche" method (experimental, undocumented) *)
   Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
     Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) ||
   Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
diff -r b969263fcf02 -r a989bdaf8121 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Feb 25 12:53:08 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Feb 25 14:34:18 2014 +0100
@@ -392,13 +392,13 @@
   Rule_Cases.make_common
     (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
 
-fun apply_method current_context meth state =
+fun apply_method current_context method state =
   let
     val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
       find_goal state;
     val ctxt = if current_context then context_of state else goal_ctxt;
   in
-    Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
+    Method.apply method ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
       state
       |> map_goal
           (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
@@ -416,13 +416,13 @@
       |> Seq.lift provide_goal (PRIMITIVE (Goal.unrestrict 1) (#2 (#2 (get_goal state')))))
     |> Seq.maps (apply_method true (K Method.succeed)));
 
-fun apply_text cc text state =
+fun apply_text current_context text state =
   let
-    val thy = theory_of state;
+    val ctxt = context_of state;
 
-    fun eval (Method.Basic m) = apply_method cc m
-      | eval (Method.Source src) = apply_method cc (Method.method thy src)
-      | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src)
+    fun eval (Method.Basic m) = apply_method current_context m
+      | eval (Method.Source src) =
+          apply_method current_context (Method.the_method ctxt (Method.check_source ctxt src))
       | eval (Method.Then txts) = Seq.EVERY (map eval txts)
       | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
       | eval (Method.Try txt) = Seq.TRY (eval txt)