--- a/src/FOL/FOL.thy Thu Aug 14 21:06:07 2008 +0200
+++ b/src/FOL/FOL.thy Fri Aug 15 15:50:44 2008 +0200
@@ -74,7 +74,7 @@
*}
method_setup case_tac =
- {* Method.goal_args_ctxt Args.name case_tac *}
+ {* Method.goal_args_ctxt Args.name_source case_tac *}
"case_tac emulation (dynamic instantiation!)"
--- a/src/HOL/Tools/inductive_package.ML Thu Aug 14 21:06:07 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML Fri Aug 15 15:50:44 2008 +0200
@@ -458,7 +458,7 @@
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
-fun ind_cases src = Method.syntax (Scan.lift (Scan.repeat1 Args.name --
+fun ind_cases src = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source --
Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) [])) src
#> (fn ((raw_props, fixes), ctxt) =>
let
--- a/src/HOL/Tools/split_rule.ML Thu Aug 14 21:06:07 2008 +0200
+++ b/src/HOL/Tools/split_rule.ML Fri Aug 15 15:50:44 2008 +0200
@@ -144,11 +144,11 @@
(* attribute syntax *)
-(* FIXME dynamically scoped due to Args.name/pair_tac *)
+(* FIXME dynamically scoped due to Args.name_source/pair_tac *)
val split_format = Attrib.syntax (Scan.lift
(Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
- OuterParse.and_list1 (Scan.repeat Args.name)
+ OuterParse.and_list1 (Scan.repeat Args.name_source)
>> (fn xss => Thm.rule_attribute (fn context =>
split_rule_goal (Context.proof_of context) xss))));
--- a/src/HOL/UNITY/UNITY_Main.thy Thu Aug 14 21:06:07 2008 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Fri Aug 15 15:50:44 2008 +0200
@@ -16,7 +16,7 @@
method_setup ensures_tac = {*
fn args => fn ctxt =>
- Method.goal_args' (Scan.lift Args.name)
+ Method.goal_args' (Scan.lift Args.name_source)
(ensures_tac (local_clasimpset_of ctxt))
args ctxt *}
"for proving progress properties"
--- a/src/Pure/Isar/args.ML Thu Aug 14 21:06:07 2008 +0200
+++ b/src/Pure/Isar/args.ML Fri Aug 15 15:50:44 2008 +0200
@@ -32,6 +32,8 @@
val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
val mode: string -> 'a * T list -> bool * ('a * T list)
val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
+ val name_source: T list -> string * T list
+ val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
val name: T list -> string * T list
val alt_name: T list -> string * T list
val symbol: T list -> string * T list
@@ -164,6 +166,9 @@
fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
+val name_source = named >> T.source_of;
+val name_source_position = named >> T.source_position_of;
+
val name = named >> T.content_of;
val alt_name = alt_string >> T.content_of;
val symbol = symbolic >> T.content_of;
--- a/src/Pure/Isar/rule_insts.ML Thu Aug 14 21:06:07 2008 +0200
+++ b/src/Pure/Isar/rule_insts.ML Fri Aug 15 15:50:44 2008 +0200
@@ -212,7 +212,7 @@
val value =
Args.internal_typ >> T.Typ ||
Args.internal_term >> T.Term ||
- Args.name >> T.Text;
+ Args.name_source >> T.Text;
val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
>> (fn (xi, (a, v)) => (a, (xi, v)));
@@ -231,7 +231,7 @@
val value =
Args.internal_term >> T.Term ||
- Args.name >> T.Text;
+ Args.name_source >> T.Text;
val inst = Scan.ahead P.not_eof -- Args.maybe value;
val concl = Args.$$$ "concl" -- Args.colon;
@@ -408,16 +408,16 @@
(* method syntax *)
val insts =
- Scan.optional
- (Scan.lift (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
+ Scan.optional (Scan.lift
+ (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
-- Attrib.thms;
fun inst_args f src ctxt =
f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
val insts_var =
- Scan.optional
- (Scan.lift (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
+ Scan.optional (Scan.lift
+ (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
-- Attrib.thms;
fun inst_args_var f src ctxt =
@@ -438,13 +438,12 @@
"apply rule in forward manner (dynamic instantiation)"),
("cut_tac", inst_args_var cut_inst_meth,
"cut rule (dynamic instantiation)"),
- ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
+ ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name_source) subgoals_tac,
"insert subgoal (dynamic instantiation)"),
- ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
+ ("thin_tac", Method.goal_args_ctxt Args.name_source thin_tac,
"remove premise (dynamic instantiation)")]));
end;
structure BasicRuleInsts: BASIC_RULE_INSTS = RuleInsts;
open BasicRuleInsts;
-
--- a/src/Pure/ML/ml_antiquote.ML Thu Aug 14 21:06:07 2008 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Fri Aug 15 15:50:44 2008 +0200
@@ -78,7 +78,7 @@
val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
-val _ = inline "sort" (Args.context -- Scan.lift Args.name >> (fn (ctxt, s) =>
+val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
@@ -86,7 +86,7 @@
val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
val _ = macro "let" (Args.context --
- Scan.lift (P.and_list1 (P.and_list1 Args.name -- (Args.$$$ "=" |-- Args.name)))
+ Scan.lift (P.and_list1 (P.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
>> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
val _ = macro "note" (Args.context :|-- (fn ctxt =>
@@ -104,11 +104,11 @@
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
val _ = value "cpat"
- (Args.context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
+ (Args.context -- Scan.lift Args.name_source >> uncurry ProofContext.read_term_pattern >> (fn t =>
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
-fun type_ syn = (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
+fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
#1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
|> syn ? Sign.base_name
|> ML_Syntax.print_string));
@@ -117,7 +117,7 @@
val _ = inline "type_syntax" (type_ true);
-fun const syn = Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
+fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
#1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
|> syn ? ProofContext.const_syntax_name ctxt
|> ML_Syntax.print_string);
@@ -126,7 +126,7 @@
val _ = inline "const_syntax" (const true);
val _ = inline "const"
- (Args.context -- Scan.lift Args.name -- Scan.optional
+ (Args.context -- Scan.lift Args.name_source -- Scan.optional
(Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
>> (fn ((ctxt, c), Ts) =>
let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
--- a/src/Pure/Thy/thy_output.ML Thu Aug 14 21:06:07 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Aug 15 15:50:44 2008 +0200
@@ -508,7 +508,7 @@
fun output_ml ml src ctxt (txt, pos) =
(ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt);
- (if ! source then str_of_source src else txt)
+ (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
|> (if ! quotes then quote else I)
|> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else
@@ -545,7 +545,7 @@
("term_type", args Args.term (output pretty_term_typ)),
("typeof", args Args.term (output pretty_term_typeof)),
("const", args Args.const_proper (output pretty_const)),
- ("abbrev", args (Scan.lift Args.name) (output pretty_abbrev)),
+ ("abbrev", args (Scan.lift Args.name_source) (output pretty_abbrev)),
("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
("text", args (Scan.lift Args.name) (output (K pretty_text))),
("goals", output_goals true),
@@ -553,8 +553,8 @@
("prf", args Attrib.thms (output (pretty_prf false))),
("full_prf", args Attrib.thms (output (pretty_prf true))),
("theory", args (Scan.lift Args.name) (output pretty_theory)),
- ("ML", args (Scan.lift (P.position Args.name)) (output_ml ml_val)),
- ("ML_type", args (Scan.lift (P.position Args.name)) (output_ml ml_type)),
- ("ML_struct", args (Scan.lift (P.position Args.name)) (output_ml ml_struct))];
+ ("ML", args (Scan.lift Args.name_source_position) (output_ml ml_val)),
+ ("ML_type", args (Scan.lift Args.name_source_position) (output_ml ml_type)),
+ ("ML_struct", args (Scan.lift Args.name_source_position) (output_ml ml_struct))];
end;
--- a/src/Tools/induct_tacs.ML Thu Aug 14 21:06:07 2008 +0200
+++ b/src/Tools/induct_tacs.ML Fri Aug 15 15:50:44 2008 +0200
@@ -117,13 +117,14 @@
val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
val varss =
- OuterParse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
+ OuterParse.and_list'
+ (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
in
val setup =
Method.add_methods
- [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) gen_case_tac,
+ [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name_source -- opt_rule) gen_case_tac,
"unstructured case analysis on types"),
("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
"unstructured induction on types")];
--- a/src/ZF/Tools/ind_cases.ML Thu Aug 14 21:06:07 2008 +0200
+++ b/src/ZF/Tools/ind_cases.ML Fri Aug 15 15:50:44 2008 +0200
@@ -62,7 +62,7 @@
|> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
|> Method.erule 0;
-val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
+val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source));
(* package setup *)
--- a/src/ZF/UNITY/SubstAx.thy Thu Aug 14 21:06:07 2008 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Fri Aug 15 15:50:44 2008 +0200
@@ -378,7 +378,7 @@
method_setup ensures_tac = {*
fn args => fn ctxt =>
- Method.goal_args' (Scan.lift Args.name) (ensures_tac ctxt)
+ Method.goal_args' (Scan.lift Args.name_source) (ensures_tac ctxt)
args ctxt *}
"for proving progress properties"