tuned signature -- moved type src to Token, without aliases;
authorwenzelm
Tue Aug 19 23:17:51 2014 +0200 (2014-08-19 ago)
changeset 58011bc6bced136e5
parent 58010 568840962230
child 58012 0b0519c41229
tuned signature -- moved type src to Token, without aliases;
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/try0.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/bundle.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/code.ML
src/Pure/Isar/element.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_antiquotation.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_thms.ML
src/Pure/Thy/term_style.ML
src/Pure/Thy/thy_output.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Aug 19 18:21:29 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Aug 19 23:17:51 2014 +0200
     1.3 @@ -21,17 +21,17 @@
     1.4    val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
     1.5  
     1.6    type lfp_sugar_thms =
     1.7 -    (thm list * thm * Args.src list) * (thm list list * Args.src list)
     1.8 +    (thm list * thm * Token.src list) * (thm list list * Token.src list)
     1.9  
    1.10    val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms
    1.11    val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
    1.12  
    1.13    type gfp_sugar_thms =
    1.14 -    ((thm list * thm) list * (Args.src list * Args.src list))
    1.15 +    ((thm list * thm) list * (Token.src list * Token.src list))
    1.16      * thm list list
    1.17      * thm list list
    1.18 -    * (thm list list * Args.src list)
    1.19 -    * (thm list list list * Args.src list)
    1.20 +    * (thm list list * Token.src list)
    1.21 +    * (thm list list list * Token.src list)
    1.22  
    1.23    val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
    1.24    val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms
    1.25 @@ -304,7 +304,7 @@
    1.26  fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
    1.27  
    1.28  type lfp_sugar_thms =
    1.29 -  (thm list * thm * Args.src list) * (thm list list * Args.src list);
    1.30 +  (thm list * thm * Token.src list) * (thm list list * Token.src list);
    1.31  
    1.32  fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) =
    1.33    ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
    1.34 @@ -315,11 +315,11 @@
    1.35    morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
    1.36  
    1.37  type gfp_sugar_thms =
    1.38 -  ((thm list * thm) list * (Args.src list * Args.src list))
    1.39 +  ((thm list * thm) list * (Token.src list * Token.src list))
    1.40    * thm list list
    1.41    * thm list list
    1.42 -  * (thm list list * Args.src list)
    1.43 -  * (thm list list list * Args.src list);
    1.44 +  * (thm list list * Token.src list)
    1.45 +  * (thm list list list * Token.src list);
    1.46  
    1.47  fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair),
    1.48      corecss, corec_discss, (corec_disc_iffss, corec_disc_iff_attrs),
     2.1 --- a/src/HOL/Tools/Function/function_common.ML	Tue Aug 19 18:21:29 2014 +0200
     2.2 +++ b/src/HOL/Tools/Function/function_common.ML	Tue Aug 19 23:17:51 2014 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4    defname : string,
     2.5      (* contains no logical entities: invariant under morphisms: *)
     2.6    add_simps : (binding -> binding) -> string -> (binding -> binding) ->
     2.7 -    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
     2.8 +    Token.src list -> thm list -> local_theory -> thm list * local_theory,
     2.9    fnames : string list,
    2.10    case_names : string list,
    2.11    fs : term list,
    2.12 @@ -37,7 +37,7 @@
    2.13    defname : string,
    2.14      (* contains no logical entities: invariant under morphisms: *)
    2.15    add_simps : (binding -> binding) -> string -> (binding -> binding) ->
    2.16 -    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
    2.17 +    Token.src list -> thm list -> local_theory -> thm list * local_theory,
    2.18    fnames : string list,
    2.19    case_names : string list,
    2.20    fs : term list,
     3.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Aug 19 18:21:29 2014 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Aug 19 23:17:51 2014 +0200
     3.3 @@ -13,7 +13,8 @@
     3.4      (binding * mixfix) -> typ -> term -> thm -> thm list -> local_theory -> local_theory
     3.5  
     3.6    val lift_def_cmd:
     3.7 -    (binding * string option * mixfix) * string * (Facts.ref * Args.src list) list -> local_theory -> Proof.state
     3.8 +    (binding * string option * mixfix) * string * (Facts.ref * Token.src list) list ->
     3.9 +    local_theory -> Proof.state
    3.10  
    3.11    val can_generate_code_cert: thm -> bool
    3.12  end
     4.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 19 18:21:29 2014 +0200
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 19 23:17:51 2014 +0200
     4.3 @@ -223,7 +223,7 @@
     4.4      val dummy_thm = Thm.transfer thy Drule.dummy_thm
     4.5      val pointer = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none bundle_name
     4.6      val restore_lifting_att = 
     4.7 -      ([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer])
     4.8 +      ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
     4.9    in
    4.10      lthy 
    4.11        |> Local_Theory.declaration {syntax = false, pervasive = true}
    4.12 @@ -969,7 +969,7 @@
    4.13      case bundle of
    4.14        [(_, [arg_src])] => 
    4.15          let
    4.16 -          val (name, _) = Args.syntax (Scan.lift Args.name) arg_src ctxt
    4.17 +          val (name, _) = Token.syntax (Scan.lift Args.name) arg_src ctxt
    4.18              handle ERROR _ => error "The provided bundle is not a lifting bundle."
    4.19          in name end
    4.20        | _ => error "The provided bundle is not a lifting bundle."
     5.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Tue Aug 19 18:21:29 2014 +0200
     5.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Tue Aug 19 23:17:51 2014 +0200
     5.3 @@ -13,7 +13,7 @@
     5.4      ((binding * binding) option * bool * thm option) -> Proof.context -> Proof.state
     5.5  
     5.6    val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
     5.7 -    (binding * binding) option) * (Facts.ref * Args.src list) option -> Proof.context -> Proof.state
     5.8 +    (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state
     5.9  end;
    5.10  
    5.11  structure Quotient_Type: QUOTIENT_TYPE =
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Aug 19 18:21:29 2014 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Aug 19 23:17:51 2014 +0200
     6.3 @@ -14,15 +14,15 @@
     6.4    type fact = (string * stature) * thm
     6.5  
     6.6    type fact_override =
     6.7 -    {add : (Facts.ref * Attrib.src list) list,
     6.8 -     del : (Facts.ref * Attrib.src list) list,
     6.9 +    {add : (Facts.ref * Token.src list) list,
    6.10 +     del : (Facts.ref * Token.src list) list,
    6.11       only : bool}
    6.12  
    6.13    val instantiate_inducts : bool Config.T
    6.14    val no_fact_override : fact_override
    6.15  
    6.16    val fact_of_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table ->
    6.17 -    Facts.ref * Attrib.src list -> ((string * stature) * thm) list
    6.18 +    Facts.ref * Token.src list -> ((string * stature) * thm) list
    6.19    val backquote_thm : Proof.context -> thm -> string
    6.20    val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
    6.21    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    6.22 @@ -50,8 +50,8 @@
    6.23  type fact = (string * stature) * thm
    6.24  
    6.25  type fact_override =
    6.26 -  {add : (Facts.ref * Attrib.src list) list,
    6.27 -   del : (Facts.ref * Attrib.src list) list,
    6.28 +  {add : (Facts.ref * Token.src list) list,
    6.29 +   del : (Facts.ref * Token.src list) list,
    6.30     only : bool}
    6.31  
    6.32  (* gracefully handle huge background theories *)
    6.33 @@ -159,7 +159,7 @@
    6.34  fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
    6.35    let
    6.36      val ths = Attrib.eval_thms ctxt [xthm]
    6.37 -    val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args)
    6.38 +    val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args)
    6.39  
    6.40      fun nth_name j =
    6.41        (case xref of
     7.1 --- a/src/HOL/Tools/inductive.ML	Tue Aug 19 18:21:29 2014 +0200
     7.2 +++ b/src/HOL/Tools/inductive.ML	Tue Aug 19 23:17:51 2014 +0200
     7.3 @@ -53,7 +53,7 @@
     7.4      (binding * string option * mixfix) list ->
     7.5      (binding * string option * mixfix) list ->
     7.6      (Attrib.binding * string) list ->
     7.7 -    (Facts.ref * Attrib.src list) list ->
     7.8 +    (Facts.ref * Token.src list) list ->
     7.9      local_theory -> inductive_result * local_theory
    7.10    val add_inductive_global: inductive_flags ->
    7.11      ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
    7.12 @@ -76,7 +76,7 @@
    7.13      term list -> (binding * mixfix) list ->
    7.14      local_theory -> inductive_result * local_theory
    7.15    val declare_rules: binding -> bool -> bool -> string list -> term list ->
    7.16 -    thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
    7.17 +    thm list -> binding list -> Token.src list list -> (thm * string list * int) list ->
    7.18      thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory
    7.19    val add_ind_def: add_ind_def
    7.20    val gen_add_inductive_i: add_ind_def -> inductive_flags ->
    7.21 @@ -85,7 +85,7 @@
    7.22    val gen_add_inductive: add_ind_def -> bool -> bool ->
    7.23      (binding * string option * mixfix) list ->
    7.24      (binding * string option * mixfix) list ->
    7.25 -    (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
    7.26 +    (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
    7.27      local_theory -> inductive_result * local_theory
    7.28    val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser
    7.29  end;
     8.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Aug 19 18:21:29 2014 +0200
     8.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Aug 19 23:17:51 2014 +0200
     8.3 @@ -20,7 +20,7 @@
     8.4    val add_inductive: bool -> bool ->
     8.5      (binding * string option * mixfix) list ->
     8.6      (binding * string option * mixfix) list ->
     8.7 -    (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     8.8 +    (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
     8.9      local_theory -> Inductive.inductive_result * local_theory
    8.10    val mono_add: attribute
    8.11    val mono_del: attribute
     9.1 --- a/src/HOL/Tools/recdef.ML	Tue Aug 19 18:21:29 2014 +0200
     9.2 +++ b/src/HOL/Tools/recdef.ML	Tue Aug 19 23:17:51 2014 +0200
     9.3 @@ -15,17 +15,17 @@
     9.4    val cong_del: attribute
     9.5    val wf_add: attribute
     9.6    val wf_del: attribute
     9.7 -  val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
     9.8 -    Attrib.src option -> theory -> theory
     9.9 +  val add_recdef: bool -> xstring -> string -> ((binding * string) * Token.src list) list ->
    9.10 +    Token.src option -> theory -> theory
    9.11        * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    9.12    val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
    9.13      theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    9.14 -  val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
    9.15 +  val defer_recdef: xstring -> string list -> (Facts.ref * Token.src list) list
    9.16      -> theory -> theory * {induct_rules: thm}
    9.17    val defer_recdef_i: xstring -> term list -> thm list -> theory -> theory * {induct_rules: thm}
    9.18 -  val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> bool ->
    9.19 +  val recdef_tc: bstring * Token.src list -> xstring -> int option -> bool ->
    9.20      local_theory -> Proof.state
    9.21 -  val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> bool ->
    9.22 +  val recdef_tc_i: bstring * Token.src list -> string -> int option -> bool ->
    9.23      local_theory -> Proof.state
    9.24    val setup: theory -> theory
    9.25  end;
    9.26 @@ -164,7 +164,7 @@
    9.27      val ctxt =
    9.28        (case opt_src of
    9.29          NONE => ctxt0
    9.30 -      | SOME src => #2 (Args.syntax (Method.sections recdef_modifiers) src ctxt0));
    9.31 +      | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt0));
    9.32      val {simps, congs, wfs} = get_hints ctxt;
    9.33      val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
    9.34    in (ctxt', rev (map snd congs), wfs) end;
    9.35 @@ -292,7 +292,7 @@
    9.36  val hints =
    9.37    @{keyword "("} |--
    9.38      Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"})
    9.39 -  >> uncurry Args.src;
    9.40 +  >> uncurry Token.src;
    9.41  
    9.42  val recdef_decl =
    9.43    Scan.optional
    10.1 --- a/src/HOL/Tools/try0.ML	Tue Aug 19 18:21:29 2014 +0200
    10.2 +++ b/src/HOL/Tools/try0.ML	Tue Aug 19 23:17:51 2014 +0200
    10.3 @@ -173,7 +173,7 @@
    10.4  
    10.5  fun string_of_xthm (xref, args) =
    10.6    Facts.string_of_ref xref ^
    10.7 -  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src @{context}) args);
    10.8 +  implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args);
    10.9  
   10.10  val parse_fact_refs =
   10.11    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse_Spec.xthm >> string_of_xthm));
    11.1 --- a/src/Pure/Isar/args.ML	Tue Aug 19 18:21:29 2014 +0200
    11.2 +++ b/src/Pure/Isar/args.ML	Tue Aug 19 23:17:51 2014 +0200
    11.3 @@ -1,22 +1,12 @@
    11.4  (*  Title:      Pure/Isar/args.ML
    11.5      Author:     Markus Wenzel, TU Muenchen
    11.6  
    11.7 -Parsing with implicit value assignment.  Concrete argument syntax of
    11.8 +Quasi-inner syntax based on outer tokens: concrete argument syntax of
    11.9  attributes, methods etc.
   11.10  *)
   11.11  
   11.12  signature ARGS =
   11.13  sig
   11.14 -  type src
   11.15 -  val src: xstring * Position.T -> Token.T list -> src
   11.16 -  val name_of_src: src -> string * Position.T
   11.17 -  val range_of_src: src -> Position.T
   11.18 -  val unparse_src: src -> string list
   11.19 -  val pretty_src: Proof.context -> src -> Pretty.T
   11.20 -  val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
   11.21 -  val transform_values: morphism -> src -> src
   11.22 -  val init_assignable: src -> src
   11.23 -  val closure: src -> src
   11.24    val context: Proof.context context_parser
   11.25    val theory: theory context_parser
   11.26    val $$$ : string -> string parser
   11.27 @@ -62,67 +52,13 @@
   11.28    val type_name: {proper: bool, strict: bool} -> string context_parser
   11.29    val const: {proper: bool, strict: bool} -> string context_parser
   11.30    val goal_spec: ((int -> tactic) -> tactic) context_parser
   11.31 -  val attribs: (xstring * Position.T -> string) -> src list parser
   11.32 -  val opt_attribs: (xstring * Position.T -> string) -> src list parser
   11.33 -  val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   11.34 -  val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
   11.35 +  val attribs: (xstring * Position.T -> string) -> Token.src list parser
   11.36 +  val opt_attribs: (xstring * Position.T -> string) -> Token.src list parser
   11.37  end;
   11.38  
   11.39  structure Args: ARGS =
   11.40  struct
   11.41  
   11.42 -(** datatype src **)
   11.43 -
   11.44 -datatype src =
   11.45 -  Src of
   11.46 -   {name: string * Position.T,
   11.47 -    args: Token.T list,
   11.48 -    output_info: (string * Markup.T) option};
   11.49 -
   11.50 -fun src name args = Src {name = name, args = args, output_info = NONE};
   11.51 -
   11.52 -fun name_of_src (Src {name, ...}) = name;
   11.53 -
   11.54 -fun range_of_src (Src {name = (_, pos), args, ...}) =
   11.55 -  if null args then pos
   11.56 -  else Position.set_range (pos, #2 (Token.range_of args));
   11.57 -
   11.58 -fun unparse_src (Src {args, ...}) = map Token.unparse args;
   11.59 -
   11.60 -fun pretty_src ctxt src =
   11.61 -  let
   11.62 -    val Src {name = (name, _), args, output_info} = src;
   11.63 -    val prt_name =
   11.64 -      (case output_info of
   11.65 -        NONE => Pretty.str name
   11.66 -      | SOME (_, markup) => Pretty.mark_str (markup, name));
   11.67 -    val prt_arg = Token.pretty_value ctxt;
   11.68 -  in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
   11.69 -
   11.70 -
   11.71 -(* check *)
   11.72 -
   11.73 -fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
   11.74 -  let
   11.75 -    val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
   11.76 -    val space = Name_Space.space_of_table table;
   11.77 -    val kind = Name_Space.kind_of space;
   11.78 -    val markup = Name_Space.markup space name;
   11.79 -  in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
   11.80 -
   11.81 -
   11.82 -(* values *)
   11.83 -
   11.84 -fun map_args f (Src {name, args, output_info}) =
   11.85 -  Src {name = name, args = map f args, output_info = output_info};
   11.86 -
   11.87 -val transform_values = map_args o Token.transform_value;
   11.88 -
   11.89 -val init_assignable = map_args Token.init_assignable;
   11.90 -val closure = map_args Token.closure;
   11.91 -
   11.92 -
   11.93 -
   11.94  (** argument scanners **)
   11.95  
   11.96  (* context *)
   11.97 @@ -251,42 +187,9 @@
   11.98    let
   11.99      fun intern tok = check (Token.content_of tok, Token.pos_of tok);
  11.100      val attrib_name = internal_name >> #1 || (symbolic || named) >> evaluate Token.name0 intern;
  11.101 -    val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry src;
  11.102 +    val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry Token.src;
  11.103    in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
  11.104  
  11.105  fun opt_attribs check = Scan.optional (attribs check) [];
  11.106  
  11.107 -
  11.108 -
  11.109 -(** syntax wrapper **)
  11.110 -
  11.111 -fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
  11.112 -  let
  11.113 -    val args1 = map Token.init_assignable args0;
  11.114 -    fun reported_text () =
  11.115 -      if Context_Position.is_visible_generic context then
  11.116 -        ((pos, Markup.operator) :: maps (Token.reports_of_value o Token.closure) args1)
  11.117 -        |> map (fn (p, m) => Position.reported_text p m "")
  11.118 -      else [];
  11.119 -  in
  11.120 -    (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
  11.121 -      (SOME x, (context', [])) =>
  11.122 -        let val _ = Output.report (reported_text ())
  11.123 -        in (x, context') end
  11.124 -    | (_, (_, args2)) =>
  11.125 -        let
  11.126 -          val print_name =
  11.127 -            (case output_info of
  11.128 -              NONE => quote name
  11.129 -            | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
  11.130 -          val print_args =
  11.131 -            if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2);
  11.132 -        in
  11.133 -          error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
  11.134 -            Markup.markup_report (implode (reported_text ())))
  11.135 -        end)
  11.136 -  end;
  11.137 -
  11.138 -fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
  11.139 -
  11.140  end;
    12.1 --- a/src/Pure/Isar/attrib.ML	Tue Aug 19 18:21:29 2014 +0200
    12.2 +++ b/src/Pure/Isar/attrib.ML	Tue Aug 19 23:17:51 2014 +0200
    12.3 @@ -6,23 +6,22 @@
    12.4  
    12.5  signature ATTRIB =
    12.6  sig
    12.7 -  type src = Args.src
    12.8 -  type binding = binding * src list
    12.9 +  type binding = binding * Token.src list
   12.10    val empty_binding: binding
   12.11    val is_empty_binding: binding -> bool
   12.12    val print_attributes: Proof.context -> unit
   12.13 -  val define_global: Binding.binding -> (Args.src -> attribute) ->
   12.14 +  val define_global: Binding.binding -> (Token.src -> attribute) ->
   12.15      string -> theory -> string * theory
   12.16 -  val define: Binding.binding -> (Args.src -> attribute) ->
   12.17 +  val define: Binding.binding -> (Token.src -> attribute) ->
   12.18      string -> local_theory -> string * local_theory
   12.19    val check_name_generic: Context.generic -> xstring * Position.T -> string
   12.20    val check_name: Proof.context -> xstring * Position.T -> string
   12.21 -  val check_src: Proof.context -> src -> src
   12.22 -  val pretty_attribs: Proof.context -> src list -> Pretty.T list
   12.23 -  val attribute: Proof.context -> src -> attribute
   12.24 -  val attribute_global: theory -> src -> attribute
   12.25 -  val attribute_cmd: Proof.context -> src -> attribute
   12.26 -  val attribute_cmd_global: theory -> src -> attribute
   12.27 +  val check_src: Proof.context -> Token.src -> Token.src
   12.28 +  val pretty_attribs: Proof.context -> Token.src list -> Pretty.T list
   12.29 +  val attribute: Proof.context -> Token.src -> attribute
   12.30 +  val attribute_global: theory -> Token.src -> attribute
   12.31 +  val attribute_cmd: Proof.context -> Token.src -> attribute
   12.32 +  val attribute_cmd_global: theory -> Token.src -> attribute
   12.33    val map_specs: ('a list -> 'att list) ->
   12.34      (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
   12.35    val map_facts: ('a list -> 'att list) ->
   12.36 @@ -31,28 +30,28 @@
   12.37    val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
   12.38      (('c * 'a list) * ('b * 'a list) list) list ->
   12.39      (('c * 'att list) * ('fact * 'att list) list) list
   12.40 -  val global_notes: string -> (binding * (thm list * src list) list) list ->
   12.41 +  val global_notes: string -> (binding * (thm list * Token.src list) list) list ->
   12.42      theory -> (string * thm list) list * theory
   12.43 -  val local_notes: string -> (binding * (thm list * src list) list) list ->
   12.44 +  val local_notes: string -> (binding * (thm list * Token.src list) list) list ->
   12.45      Proof.context -> (string * thm list) list * Proof.context
   12.46 -  val generic_notes: string -> (binding * (thm list * src list) list) list ->
   12.47 +  val generic_notes: string -> (binding * (thm list * Token.src list) list) list ->
   12.48      Context.generic -> (string * thm list) list * Context.generic
   12.49 -  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   12.50 -  val attribute_syntax: attribute context_parser -> Args.src -> attribute
   12.51 +  val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
   12.52 +  val attribute_syntax: attribute context_parser -> Token.src -> attribute
   12.53    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   12.54    val local_setup: Binding.binding -> attribute context_parser -> string ->
   12.55      local_theory -> local_theory
   12.56    val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
   12.57      local_theory -> local_theory
   12.58 -  val internal: (morphism -> attribute) -> src
   12.59 +  val internal: (morphism -> attribute) -> Token.src
   12.60    val add_del: attribute -> attribute -> attribute context_parser
   12.61    val thm_sel: Facts.interval list parser
   12.62    val thm: thm context_parser
   12.63    val thms: thm list context_parser
   12.64    val multi_thm: thm list context_parser
   12.65    val partial_evaluation: Proof.context ->
   12.66 -    (binding * (thm list * Args.src list) list) list ->
   12.67 -    (binding * (thm list * Args.src list) list) list
   12.68 +    (binding * (thm list * Token.src list) list) list ->
   12.69 +    (binding * (thm list * Token.src list) list) list
   12.70    val print_options: Proof.context -> unit
   12.71    val config_bool: Binding.binding ->
   12.72      (Context.generic -> bool) -> bool Config.T * (theory -> theory)
   12.73 @@ -81,8 +80,7 @@
   12.74  
   12.75  (* source and bindings *)
   12.76  
   12.77 -type src = Args.src;
   12.78 -type binding = binding * src list;
   12.79 +type binding = binding * Token.src list;
   12.80  
   12.81  val empty_binding: binding = (Binding.empty, []);
   12.82  fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
   12.83 @@ -95,7 +93,7 @@
   12.84  
   12.85  structure Attributes = Generic_Data
   12.86  (
   12.87 -  type T = ((src -> attribute) * string) Name_Space.table;
   12.88 +  type T = ((Token.src -> attribute) * string) Name_Space.table;
   12.89    val empty : T = Name_Space.empty_table "attribute";
   12.90    val extend = I;
   12.91    fun merge data : T = Name_Space.merge_tables data;
   12.92 @@ -147,21 +145,21 @@
   12.93  val check_name = check_name_generic o Context.Proof;
   12.94  
   12.95  fun check_src ctxt src =
   12.96 - (Context_Position.report ctxt (Args.range_of_src src) Markup.language_attribute;
   12.97 -  #1 (Args.check_src ctxt (get_attributes ctxt) src));
   12.98 + (Context_Position.report ctxt (Token.range_of_src src) Markup.language_attribute;
   12.99 +  #1 (Token.check_src ctxt (get_attributes ctxt) src));
  12.100  
  12.101  
  12.102  (* pretty printing *)
  12.103  
  12.104  fun pretty_attribs _ [] = []
  12.105 -  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt) srcs)];
  12.106 +  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)];
  12.107  
  12.108  
  12.109  (* get attributes *)
  12.110  
  12.111  fun attribute_generic context =
  12.112    let val table = Attributes.get context
  12.113 -  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
  12.114 +  in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
  12.115  
  12.116  val attribute = attribute_generic o Context.Proof;
  12.117  val attribute_global = attribute_generic o Context.Theory;
  12.118 @@ -199,7 +197,7 @@
  12.119  (* attribute setup *)
  12.120  
  12.121  fun attribute_syntax scan src (context, th) =
  12.122 -  let val (a, context') = Args.syntax_generic scan src context in a (context', th) end;
  12.123 +  let val (a, context') = Token.syntax_generic scan src context in a (context', th) end;
  12.124  
  12.125  fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
  12.126  fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
  12.127 @@ -216,7 +214,7 @@
  12.128  
  12.129  (* internal attribute *)
  12.130  
  12.131 -fun internal att = Args.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
  12.132 +fun internal att = Token.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
  12.133  
  12.134  val _ = Theory.setup
  12.135    (setup (Binding.make ("attribute", @{here}))
  12.136 @@ -287,13 +285,13 @@
  12.137  
  12.138  fun apply_att src (context, th) =
  12.139    let
  12.140 -    val src1 = Args.init_assignable src;
  12.141 +    val src1 = Token.init_assignable_src src;
  12.142      val result = attribute_generic context src1 (context, th);
  12.143 -    val src2 = Args.closure src1;
  12.144 +    val src2 = Token.closure_src src1;
  12.145    in (src2, result) end;
  12.146  
  12.147  fun err msg src =
  12.148 -  let val (name, pos) = Args.name_of_src src
  12.149 +  let val (name, pos) = Token.name_of_src src
  12.150    in error (msg ^ " " ^ quote name ^ Position.here pos) end;
  12.151  
  12.152  fun eval src ((th, dyn), (decls, context)) =
    13.1 --- a/src/Pure/Isar/bundle.ML	Tue Aug 19 18:21:29 2014 +0200
    13.2 +++ b/src/Pure/Isar/bundle.ML	Tue Aug 19 23:17:51 2014 +0200
    13.3 @@ -6,13 +6,13 @@
    13.4  
    13.5  signature BUNDLE =
    13.6  sig
    13.7 -  type bundle = (thm list * Args.src list) list
    13.8 +  type bundle = (thm list * Token.src list) list
    13.9    val check: Proof.context -> xstring * Position.T -> string
   13.10    val get_bundle: Proof.context -> string -> bundle
   13.11    val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle
   13.12 -  val bundle: binding * (thm list * Args.src list) list ->
   13.13 +  val bundle: binding * (thm list * Token.src list) list ->
   13.14      (binding * typ option * mixfix) list -> local_theory -> local_theory
   13.15 -  val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
   13.16 +  val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
   13.17      (binding * string option * mixfix) list -> local_theory -> local_theory
   13.18    val includes: string list -> Proof.context -> Proof.context
   13.19    val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
   13.20 @@ -31,10 +31,10 @@
   13.21  
   13.22  (* maintain bundles *)
   13.23  
   13.24 -type bundle = (thm list * Args.src list) list;
   13.25 +type bundle = (thm list * Token.src list) list;
   13.26  
   13.27  fun transform_bundle phi : bundle -> bundle =
   13.28 -  map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts));
   13.29 +  map (fn (fact, atts) => (Morphism.fact phi fact, map (Token.transform_src phi) atts));
   13.30  
   13.31  structure Data = Generic_Data
   13.32  (
    14.1 --- a/src/Pure/Isar/calculation.ML	Tue Aug 19 18:21:29 2014 +0200
    14.2 +++ b/src/Pure/Isar/calculation.ML	Tue Aug 19 23:17:51 2014 +0200
    14.3 @@ -14,10 +14,10 @@
    14.4    val sym_del: attribute
    14.5    val symmetric: attribute
    14.6    val also: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
    14.7 -  val also_cmd: (Facts.ref * Attrib.src list) list option ->
    14.8 +  val also_cmd: (Facts.ref * Token.src list) list option ->
    14.9      bool -> Proof.state -> Proof.state Seq.result Seq.seq
   14.10    val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
   14.11 -  val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
   14.12 +  val finally_cmd: (Facts.ref * Token.src list) list option -> bool ->
   14.13      Proof.state -> Proof.state Seq.result Seq.seq
   14.14    val moreover: bool -> Proof.state -> Proof.state
   14.15    val ultimately: bool -> Proof.state -> Proof.state
    15.1 --- a/src/Pure/Isar/code.ML	Tue Aug 19 18:21:29 2014 +0200
    15.2 +++ b/src/Pure/Isar/code.ML	Tue Aug 19 23:17:51 2014 +0200
    15.3 @@ -49,13 +49,13 @@
    15.4    val add_nbe_eqn: thm -> theory -> theory
    15.5    val add_abs_eqn: thm -> theory -> theory
    15.6    val add_abs_eqn_attribute: attribute
    15.7 -  val add_abs_eqn_attrib: Attrib.src
    15.8 +  val add_abs_eqn_attrib: Token.src
    15.9    val add_default_eqn: thm -> theory -> theory
   15.10    val add_default_eqn_attribute: attribute
   15.11 -  val add_default_eqn_attrib: Attrib.src
   15.12 +  val add_default_eqn_attrib: Token.src
   15.13    val add_nbe_default_eqn: thm -> theory -> theory
   15.14    val add_nbe_default_eqn_attribute: attribute
   15.15 -  val add_nbe_default_eqn_attrib: Attrib.src
   15.16 +  val add_nbe_default_eqn_attrib: Token.src
   15.17    val del_eqn: thm -> theory -> theory
   15.18    val del_eqns: string -> theory -> theory
   15.19    val del_exception: string -> theory -> theory
    16.1 --- a/src/Pure/Isar/element.ML	Tue Aug 19 18:21:29 2014 +0200
    16.2 +++ b/src/Pure/Isar/element.ML	Tue Aug 19 23:17:51 2014 +0200
    16.3 @@ -17,18 +17,18 @@
    16.4      Constrains of (string * 'typ) list |
    16.5      Assumes of (Attrib.binding * ('term * 'term list) list) list |
    16.6      Defines of (Attrib.binding * ('term * 'term list)) list |
    16.7 -    Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list
    16.8 +    Notes of string * (Attrib.binding * ('fact * Token.src list) list) list
    16.9    type context = (string, string, Facts.ref) ctxt
   16.10    type context_i = (typ, term, thm list) ctxt
   16.11    val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b,
   16.12 -    pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} ->
   16.13 +    pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Token.src -> Token.src} ->
   16.14      ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
   16.15 -  val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
   16.16 +  val map_ctxt_attrib: (Token.src -> Token.src) ->
   16.17      ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
   16.18    val transform_ctxt: morphism -> context_i -> context_i
   16.19    val transform_facts: morphism ->
   16.20 -    (Attrib.binding * (thm list * Args.src list) list) list ->
   16.21 -    (Attrib.binding * (thm list * Args.src list) list) list
   16.22 +    (Attrib.binding * (thm list * Token.src list) list) list ->
   16.23 +    (Attrib.binding * (thm list * Token.src list) list) list
   16.24    val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
   16.25    val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
   16.26    val pretty_statement: Proof.context -> string -> thm -> Pretty.T
   16.27 @@ -78,7 +78,7 @@
   16.28    Constrains of (string * 'typ) list |
   16.29    Assumes of (Attrib.binding * ('term * 'term list) list) list |
   16.30    Defines of (Attrib.binding * ('term * 'term list)) list |
   16.31 -  Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list;
   16.32 +  Notes of string * (Attrib.binding * ('fact * Token.src list) list) list;
   16.33  
   16.34  type context = (string, string, Facts.ref) ctxt;
   16.35  type context_i = (typ, term, thm list) ctxt;
   16.36 @@ -103,7 +103,7 @@
   16.37    term = Morphism.term phi,
   16.38    pattern = Morphism.term phi,
   16.39    fact = Morphism.fact phi,
   16.40 -  attrib = Args.transform_values phi};
   16.41 +  attrib = Token.transform_src phi};
   16.42  
   16.43  fun transform_facts phi facts =
   16.44    Notes ("", facts) |> transform_ctxt phi |> (fn Notes (_, facts') => facts');
   16.45 @@ -509,14 +509,14 @@
   16.46  fun activate_i elem ctxt =
   16.47    let
   16.48      val elem' =
   16.49 -      (case map_ctxt_attrib Args.init_assignable elem of
   16.50 +      (case map_ctxt_attrib Token.init_assignable_src elem of
   16.51          Defines defs =>
   16.52            Defines (defs |> map (fn ((a, atts), (t, ps)) =>
   16.53              ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
   16.54                (t, ps))))
   16.55        | e => e);
   16.56      val ctxt' = Context.proof_map (init elem') ctxt;
   16.57 -  in (map_ctxt_attrib Args.closure elem', ctxt') end;
   16.58 +  in (map_ctxt_attrib Token.closure_src elem', ctxt') end;
   16.59  
   16.60  fun activate raw_elem ctxt =
   16.61    let val elem = raw_elem |> map_ctxt
    17.1 --- a/src/Pure/Isar/generic_target.ML	Tue Aug 19 18:21:29 2014 +0200
    17.2 +++ b/src/Pure/Isar/generic_target.ML	Tue Aug 19 23:17:51 2014 +0200
    17.3 @@ -23,9 +23,9 @@
    17.4      bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    17.5      (term * (string * thm)) * local_theory
    17.6    val notes:
    17.7 -    (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
    17.8 -      (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
    17.9 -    string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
   17.10 +    (string -> (Attrib.binding * (thm list * Token.src list) list) list ->
   17.11 +      (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
   17.12 +    string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
   17.13      (string * thm list) list * local_theory
   17.14    val abbrev: (string * bool -> binding * mixfix -> term ->
   17.15        term list * term list -> local_theory -> local_theory) ->
   17.16 @@ -35,8 +35,8 @@
   17.17    val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
   17.18      term list * term list -> local_theory -> (term * thm) * local_theory
   17.19    val theory_notes: string ->
   17.20 -    (Attrib.binding * (thm list * Args.src list) list) list ->
   17.21 -    (Attrib.binding * (thm list * Args.src list) list) list ->
   17.22 +    (Attrib.binding * (thm list * Token.src list) list) list ->
   17.23 +    (Attrib.binding * (thm list * Token.src list) list) list ->
   17.24      local_theory -> local_theory
   17.25    val theory_declaration: declaration -> local_theory -> local_theory
   17.26    val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
   17.27 @@ -46,8 +46,8 @@
   17.28  
   17.29    (* locale operations *)
   17.30    val locale_notes: string -> string ->
   17.31 -    (Attrib.binding * (thm list * Args.src list) list) list ->
   17.32 -    (Attrib.binding * (thm list * Args.src list) list) list ->
   17.33 +    (Attrib.binding * (thm list * Token.src list) list) list ->
   17.34 +    (Attrib.binding * (thm list * Token.src list) list) list ->
   17.35      local_theory -> local_theory
   17.36    val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
   17.37    val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
    18.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Aug 19 18:21:29 2014 +0200
    18.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Aug 19 23:17:51 2014 +0200
    18.3 @@ -16,7 +16,7 @@
    18.4    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
    18.5    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
    18.6    val oracle: bstring * Position.T -> Symbol_Pos.source -> theory -> theory
    18.7 -  val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
    18.8 +  val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
    18.9    val declaration: {syntax: bool, pervasive: bool} ->
   18.10      Symbol_Pos.source -> local_theory -> local_theory
   18.11    val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
   18.12 @@ -39,11 +39,11 @@
   18.13    val thy_deps: Toplevel.transition -> Toplevel.transition
   18.14    val locale_deps: Toplevel.transition -> Toplevel.transition
   18.15    val class_deps: Toplevel.transition -> Toplevel.transition
   18.16 -  val print_stmts: string list * (Facts.ref * Attrib.src list) list
   18.17 +  val print_stmts: string list * (Facts.ref * Token.src list) list
   18.18      -> Toplevel.transition -> Toplevel.transition
   18.19 -  val print_thms: string list * (Facts.ref * Attrib.src list) list
   18.20 +  val print_thms: string list * (Facts.ref * Token.src list) list
   18.21      -> Toplevel.transition -> Toplevel.transition
   18.22 -  val print_prfs: bool -> string list * (Facts.ref * Attrib.src list) list option
   18.23 +  val print_prfs: bool -> string list * (Facts.ref * Token.src list) list option
   18.24      -> Toplevel.transition -> Toplevel.transition
   18.25    val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
   18.26    val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
    19.1 --- a/src/Pure/Isar/local_theory.ML	Tue Aug 19 18:21:29 2014 +0200
    19.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Aug 19 23:17:51 2014 +0200
    19.3 @@ -9,8 +9,7 @@
    19.4  
    19.5  structure Attrib =
    19.6  struct
    19.7 -  type src = Args.src;
    19.8 -  type binding = binding * src list;
    19.9 +  type binding = binding * Token.src list;
   19.10  end;
   19.11  
   19.12  signature LOCAL_THEORY =
   19.13 @@ -49,9 +48,9 @@
   19.14    val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
   19.15      (term * (string * thm)) * local_theory
   19.16    val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   19.17 -  val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
   19.18 +  val notes: (Attrib.binding * (thm list * Token.src list) list) list ->
   19.19      local_theory -> (string * thm list) list * local_theory
   19.20 -  val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   19.21 +  val notes_kind: string -> (Attrib.binding * (thm list * Token.src list) list) list ->
   19.22      local_theory -> (string * thm list) list * local_theory
   19.23    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
   19.24      (term * term) * local_theory
   19.25 @@ -87,7 +86,7 @@
   19.26   {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
   19.27      (term * (string * thm)) * local_theory,
   19.28    notes: string ->
   19.29 -    (Attrib.binding * (thm list * Attrib.src list) list) list ->
   19.30 +    (Attrib.binding * (thm list * Token.src list) list) list ->
   19.31      local_theory -> (string * thm list) list * local_theory,
   19.32    abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
   19.33      (term * term) * local_theory,
    20.1 --- a/src/Pure/Isar/locale.ML	Tue Aug 19 18:21:29 2014 +0200
    20.2 +++ b/src/Pure/Isar/locale.ML	Tue Aug 19 23:17:51 2014 +0200
    20.3 @@ -34,7 +34,7 @@
    20.4      term option * term list ->
    20.5      thm option * thm option -> thm list ->
    20.6      declaration list ->
    20.7 -    (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
    20.8 +    (string * (Attrib.binding * (thm list * Token.src list) list) list) list ->
    20.9      (string * morphism) list -> theory -> theory
   20.10    val intern: theory -> xstring -> string
   20.11    val check: theory -> xstring * Position.T -> string
   20.12 @@ -49,7 +49,7 @@
   20.13    val specification_of: theory -> string -> term option * term list
   20.14  
   20.15    (* Storing results *)
   20.16 -  val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   20.17 +  val add_thmss: string -> string -> (Attrib.binding * (thm list * Token.src list) list) list ->
   20.18      Proof.context -> Proof.context
   20.19    val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
   20.20  
   20.21 @@ -127,7 +127,7 @@
   20.22    (** dynamic part **)
   20.23    syntax_decls: (declaration * serial) list,
   20.24      (* syntax declarations *)
   20.25 -  notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
   20.26 +  notes: ((string * (Attrib.binding * (thm list * Token.src list) list) list) * serial) list,
   20.27      (* theorem declarations *)
   20.28    dependencies: ((string * (morphism * morphism)) * serial) list
   20.29      (* locale dependencies (sublocale relation) in reverse order *),
    21.1 --- a/src/Pure/Isar/method.ML	Tue Aug 19 18:21:29 2014 +0200
    21.2 +++ b/src/Pure/Isar/method.ML	Tue Aug 19 23:17:51 2014 +0200
    21.3 @@ -41,15 +41,14 @@
    21.4    val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
    21.5    val tactic: Symbol_Pos.source -> Proof.context -> method
    21.6    val raw_tactic: Symbol_Pos.source -> Proof.context -> method
    21.7 -  type src = Args.src
    21.8    type combinator_info
    21.9    val no_combinator_info: combinator_info
   21.10    datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int
   21.11    datatype text =
   21.12 -    Source of src |
   21.13 +    Source of Token.src |
   21.14      Basic of Proof.context -> method |
   21.15      Combinator of combinator_info * combinator * text list
   21.16 -  val map_source: (src -> src) -> text -> text
   21.17 +  val map_source: (Token.src -> Token.src) -> text -> text
   21.18    val primitive_text: (Proof.context -> thm -> thm) -> text
   21.19    val succeed_text: text
   21.20    val default_text: text
   21.21 @@ -59,15 +58,16 @@
   21.22    val finish_text: text option * bool -> text
   21.23    val print_methods: Proof.context -> unit
   21.24    val check_name: Proof.context -> xstring * Position.T -> string
   21.25 -  val method_syntax: (Proof.context -> method) context_parser -> Args.src -> Proof.context -> method
   21.26 +  val method_syntax: (Proof.context -> method) context_parser ->
   21.27 +    Token.src -> Proof.context -> method
   21.28    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
   21.29    val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
   21.30      local_theory -> local_theory
   21.31    val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
   21.32      local_theory -> local_theory
   21.33 -  val method: Proof.context -> src -> Proof.context -> method
   21.34 -  val method_closure: Proof.context -> src -> src
   21.35 -  val method_cmd: Proof.context -> src -> Proof.context -> method
   21.36 +  val method: Proof.context -> Token.src -> Proof.context -> method
   21.37 +  val method_closure: Proof.context -> Token.src -> Token.src
   21.38 +  val method_cmd: Proof.context -> Token.src -> Proof.context -> method
   21.39    val evaluate: text -> Proof.context -> method
   21.40    type modifier = (Proof.context -> Proof.context) * attribute
   21.41    val section: modifier parser list -> thm list context_parser
   21.42 @@ -274,8 +274,6 @@
   21.43  
   21.44  (* method text *)
   21.45  
   21.46 -type src = Args.src;
   21.47 -
   21.48  datatype combinator_info = Combinator_Info of {keywords: Position.T list};
   21.49  fun combinator_info keywords = Combinator_Info {keywords = keywords};
   21.50  val no_combinator_info = combinator_info [];
   21.51 @@ -283,7 +281,7 @@
   21.52  datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int;
   21.53  
   21.54  datatype text =
   21.55 -  Source of src |
   21.56 +  Source of Token.src |
   21.57    Basic of Proof.context -> method |
   21.58    Combinator of combinator_info * combinator * text list;
   21.59  
   21.60 @@ -293,7 +291,7 @@
   21.61  
   21.62  fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
   21.63  val succeed_text = Basic (K succeed);
   21.64 -val default_text = Source (Args.src ("default", Position.none) []);
   21.65 +val default_text = Source (Token.src ("default", Position.none) []);
   21.66  val this_text = Basic (K this);
   21.67  val done_text = Basic (K (SIMPLE_METHOD all_tac));
   21.68  fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
   21.69 @@ -307,7 +305,7 @@
   21.70  
   21.71  structure Methods = Generic_Data
   21.72  (
   21.73 -  type T = ((src -> Proof.context -> method) * string) Name_Space.table;
   21.74 +  type T = ((Token.src -> Proof.context -> method) * string) Name_Space.table;
   21.75    val empty : T = Name_Space.empty_table "method";
   21.76    val extend = I;
   21.77    fun merge data : T = Name_Space.merge_tables data;
   21.78 @@ -354,13 +352,13 @@
   21.79  (* check *)
   21.80  
   21.81  fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
   21.82 -fun check_src ctxt src = Args.check_src ctxt (get_methods ctxt) src;
   21.83 +fun check_src ctxt src = Token.check_src ctxt (get_methods ctxt) src;
   21.84  
   21.85  
   21.86  (* method setup *)
   21.87  
   21.88  fun method_syntax scan src ctxt : method =
   21.89 -  let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end;
   21.90 +  let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end;
   21.91  
   21.92  fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
   21.93  fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
   21.94 @@ -379,15 +377,15 @@
   21.95  
   21.96  fun method ctxt =
   21.97    let val table = get_methods ctxt
   21.98 -  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
   21.99 +  in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
  21.100  
  21.101  fun method_closure ctxt0 src0 =
  21.102    let
  21.103      val (src1, meth) = check_src ctxt0 src0;
  21.104 -    val src2 = Args.init_assignable src1;
  21.105 +    val src2 = Token.init_assignable_src src1;
  21.106      val ctxt = Context_Position.not_really ctxt0;
  21.107      val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm));
  21.108 -  in Args.closure src2 end;
  21.109 +  in Token.closure_src src2 end;
  21.110  
  21.111  fun method_cmd ctxt = method ctxt o method_closure ctxt;
  21.112  
  21.113 @@ -505,9 +503,9 @@
  21.114  local
  21.115  
  21.116  fun meth4 x =
  21.117 - (Parse.position Parse.xname >> (fn name => Source (Args.src name [])) ||
  21.118 + (Parse.position Parse.xname >> (fn name => Source (Token.src name [])) ||
  21.119    Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
  21.120 -    Source (Args.src ("cartouche", Token.pos_of tok) [tok])) ||
  21.121 +    Source (Token.src ("cartouche", Token.pos_of tok) [tok])) ||
  21.122    Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
  21.123  and meth3 x =
  21.124   (meth4 -- Parse.position (Parse.$$$ "?")
  21.125 @@ -520,7 +518,7 @@
  21.126          Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
  21.127    meth4) x
  21.128  and meth2 x =
  21.129 - (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Args.src) ||
  21.130 + (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) ||
  21.131    meth3) x
  21.132  and meth1 x =
  21.133    (Parse.enum1_positions "," meth2
    22.1 --- a/src/Pure/Isar/parse.ML	Tue Aug 19 18:21:29 2014 +0200
    22.2 +++ b/src/Pure/Isar/parse.ML	Tue Aug 19 23:17:51 2014 +0200
    22.3 @@ -6,8 +6,6 @@
    22.4  
    22.5  signature PARSE =
    22.6  sig
    22.7 -  type 'a parser = Token.T list -> 'a * Token.T list
    22.8 -  type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
    22.9    val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
   22.10    val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
   22.11    val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
   22.12 @@ -114,10 +112,6 @@
   22.13  structure Parse: PARSE =
   22.14  struct
   22.15  
   22.16 -type 'a parser = Token.T list -> 'a * Token.T list;
   22.17 -type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list);
   22.18 -
   22.19 -
   22.20  (** error handling **)
   22.21  
   22.22  (* group atomic parsers (no cuts!) *)
   22.23 @@ -441,6 +435,3 @@
   22.24  
   22.25  end;
   22.26  
   22.27 -type 'a parser = 'a Parse.parser;
   22.28 -type 'a context_parser = 'a Parse.context_parser;
   22.29 -
    23.1 --- a/src/Pure/Isar/parse_spec.ML	Tue Aug 19 18:21:29 2014 +0200
    23.2 +++ b/src/Pure/Isar/parse_spec.ML	Tue Aug 19 23:17:51 2014 +0200
    23.3 @@ -6,17 +6,17 @@
    23.4  
    23.5  signature PARSE_SPEC =
    23.6  sig
    23.7 -  val attribs: Attrib.src list parser
    23.8 -  val opt_attribs: Attrib.src list parser
    23.9 +  val attribs: Token.src list parser
   23.10 +  val opt_attribs: Token.src list parser
   23.11    val thm_name: string -> Attrib.binding parser
   23.12    val opt_thm_name: string -> Attrib.binding parser
   23.13    val spec: (Attrib.binding * string) parser
   23.14    val specs: (Attrib.binding * string list) parser
   23.15    val alt_specs: (Attrib.binding * string) list parser
   23.16    val where_alt_specs: (Attrib.binding * string) list parser
   23.17 -  val xthm: (Facts.ref * Attrib.src list) parser
   23.18 -  val xthms1: (Facts.ref * Attrib.src list) list parser
   23.19 -  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
   23.20 +  val xthm: (Facts.ref * Token.src list) parser
   23.21 +  val xthms1: (Facts.ref * Token.src list) list parser
   23.22 +  val name_facts: (Attrib.binding * (Facts.ref * Token.src list) list) list parser
   23.23    val constdecl: (binding * string option * mixfix) parser
   23.24    val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
   23.25    val includes: (xstring * Position.T) list parser
   23.26 @@ -37,7 +37,7 @@
   23.27  
   23.28  (* theorem specifications *)
   23.29  
   23.30 -val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Args.src;
   23.31 +val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Token.src;
   23.32  val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
   23.33  val opt_attribs = Scan.optional attribs [];
   23.34  
    24.1 --- a/src/Pure/Isar/proof.ML	Tue Aug 19 18:21:29 2014 +0200
    24.2 +++ b/src/Pure/Isar/proof.ML	Tue Aug 19 23:17:51 2014 +0200
    24.3 @@ -61,18 +61,18 @@
    24.4    val chain: state -> state
    24.5    val chain_facts: thm list -> state -> state
    24.6    val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
    24.7 -  val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
    24.8 +  val note_thmss_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list -> state -> state
    24.9    val from_thmss: ((thm list * attribute list) list) list -> state -> state
   24.10 -  val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   24.11 +  val from_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
   24.12    val with_thmss: ((thm list * attribute list) list) list -> state -> state
   24.13 -  val with_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   24.14 +  val with_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
   24.15    val using: ((thm list * attribute list) list) list -> state -> state
   24.16 -  val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   24.17 +  val using_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
   24.18    val unfolding: ((thm list * attribute list) list) list -> state -> state
   24.19 -  val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   24.20 +  val unfolding_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
   24.21    val invoke_case: (string * Position.T) * binding option list * attribute list ->
   24.22      state -> state
   24.23 -  val invoke_case_cmd: (string * Position.T) * binding option list * Attrib.src list ->
   24.24 +  val invoke_case_cmd: (string * Position.T) * binding option list * Token.src list ->
   24.25      state -> state
   24.26    val begin_block: state -> state
   24.27    val next_block: state -> state
    25.1 --- a/src/Pure/Isar/specification.ML	Tue Aug 19 18:21:29 2014 +0200
    25.2 +++ b/src/Pure/Isar/specification.ML	Tue Aug 19 23:17:51 2014 +0200
    25.3 @@ -51,11 +51,11 @@
    25.4    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    25.5    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    25.6    val theorems: string ->
    25.7 -    (Attrib.binding * (thm list * Attrib.src list) list) list ->
    25.8 +    (Attrib.binding * (thm list * Token.src list) list) list ->
    25.9      (binding * typ option * mixfix) list ->
   25.10      bool -> local_theory -> (string * thm list) list * local_theory
   25.11    val theorems_cmd: string ->
   25.12 -    (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
   25.13 +    (Attrib.binding * (Facts.ref * Token.src list) list) list ->
   25.14      (binding * string option * mixfix) list ->
   25.15      bool -> local_theory -> (string * thm list) list * local_theory
   25.16    val theorem: string -> Method.text option ->
    26.1 --- a/src/Pure/Isar/token.ML	Tue Aug 19 18:21:29 2014 +0200
    26.2 +++ b/src/Pure/Isar/token.ML	Tue Aug 19 23:17:51 2014 +0200
    26.3 @@ -66,10 +66,22 @@
    26.4    val mk_term: term -> T
    26.5    val mk_fact: string option * thm list -> T
    26.6    val mk_attribute: (morphism -> attribute) -> T
    26.7 -  val transform_value: morphism -> T -> T
    26.8 +  val transform: morphism -> T -> T
    26.9    val init_assignable: T -> T
   26.10    val assign: value option -> T -> unit
   26.11    val closure: T -> T
   26.12 +
   26.13 +  type src
   26.14 +  val src: xstring * Position.T -> T list -> src
   26.15 +  val name_of_src: src -> string * Position.T
   26.16 +  val range_of_src: src -> Position.T
   26.17 +  val unparse_src: src -> string list
   26.18 +  val pretty_src: Proof.context -> src -> Pretty.T
   26.19 +  val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
   26.20 +  val transform_src: morphism -> src -> src
   26.21 +  val init_assignable_src: src -> src
   26.22 +  val closure_src: src -> src
   26.23 +
   26.24    val ident_or_symbolic: string -> bool
   26.25    val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
   26.26    val source': {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
   26.27 @@ -78,6 +90,11 @@
   26.28      Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
   26.29        (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   26.30    val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
   26.31 +
   26.32 +  type 'a parser = T list -> 'a * T list
   26.33 +  type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
   26.34 +  val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   26.35 +  val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
   26.36  end;
   26.37  
   26.38  structure Token: TOKEN =
   26.39 @@ -378,7 +395,7 @@
   26.40  
   26.41  (* transform value *)
   26.42  
   26.43 -fun transform_value phi =
   26.44 +fun transform phi =
   26.45    map_value (fn v =>
   26.46      (case v of
   26.47        Literal _ => v
   26.48 @@ -407,6 +424,58 @@
   26.49  
   26.50  
   26.51  
   26.52 +(** src **)
   26.53 +
   26.54 +datatype src =
   26.55 +  Src of
   26.56 +   {name: string * Position.T,
   26.57 +    args: T list,
   26.58 +    output_info: (string * Markup.T) option};
   26.59 +
   26.60 +fun src name args = Src {name = name, args = args, output_info = NONE};
   26.61 +
   26.62 +fun name_of_src (Src {name, ...}) = name;
   26.63 +
   26.64 +fun range_of_src (Src {name = (_, pos), args, ...}) =
   26.65 +  if null args then pos
   26.66 +  else Position.set_range (pos, #2 (range_of args));
   26.67 +
   26.68 +fun unparse_src (Src {args, ...}) = map unparse args;
   26.69 +
   26.70 +fun pretty_src ctxt src =
   26.71 +  let
   26.72 +    val Src {name = (name, _), args, output_info} = src;
   26.73 +    val prt_name =
   26.74 +      (case output_info of
   26.75 +        NONE => Pretty.str name
   26.76 +      | SOME (_, markup) => Pretty.mark_str (markup, name));
   26.77 +    val prt_arg = pretty_value ctxt;
   26.78 +  in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
   26.79 +
   26.80 +
   26.81 +(* check *)
   26.82 +
   26.83 +fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
   26.84 +  let
   26.85 +    val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
   26.86 +    val space = Name_Space.space_of_table table;
   26.87 +    val kind = Name_Space.kind_of space;
   26.88 +    val markup = Name_Space.markup space name;
   26.89 +  in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
   26.90 +
   26.91 +
   26.92 +(* values *)
   26.93 +
   26.94 +fun map_args f (Src {name, args, output_info}) =
   26.95 +  Src {name = name, args = map f args, output_info = output_info};
   26.96 +
   26.97 +val transform_src = map_args o transform;
   26.98 +
   26.99 +val init_assignable_src = map_args init_assignable;
  26.100 +val closure_src = map_args closure;
  26.101 +
  26.102 +
  26.103 +
  26.104  (** scanners **)
  26.105  
  26.106  open Basic_Symbol_Pos;
  26.107 @@ -546,4 +615,44 @@
  26.108        |> Source.exhaust;
  26.109    in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
  26.110  
  26.111 +
  26.112 +
  26.113 +(** parsers **)
  26.114 +
  26.115 +type 'a parser = T list -> 'a * T list;
  26.116 +type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
  26.117 +
  26.118 +fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
  26.119 +  let
  26.120 +    val args1 = map init_assignable args0;
  26.121 +    fun reported_text () =
  26.122 +      if Context_Position.is_visible_generic context then
  26.123 +        ((pos, Markup.operator) :: maps (reports_of_value o closure) args1)
  26.124 +        |> map (fn (p, m) => Position.reported_text p m "")
  26.125 +      else [];
  26.126 +  in
  26.127 +    (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of
  26.128 +      (SOME x, (context', [])) =>
  26.129 +        let val _ = Output.report (reported_text ())
  26.130 +        in (x, context') end
  26.131 +    | (_, (_, args2)) =>
  26.132 +        let
  26.133 +          val print_name =
  26.134 +            (case output_info of
  26.135 +              NONE => quote name
  26.136 +            | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
  26.137 +          val print_args =
  26.138 +            if null args2 then "" else ":\n  " ^ space_implode " " (map print args2);
  26.139 +        in
  26.140 +          error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
  26.141 +            Markup.markup_report (implode (reported_text ())))
  26.142 +        end)
  26.143 +  end;
  26.144 +
  26.145 +fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
  26.146 +
  26.147  end;
  26.148 +
  26.149 +type 'a parser = 'a Token.parser;
  26.150 +type 'a context_parser = 'a Token.context_parser;
  26.151 +
    27.1 --- a/src/Pure/ML/ml_antiquotation.ML	Tue Aug 19 18:21:29 2014 +0200
    27.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Tue Aug 19 23:17:51 2014 +0200
    27.3 @@ -8,7 +8,7 @@
    27.4  sig
    27.5    val variant: string -> Proof.context -> string * Proof.context
    27.6    val declaration: binding -> 'a context_parser ->
    27.7 -    (Args.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
    27.8 +    (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
    27.9      theory -> theory
   27.10    val inline: binding -> string context_parser -> theory -> theory
   27.11    val value: binding -> string context_parser -> theory -> theory
   27.12 @@ -40,7 +40,7 @@
   27.13  fun declaration name scan body =
   27.14    ML_Context.add_antiquotation name
   27.15      (fn src => fn orig_ctxt =>
   27.16 -      let val (x, _) = Args.syntax scan src orig_ctxt
   27.17 +      let val (x, _) = Token.syntax scan src orig_ctxt
   27.18        in body src x orig_ctxt end);
   27.19  
   27.20  fun inline name scan =
   27.21 @@ -62,7 +62,7 @@
   27.22      (fn src => fn () => fn ctxt =>
   27.23        let
   27.24          val (a, ctxt') = variant "position" ctxt;
   27.25 -        val (_, pos) = Args.name_of_src src;
   27.26 +        val (_, pos) = Token.name_of_src src;
   27.27          val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
   27.28          val body = "Isabelle." ^ a;
   27.29        in (K (env, body), ctxt') end) #>
    28.1 --- a/src/Pure/ML/ml_antiquotations.ML	Tue Aug 19 18:21:29 2014 +0200
    28.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Tue Aug 19 23:17:51 2014 +0200
    28.3 @@ -64,7 +64,7 @@
    28.4      (Scan.lift (Scan.optional Args.name "Output.writeln"))
    28.5        (fn src => fn output => fn ctxt =>
    28.6          let
    28.7 -          val (_, pos) = Args.name_of_src src;
    28.8 +          val (_, pos) = Token.name_of_src src;
    28.9            val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
   28.10            val env =
   28.11              "val " ^ a ^ ": string -> unit =\n\
    29.1 --- a/src/Pure/ML/ml_context.ML	Tue Aug 19 18:21:29 2014 +0200
    29.2 +++ b/src/Pure/ML/ml_context.ML	Tue Aug 19 23:17:51 2014 +0200
    29.3 @@ -14,7 +14,7 @@
    29.4    val exec: (unit -> unit) -> Context.generic -> Context.generic
    29.5    val check_antiquotation: Proof.context -> xstring * Position.T -> string
    29.6    type decl = Proof.context -> string * string
    29.7 -  val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
    29.8 +  val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
    29.9      theory -> theory
   29.10    val print_antiquotations: Proof.context -> unit
   29.11    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
   29.12 @@ -55,7 +55,7 @@
   29.13  type decl = Proof.context -> string * string;  (*final context -> ML env, ML body*)
   29.14  structure Antiquotations = Theory_Data
   29.15  (
   29.16 -  type T = (Args.src -> Proof.context -> decl * Proof.context) Name_Space.table;
   29.17 +  type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table;
   29.18    val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
   29.19    val extend = I;
   29.20    fun merge data : T = Name_Space.merge_tables data;
   29.21 @@ -75,7 +75,7 @@
   29.22    |> Pretty.writeln;
   29.23  
   29.24  fun apply_antiquotation src ctxt =
   29.25 -  let val (src', f) = Args.check_src ctxt (get_antiquotations ctxt) src
   29.26 +  let val (src', f) = Token.check_src ctxt (get_antiquotations ctxt) src
   29.27    in f src' ctxt end;
   29.28  
   29.29  
   29.30 @@ -85,7 +85,7 @@
   29.31  
   29.32  val antiq =
   29.33    Parse.!!! (Parse.position Parse.xname -- Parse.args --| Scan.ahead Parse.eof)
   29.34 -  >> uncurry Args.src;
   29.35 +  >> uncurry Token.src;
   29.36  
   29.37  val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
   29.38  
    30.1 --- a/src/Pure/ML/ml_thms.ML	Tue Aug 19 18:21:29 2014 +0200
    30.2 +++ b/src/Pure/ML/ml_thms.ML	Tue Aug 19 23:17:51 2014 +0200
    30.3 @@ -6,7 +6,7 @@
    30.4  
    30.5  signature ML_THMS =
    30.6  sig
    30.7 -  val the_attributes: Proof.context -> int -> Args.src list
    30.8 +  val the_attributes: Proof.context -> int -> Token.src list
    30.9    val the_thmss: Proof.context -> thm list list
   30.10    val get_stored_thms: unit -> thm list
   30.11    val get_stored_thm: unit -> thm
   30.12 @@ -25,7 +25,7 @@
   30.13  
   30.14  structure Data = Proof_Data
   30.15  (
   30.16 -  type T = Args.src list Inttab.table * thms list;
   30.17 +  type T = Token.src list Inttab.table * thms list;
   30.18    fun init _ = (Inttab.empty, []);
   30.19  );
   30.20  
    31.1 --- a/src/Pure/Thy/term_style.ML	Tue Aug 19 18:21:29 2014 +0200
    31.2 +++ b/src/Pure/Thy/term_style.ML	Tue Aug 19 23:17:51 2014 +0200
    31.3 @@ -35,8 +35,8 @@
    31.4  fun parse_single ctxt =
    31.5    Parse.position Parse.xname -- Parse.args >> (fn (name, args) =>
    31.6      let
    31.7 -      val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args);
    31.8 -      val (f, _) = Args.syntax (Scan.lift parse) src ctxt;
    31.9 +      val (src, parse) = Token.check_src ctxt (get_data ctxt) (Token.src name args);
   31.10 +      val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
   31.11      in f ctxt end);
   31.12  
   31.13  val parse = Args.context :|-- (fn ctxt => Scan.lift
    32.1 --- a/src/Pure/Thy/thy_output.ML	Tue Aug 19 18:21:29 2014 +0200
    32.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Aug 19 23:17:51 2014 +0200
    32.3 @@ -18,7 +18,7 @@
    32.4    val check_option: Proof.context -> xstring * Position.T -> string
    32.5    val print_antiquotations: Proof.context -> unit
    32.6    val antiquotation: binding -> 'a context_parser ->
    32.7 -    ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
    32.8 +    ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
    32.9        theory -> theory
   32.10    val boolean: string -> bool
   32.11    val integer: string -> int
   32.12 @@ -30,9 +30,9 @@
   32.13    val pretty_text: Proof.context -> string -> Pretty.T
   32.14    val pretty_term: Proof.context -> term -> Pretty.T
   32.15    val pretty_thm: Proof.context -> thm -> Pretty.T
   32.16 -  val str_of_source: Args.src -> string
   32.17 +  val str_of_source: Token.src -> string
   32.18    val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
   32.19 -    Args.src -> 'a list -> Pretty.T list
   32.20 +    Token.src -> 'a list -> Pretty.T list
   32.21    val output: Proof.context -> Pretty.T list -> string
   32.22    val verb_text: string -> string
   32.23  end;
   32.24 @@ -67,7 +67,7 @@
   32.25  structure Antiquotations = Theory_Data
   32.26  (
   32.27    type T =
   32.28 -    (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
   32.29 +    (Token.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
   32.30        (string -> Proof.context -> Proof.context) Name_Space.table;
   32.31    val empty : T =
   32.32      (Name_Space.empty_table Markup.document_antiquotationN,
   32.33 @@ -91,7 +91,7 @@
   32.34  fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
   32.35  
   32.36  fun command src state ctxt =
   32.37 -  let val (src', f) = Args.check_src ctxt (#1 (get_antiquotations ctxt)) src
   32.38 +  let val (src', f) = Token.check_src ctxt (#1 (get_antiquotations ctxt)) src
   32.39    in f src' state ctxt end;
   32.40  
   32.41  fun option ((xname, pos), s) ctxt =
   32.42 @@ -114,7 +114,7 @@
   32.43  fun antiquotation name scan body =
   32.44    add_command name
   32.45      (fn src => fn state => fn ctxt =>
   32.46 -      let val (x, ctxt') = Args.syntax scan src ctxt
   32.47 +      let val (x, ctxt') = Token.syntax scan src ctxt
   32.48        in body {source = src, state = state, context = ctxt'} x end);
   32.49  
   32.50  
   32.51 @@ -151,7 +151,7 @@
   32.52  val antiq =
   32.53    Parse.!!!
   32.54      (Parse.position Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
   32.55 -  >> (fn ((name, props), args) => (props, Args.src name args));
   32.56 +  >> (fn ((name, props), args) => (props, Token.src name args));
   32.57  
   32.58  end;
   32.59  
   32.60 @@ -534,7 +534,7 @@
   32.61  
   32.62  (* default output *)
   32.63  
   32.64 -val str_of_source = space_implode " " o Args.unparse_src;
   32.65 +val str_of_source = space_implode " " o Token.unparse_src;
   32.66  
   32.67  fun maybe_pretty_source pretty ctxt src xs =
   32.68    map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
   32.69 @@ -624,7 +624,7 @@
   32.70        Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
   32.71      (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
   32.72        let
   32.73 -        val prop_src = Args.src (Args.name_of_src source) [prop_token];
   32.74 +        val prop_src = Token.src (Token.name_of_src source) [prop_token];
   32.75  
   32.76          val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
   32.77          val _ = Context_Position.reports ctxt reports;
    33.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Aug 19 18:21:29 2014 +0200
    33.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Aug 19 23:17:51 2014 +0200
    33.3 @@ -32,8 +32,8 @@
    33.4    val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
    33.5      thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
    33.6    val add_datatype: string * string list -> (string * string list * mixfix) list list ->
    33.7 -    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
    33.8 -    (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
    33.9 +    (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list *
   33.10 +    (Facts.ref * Token.src list) list -> theory -> theory * inductive_result * datatype_result
   33.11  end;
   33.12  
   33.13  functor Add_datatype_def_Fun
    34.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Aug 19 18:21:29 2014 +0200
    34.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Aug 19 23:17:51 2014 +0200
    34.3 @@ -12,8 +12,8 @@
    34.4    val induct_tac: Proof.context -> string -> int -> tactic
    34.5    val exhaust_tac: Proof.context -> string -> int -> tactic
    34.6    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
    34.7 -  val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
    34.8 -    (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
    34.9 +  val rep_datatype: Facts.ref * Token.src list -> Facts.ref * Token.src list ->
   34.10 +    (Facts.ref * Token.src list) list -> (Facts.ref * Token.src list) list -> theory -> theory
   34.11    val setup: theory -> theory
   34.12  end;
   34.13  
    35.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Aug 19 18:21:29 2014 +0200
    35.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Aug 19 23:17:51 2014 +0200
    35.3 @@ -29,9 +29,9 @@
    35.4      ((binding * term) * attribute list) list ->
    35.5      thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
    35.6    val add_inductive: string list * string ->
    35.7 -    ((binding * string) * Attrib.src list) list ->
    35.8 -    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
    35.9 -    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
   35.10 +    ((binding * string) * Token.src list) list ->
   35.11 +    (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list *
   35.12 +    (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list ->
   35.13      theory -> theory * inductive_result
   35.14  end;
   35.15  
    36.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Aug 19 18:21:29 2014 +0200
    36.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Aug 19 23:17:51 2014 +0200
    36.3 @@ -8,7 +8,7 @@
    36.4  
    36.5  signature PRIMREC_PACKAGE =
    36.6  sig
    36.7 -  val add_primrec: ((binding * string) * Attrib.src list) list -> theory -> theory * thm list
    36.8 +  val add_primrec: ((binding * string) * Token.src list) list -> theory -> theory * thm list
    36.9    val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
   36.10  end;
   36.11