more static checking of proof methods;
authorwenzelm
Thu Mar 20 22:00:13 2014 +0100 (2014-03-20)
changeset 5623231e283f606e2
parent 56231 b98813774a63
child 56233 797060c19f5c
more static checking of proof methods;
NEWS
src/Pure/Isar/method.ML
     1.1 --- a/NEWS	Thu Mar 20 21:07:57 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 20 22:00:13 2014 +0100
     1.3 @@ -25,6 +25,15 @@
     1.4  supports input methods via ` (backquote), or << and >> (double angle
     1.5  brackets).
     1.6  
     1.7 +* More static checking of proof methods, which allows the system to
     1.8 +form a closure over the concrete syntax.  Method arguments should be
     1.9 +processed in the original proof context as far as possible, before
    1.10 +operating on the goal state.  In any case, the standard discipline for
    1.11 +subgoal-addressing needs to be observed: no subgoals or a subgoal
    1.12 +number that is out of range produces an empty result sequence, not an
    1.13 +exception.  Potential INCOMPATIBILITY for non-conformant tactical
    1.14 +proof tools.
    1.15 +
    1.16  
    1.17  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.18  
     2.1 --- a/src/Pure/Isar/method.ML	Thu Mar 20 21:07:57 2014 +0100
     2.2 +++ b/src/Pure/Isar/method.ML	Thu Mar 20 22:00:13 2014 +0100
     2.3 @@ -64,7 +64,6 @@
     2.4    val finish_text: text option * bool -> text
     2.5    val print_methods: Proof.context -> unit
     2.6    val check_name: Proof.context -> xstring * Position.T -> string
     2.7 -  val check_src: Proof.context -> src -> src
     2.8    val method: Proof.context -> src -> Proof.context -> method
     2.9    val method_cmd: Proof.context -> src -> Proof.context -> method
    2.10    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
    2.11 @@ -339,7 +338,7 @@
    2.12  (* check *)
    2.13  
    2.14  fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
    2.15 -fun check_src ctxt src = #1 (Args.check_src ctxt (get_methods ctxt) src);
    2.16 +fun check_src ctxt src = Args.check_src ctxt (get_methods ctxt) src;
    2.17  
    2.18  
    2.19  (* get methods *)
    2.20 @@ -348,7 +347,14 @@
    2.21    let val table = get_methods ctxt
    2.22    in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
    2.23  
    2.24 -fun method_cmd ctxt = method ctxt o check_src ctxt;
    2.25 +fun method_closure ctxt src0 =
    2.26 +  let
    2.27 +    val (src1, meth) = check_src ctxt src0;
    2.28 +    val src2 = Args.init_assignable src1;
    2.29 +    val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
    2.30 +  in Args.closure src2 end;
    2.31 +
    2.32 +fun method_cmd ctxt = method ctxt o method_closure ctxt;
    2.33  
    2.34  
    2.35  (* method setup *)