Args.name_source(_position) for proper position information;
authorwenzelm
Fri Aug 15 15:50:44 2008 +0200 (2008-08-15)
changeset 27882eaa9fef9f4c1
parent 27881 f0d543629376
child 27883 e506f0c6d3f0
Args.name_source(_position) for proper position information;
src/FOL/FOL.thy
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/split_rule.ML
src/HOL/UNITY/UNITY_Main.thy
src/Pure/Isar/args.ML
src/Pure/Isar/rule_insts.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/Thy/thy_output.ML
src/Tools/induct_tacs.ML
src/ZF/Tools/ind_cases.ML
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/src/FOL/FOL.thy	Thu Aug 14 21:06:07 2008 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Aug 15 15:50:44 2008 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  *}
     1.5  
     1.6  method_setup case_tac =
     1.7 -  {* Method.goal_args_ctxt Args.name case_tac *}
     1.8 +  {* Method.goal_args_ctxt Args.name_source case_tac *}
     1.9    "case_tac emulation (dynamic instantiation!)"
    1.10  
    1.11  
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Aug 14 21:06:07 2008 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Aug 15 15:50:44 2008 +0200
     2.3 @@ -458,7 +458,7 @@
     2.4  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
     2.5  
     2.6  
     2.7 -fun ind_cases src = Method.syntax (Scan.lift (Scan.repeat1 Args.name --
     2.8 +fun ind_cases src = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source --
     2.9      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) [])) src
    2.10    #> (fn ((raw_props, fixes), ctxt) =>
    2.11      let
     3.1 --- a/src/HOL/Tools/split_rule.ML	Thu Aug 14 21:06:07 2008 +0200
     3.2 +++ b/src/HOL/Tools/split_rule.ML	Fri Aug 15 15:50:44 2008 +0200
     3.3 @@ -144,11 +144,11 @@
     3.4  
     3.5  (* attribute syntax *)
     3.6  
     3.7 -(* FIXME dynamically scoped due to Args.name/pair_tac *)
     3.8 +(* FIXME dynamically scoped due to Args.name_source/pair_tac *)
     3.9  
    3.10  val split_format = Attrib.syntax (Scan.lift
    3.11   (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
    3.12 -  OuterParse.and_list1 (Scan.repeat Args.name)
    3.13 +  OuterParse.and_list1 (Scan.repeat Args.name_source)
    3.14      >> (fn xss => Thm.rule_attribute (fn context =>
    3.15          split_rule_goal (Context.proof_of context) xss))));
    3.16  
     4.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Thu Aug 14 21:06:07 2008 +0200
     4.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Fri Aug 15 15:50:44 2008 +0200
     4.3 @@ -16,7 +16,7 @@
     4.4  
     4.5  method_setup ensures_tac = {*
     4.6      fn args => fn ctxt =>
     4.7 -        Method.goal_args' (Scan.lift Args.name)
     4.8 +        Method.goal_args' (Scan.lift Args.name_source)
     4.9             (ensures_tac (local_clasimpset_of ctxt))
    4.10             args ctxt *}
    4.11      "for proving progress properties"
     5.1 --- a/src/Pure/Isar/args.ML	Thu Aug 14 21:06:07 2008 +0200
     5.2 +++ b/src/Pure/Isar/args.ML	Fri Aug 15 15:50:44 2008 +0200
     5.3 @@ -32,6 +32,8 @@
     5.4    val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
     5.5    val mode: string -> 'a * T list -> bool * ('a * T list)
     5.6    val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
     5.7 +  val name_source: T list -> string * T list
     5.8 +  val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
     5.9    val name: T list -> string * T list
    5.10    val alt_name: T list -> string * T list
    5.11    val symbol: T list -> string * T list
    5.12 @@ -164,6 +166,9 @@
    5.13  fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
    5.14  fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
    5.15  
    5.16 +val name_source = named >> T.source_of;
    5.17 +val name_source_position = named >> T.source_position_of;
    5.18 +
    5.19  val name = named >> T.content_of;
    5.20  val alt_name = alt_string >> T.content_of;
    5.21  val symbol = symbolic >> T.content_of;
     6.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Aug 14 21:06:07 2008 +0200
     6.2 +++ b/src/Pure/Isar/rule_insts.ML	Fri Aug 15 15:50:44 2008 +0200
     6.3 @@ -212,7 +212,7 @@
     6.4  val value =
     6.5    Args.internal_typ >> T.Typ ||
     6.6    Args.internal_term >> T.Term ||
     6.7 -  Args.name >> T.Text;
     6.8 +  Args.name_source >> T.Text;
     6.9  
    6.10  val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
    6.11    >> (fn (xi, (a, v)) => (a, (xi, v)));
    6.12 @@ -231,7 +231,7 @@
    6.13  
    6.14  val value =
    6.15    Args.internal_term >> T.Term ||
    6.16 -  Args.name >> T.Text;
    6.17 +  Args.name_source >> T.Text;
    6.18  
    6.19  val inst = Scan.ahead P.not_eof -- Args.maybe value;
    6.20  val concl = Args.$$$ "concl" -- Args.colon;
    6.21 @@ -408,16 +408,16 @@
    6.22  (* method syntax *)
    6.23  
    6.24  val insts =
    6.25 -  Scan.optional
    6.26 -    (Scan.lift (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
    6.27 +  Scan.optional (Scan.lift
    6.28 +    (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
    6.29      -- Attrib.thms;
    6.30  
    6.31  fun inst_args f src ctxt =
    6.32    f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
    6.33  
    6.34  val insts_var =
    6.35 -  Scan.optional
    6.36 -    (Scan.lift (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
    6.37 +  Scan.optional (Scan.lift
    6.38 +    (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
    6.39      -- Attrib.thms;
    6.40  
    6.41  fun inst_args_var f src ctxt =
    6.42 @@ -438,13 +438,12 @@
    6.43        "apply rule in forward manner (dynamic instantiation)"),
    6.44      ("cut_tac", inst_args_var cut_inst_meth,
    6.45        "cut rule (dynamic instantiation)"),
    6.46 -    ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
    6.47 +    ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name_source) subgoals_tac,
    6.48        "insert subgoal (dynamic instantiation)"),
    6.49 -    ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
    6.50 +    ("thin_tac", Method.goal_args_ctxt Args.name_source thin_tac,
    6.51        "remove premise (dynamic instantiation)")]));
    6.52  
    6.53  end;
    6.54  
    6.55  structure BasicRuleInsts: BASIC_RULE_INSTS = RuleInsts;
    6.56  open BasicRuleInsts;
    6.57 -
     7.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Aug 14 21:06:07 2008 +0200
     7.2 +++ b/src/Pure/ML/ml_antiquote.ML	Fri Aug 15 15:50:44 2008 +0200
     7.3 @@ -78,7 +78,7 @@
     7.4  
     7.5  val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
     7.6  
     7.7 -val _ = inline "sort" (Args.context -- Scan.lift Args.name >> (fn (ctxt, s) =>
     7.8 +val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
     7.9    ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
    7.10  
    7.11  val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
    7.12 @@ -86,7 +86,7 @@
    7.13  val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
    7.14  
    7.15  val _ = macro "let" (Args.context --
    7.16 -  Scan.lift (P.and_list1 (P.and_list1 Args.name -- (Args.$$$ "=" |-- Args.name)))
    7.17 +  Scan.lift (P.and_list1 (P.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
    7.18      >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
    7.19  
    7.20  val _ = macro "note" (Args.context :|-- (fn ctxt =>
    7.21 @@ -104,11 +104,11 @@
    7.22    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
    7.23  
    7.24  val _ = value "cpat"
    7.25 -  (Args.context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
    7.26 +  (Args.context -- Scan.lift Args.name_source >> uncurry ProofContext.read_term_pattern >> (fn t =>
    7.27      "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
    7.28  
    7.29  
    7.30 -fun type_ syn = (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
    7.31 +fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
    7.32      #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
    7.33      |> syn ? Sign.base_name
    7.34      |> ML_Syntax.print_string));
    7.35 @@ -117,7 +117,7 @@
    7.36  val _ = inline "type_syntax" (type_ true);
    7.37  
    7.38  
    7.39 -fun const syn = Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
    7.40 +fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
    7.41    #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
    7.42    |> syn ? ProofContext.const_syntax_name ctxt
    7.43    |> ML_Syntax.print_string);
    7.44 @@ -126,7 +126,7 @@
    7.45  val _ = inline "const_syntax" (const true);
    7.46  
    7.47  val _ = inline "const"
    7.48 -  (Args.context -- Scan.lift Args.name -- Scan.optional
    7.49 +  (Args.context -- Scan.lift Args.name_source -- Scan.optional
    7.50        (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
    7.51      >> (fn ((ctxt, c), Ts) =>
    7.52        let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
     8.1 --- a/src/Pure/Thy/thy_output.ML	Thu Aug 14 21:06:07 2008 +0200
     8.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 15 15:50:44 2008 +0200
     8.3 @@ -508,7 +508,7 @@
     8.4  
     8.5  fun output_ml ml src ctxt (txt, pos) =
     8.6   (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt);
     8.7 -  (if ! source then str_of_source src else txt)
     8.8 +  (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
     8.9    |> (if ! quotes then quote else I)
    8.10    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    8.11    else
    8.12 @@ -545,7 +545,7 @@
    8.13    ("term_type", args Args.term (output pretty_term_typ)),
    8.14    ("typeof", args Args.term (output pretty_term_typeof)),
    8.15    ("const", args Args.const_proper (output pretty_const)),
    8.16 -  ("abbrev", args (Scan.lift Args.name) (output pretty_abbrev)),
    8.17 +  ("abbrev", args (Scan.lift Args.name_source) (output pretty_abbrev)),
    8.18    ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
    8.19    ("text", args (Scan.lift Args.name) (output (K pretty_text))),
    8.20    ("goals", output_goals true),
    8.21 @@ -553,8 +553,8 @@
    8.22    ("prf", args Attrib.thms (output (pretty_prf false))),
    8.23    ("full_prf", args Attrib.thms (output (pretty_prf true))),
    8.24    ("theory", args (Scan.lift Args.name) (output pretty_theory)),
    8.25 -  ("ML", args (Scan.lift (P.position Args.name)) (output_ml ml_val)),
    8.26 -  ("ML_type", args (Scan.lift (P.position Args.name)) (output_ml ml_type)),
    8.27 -  ("ML_struct", args (Scan.lift (P.position Args.name)) (output_ml ml_struct))];
    8.28 +  ("ML", args (Scan.lift Args.name_source_position) (output_ml ml_val)),
    8.29 +  ("ML_type", args (Scan.lift Args.name_source_position) (output_ml ml_type)),
    8.30 +  ("ML_struct", args (Scan.lift Args.name_source_position) (output_ml ml_struct))];
    8.31  
    8.32  end;
     9.1 --- a/src/Tools/induct_tacs.ML	Thu Aug 14 21:06:07 2008 +0200
     9.2 +++ b/src/Tools/induct_tacs.ML	Fri Aug 15 15:50:44 2008 +0200
     9.3 @@ -117,13 +117,14 @@
     9.4  val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
     9.5  
     9.6  val varss =
     9.7 -  OuterParse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
     9.8 +  OuterParse.and_list'
     9.9 +    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
    9.10  
    9.11  in
    9.12  
    9.13  val setup =
    9.14    Method.add_methods
    9.15 -   [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) gen_case_tac,
    9.16 +   [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name_source -- opt_rule) gen_case_tac,
    9.17        "unstructured case analysis on types"),
    9.18      ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
    9.19        "unstructured induction on types")];
    10.1 --- a/src/ZF/Tools/ind_cases.ML	Thu Aug 14 21:06:07 2008 +0200
    10.2 +++ b/src/ZF/Tools/ind_cases.ML	Fri Aug 15 15:50:44 2008 +0200
    10.3 @@ -62,7 +62,7 @@
    10.4    |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
    10.5    |> Method.erule 0;
    10.6  
    10.7 -val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
    10.8 +val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source));
    10.9  
   10.10  
   10.11  (* package setup *)
    11.1 --- a/src/ZF/UNITY/SubstAx.thy	Thu Aug 14 21:06:07 2008 +0200
    11.2 +++ b/src/ZF/UNITY/SubstAx.thy	Fri Aug 15 15:50:44 2008 +0200
    11.3 @@ -378,7 +378,7 @@
    11.4  
    11.5  method_setup ensures_tac = {*
    11.6      fn args => fn ctxt =>
    11.7 -        Method.goal_args' (Scan.lift Args.name) (ensures_tac ctxt)
    11.8 +        Method.goal_args' (Scan.lift Args.name_source) (ensures_tac ctxt)
    11.9             args ctxt *}
   11.10      "for proving progress properties"
   11.11