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;
--- 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" #>
--- 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;
--- 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);
--- 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"
--- 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
--- 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)