# HG changeset patch
# User wenzelm
# Date 1218808244 -7200
# Node ID eaa9fef9f4c1e335bf14b8b17db864c6c7ae906e
# Parent  f0d543629376cc025d3143069442f08cc29de8ed
Args.name_source(_position) for proper position information;

diff -r f0d543629376 -r eaa9fef9f4c1 src/FOL/FOL.thy
--- 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!)"
 
 
diff -r f0d543629376 -r eaa9fef9f4c1 src/HOL/Tools/inductive_package.ML
--- 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
diff -r f0d543629376 -r eaa9fef9f4c1 src/HOL/Tools/split_rule.ML
--- 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))));
 
diff -r f0d543629376 -r eaa9fef9f4c1 src/HOL/UNITY/UNITY_Main.thy
--- 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"
diff -r f0d543629376 -r eaa9fef9f4c1 src/Pure/Isar/args.ML
--- 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;
diff -r f0d543629376 -r eaa9fef9f4c1 src/Pure/Isar/rule_insts.ML
--- 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;
-
diff -r f0d543629376 -r eaa9fef9f4c1 src/Pure/ML/ml_antiquote.ML
--- 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)
diff -r f0d543629376 -r eaa9fef9f4c1 src/Pure/Thy/thy_output.ML
--- 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;
diff -r f0d543629376 -r eaa9fef9f4c1 src/Tools/induct_tacs.ML
--- 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")];
diff -r f0d543629376 -r eaa9fef9f4c1 src/ZF/Tools/ind_cases.ML
--- 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 *)
diff -r f0d543629376 -r eaa9fef9f4c1 src/ZF/UNITY/SubstAx.thy
--- 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"