src/Pure/Isar/attrib.ML

--- a/src/Pure/Isar/attrib.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -6,23 +6,22 @@
 
 signature ATTRIB =
 sig
-  type src = Args.src
-  type binding = binding * src list
+  type binding = binding * Token.src list
   val empty_binding: binding
   val is_empty_binding: binding -> bool
   val print_attributes: Proof.context -> unit
-  val define_global: Binding.binding -> (Args.src -> attribute) ->
+  val define_global: Binding.binding -> (Token.src -> attribute) ->
     string -> theory -> string * theory
-  val define: Binding.binding -> (Args.src -> attribute) ->
+  val define: Binding.binding -> (Token.src -> attribute) ->
     string -> local_theory -> string * local_theory
   val check_name_generic: Context.generic -> xstring * Position.T -> string
   val check_name: Proof.context -> xstring * Position.T -> string
-  val check_src: Proof.context -> src -> src
-  val pretty_attribs: Proof.context -> src list -> Pretty.T list
-  val attribute: Proof.context -> src -> attribute
-  val attribute_global: theory -> src -> attribute
-  val attribute_cmd: Proof.context -> src -> attribute
-  val attribute_cmd_global: theory -> src -> attribute
+  val check_src: Proof.context -> Token.src -> Token.src
+  val pretty_attribs: Proof.context -> Token.src list -> Pretty.T list
+  val attribute: Proof.context -> Token.src -> attribute
+  val attribute_global: theory -> Token.src -> attribute
+  val attribute_cmd: Proof.context -> Token.src -> attribute
+  val attribute_cmd_global: theory -> Token.src -> attribute
   val map_specs: ('a list -> 'att list) ->
     (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
   val map_facts: ('a list -> 'att list) ->
@@ -31,28 +30,28 @@
   val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
-  val global_notes: string -> (binding * (thm list * src list) list) list ->
+  val global_notes: string -> (binding * (thm list * Token.src list) list) list ->
     theory -> (string * thm list) list * theory
-  val local_notes: string -> (binding * (thm list * src list) list) list ->
+  val local_notes: string -> (binding * (thm list * Token.src list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
-  val generic_notes: string -> (binding * (thm list * src list) list) list ->
+  val generic_notes: string -> (binding * (thm list * Token.src list) list) list ->
     Context.generic -> (string * thm list) list * Context.generic
-  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
-  val attribute_syntax: attribute context_parser -> Args.src -> attribute
+  val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
+  val attribute_syntax: attribute context_parser -> Token.src -> attribute
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val local_setup: Binding.binding -> attribute context_parser -> string ->
     local_theory -> local_theory
   val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
     local_theory -> local_theory
-  val internal: (morphism -> attribute) -> src
+  val internal: (morphism -> attribute) -> Token.src
   val add_del: attribute -> attribute -> attribute context_parser
   val thm_sel: Facts.interval list parser
   val thm: thm context_parser
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
   val partial_evaluation: Proof.context ->
-    (binding * (thm list * Args.src list) list) list ->
-    (binding * (thm list * Args.src list) list) list
+    (binding * (thm list * Token.src list) list) list ->
+    (binding * (thm list * Token.src list) list) list
   val print_options: Proof.context -> unit
   val config_bool: Binding.binding ->
     (Context.generic -> bool) -> bool Config.T * (theory -> theory)
@@ -81,8 +80,7 @@
 
 (* source and bindings *)
 
-type src = Args.src;
-type binding = binding * src list;
+type binding = binding * Token.src list;
 
 val empty_binding: binding = (Binding.empty, []);
 fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
@@ -95,7 +93,7 @@
 
 structure Attributes = Generic_Data
 (
-  type T = ((src -> attribute) * string) Name_Space.table;
+  type T = ((Token.src -> attribute) * string) Name_Space.table;
   val empty : T = Name_Space.empty_table "attribute";
   val extend = I;
   fun merge data : T = Name_Space.merge_tables data;
@@ -147,21 +145,21 @@
 val check_name = check_name_generic o Context.Proof;
 
 fun check_src ctxt src =
- (Context_Position.report ctxt (Args.range_of_src src) Markup.language_attribute;
-  #1 (Args.check_src ctxt (get_attributes ctxt) src));
+ (Context_Position.report ctxt (Token.range_of_src src) Markup.language_attribute;
+  #1 (Token.check_src ctxt (get_attributes ctxt) src));
 
 
 (* pretty printing *)
 
 fun pretty_attribs _ [] = []
-  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt) srcs)];
+  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)];
 
 
 (* get attributes *)
 
 fun attribute_generic context =
   let val table = Attributes.get context
-  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
+  in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
 
 val attribute = attribute_generic o Context.Proof;
 val attribute_global = attribute_generic o Context.Theory;
@@ -199,7 +197,7 @@
 (* attribute setup *)
 
 fun attribute_syntax scan src (context, th) =
-  let val (a, context') = Args.syntax_generic scan src context in a (context', th) end;
+  let val (a, context') = Token.syntax_generic scan src context in a (context', th) end;
 
 fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
@@ -216,7 +214,7 @@
 
 (* internal attribute *)
 
-fun internal att = Args.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
+fun internal att = Token.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
 
 val _ = Theory.setup
   (setup (Binding.make ("attribute", @{here}))
@@ -287,13 +285,13 @@
 
 fun apply_att src (context, th) =
   let
-    val src1 = Args.init_assignable src;
+    val src1 = Token.init_assignable_src src;
     val result = attribute_generic context src1 (context, th);
-    val src2 = Args.closure src1;
+    val src2 = Token.closure_src src1;
   in (src2, result) end;
 
 fun err msg src =
-  let val (name, pos) = Args.name_of_src src
+  let val (name, pos) = Token.name_of_src src
   in error (msg ^ " " ^ quote name ^ Position.here pos) end;
 
 fun eval src ((th, dyn), (decls, context)) =