# HG changeset patch
# User wenzelm
# Date 1395349213 -3600
# Node ID 31e283f606e28e82801716a93ac64e858e020f0b
# Parent  b98813774a633d15dfeb37c012c6a2fff72c1291
more static checking of proof methods;

diff -r b98813774a63 -r 31e283f606e2 NEWS
--- a/NEWS	Thu Mar 20 21:07:57 2014 +0100
+++ b/NEWS	Thu Mar 20 22:00:13 2014 +0100
@@ -25,6 +25,15 @@
 supports input methods via ` (backquote), or << and >> (double angle
 brackets).
 
+* More static checking of proof methods, which allows the system to
+form a closure over the concrete syntax.  Method arguments should be
+processed in the original proof context as far as possible, before
+operating on the goal state.  In any case, the standard discipline for
+subgoal-addressing needs to be observed: no subgoals or a subgoal
+number that is out of range produces an empty result sequence, not an
+exception.  Potential INCOMPATIBILITY for non-conformant tactical
+proof tools.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r b98813774a63 -r 31e283f606e2 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Mar 20 21:07:57 2014 +0100
+++ b/src/Pure/Isar/method.ML	Thu Mar 20 22:00:13 2014 +0100
@@ -64,7 +64,6 @@
   val finish_text: text option * bool -> text
   val print_methods: Proof.context -> unit
   val check_name: Proof.context -> xstring * Position.T -> string
-  val check_src: Proof.context -> src -> src
   val method: Proof.context -> src -> Proof.context -> method
   val method_cmd: Proof.context -> src -> Proof.context -> method
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
@@ -339,7 +338,7 @@
 (* check *)
 
 fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
-fun check_src ctxt src = #1 (Args.check_src ctxt (get_methods ctxt) src);
+fun check_src ctxt src = Args.check_src ctxt (get_methods ctxt) src;
 
 
 (* get methods *)
@@ -348,7 +347,14 @@
   let val table = get_methods ctxt
   in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
 
-fun method_cmd ctxt = method ctxt o check_src ctxt;
+fun method_closure ctxt src0 =
+  let
+    val (src1, meth) = check_src ctxt src0;
+    val src2 = Args.init_assignable src1;
+    val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
+  in Args.closure src2 end;
+
+fun method_cmd ctxt = method ctxt o method_closure ctxt;
 
 
 (* method setup *)