support for nested Token.src within Token.T;
tuned signature;

--- a/src/Pure/Isar/args.ML	Tue Aug 19 23:17:51 2014 +0200
+++ b/src/Pure/Isar/args.ML	Wed Aug 20 11:05:41 2014 +0200
@@ -33,11 +33,13 @@
   val symbol: string parser
   val liberal_name: string parser
   val var: indexname parser
+  val internal_source: Token.src parser
   val internal_name: (string * morphism) parser
   val internal_typ: typ parser
   val internal_term: term parser
   val internal_fact: thm list parser
   val internal_attribute: (morphism -> attribute) parser
+  val named_source: (Token.T -> Token.src) -> Token.src parser
   val named_typ: (string -> typ) -> typ parser
   val named_term: (string -> term) -> term parser
   val named_fact: (string -> string option * thm list) -> thm list parser
@@ -129,13 +131,16 @@
 fun evaluate mk eval arg =
   let val x = eval arg in (Token.assign (SOME (mk x)) arg; x) end;
 
+val internal_source = value (fn Token.Source src => src);
 val internal_name = value (fn Token.Name a => a);
 val internal_typ = value (fn Token.Typ T => T);
 val internal_term = value (fn Token.Term t => t);
 val internal_fact = value (fn Token.Fact (_, ths) => ths);
 val internal_attribute = value (fn Token.Attribute att => att);
 
-fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
+fun named_source read = internal_source || named >> evaluate Token.Source read;
+
+fun named_typ read = internal_typ || named >> evaluate Token.Typ (read o Token.inner_syntax_of);
 fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
 
 fun named_fact get =

--- a/src/Pure/Isar/token.ML	Tue Aug 19 23:17:51 2014 +0200
+++ b/src/Pure/Isar/token.ML	Wed Aug 20 11:05:41 2014 +0200
@@ -10,8 +10,12 @@
     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
     Error of string | Sync | EOF
+  val str_of_kind: kind -> string
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
+  type T
+  type src
   datatype value =
+    Source of src |
     Literal of bool * Markup.T |
     Name of string * morphism |
     Typ of typ |
@@ -20,10 +24,13 @@
     Attribute of morphism -> attribute |
     Files of file Exn.result list
   val name0: string -> value
-  type T
-  val str_of_kind: kind -> string
   val pos_of: T -> Position.T
   val range_of: T list -> Position.range
+  val src: xstring * Position.T -> T list -> src
+  val name_of_src: src -> string * Position.T
+  val args_of_src: src -> T list
+  val range_of_src: src -> Position.T
+  val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -53,8 +60,8 @@
   val report: T -> Position.report_text
   val markup: T -> Markup.T
   val unparse: T -> string
+  val unparse_src: src -> string list
   val print: T -> string
-  val pretty_value: Proof.context -> T -> Pretty.T
   val text_of: T -> string * string
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
@@ -67,21 +74,14 @@
   val mk_fact: string option * thm list -> T
   val mk_attribute: (morphism -> attribute) -> T
   val transform: morphism -> T -> T
+  val transform_src: morphism -> src -> src
   val init_assignable: T -> T
+  val init_assignable_src: src -> src
   val assign: value option -> T -> unit
   val closure: T -> T
-
-  type src
-  val src: xstring * Position.T -> T list -> src
-  val name_of_src: src -> string * Position.T
-  val range_of_src: src -> Position.T
-  val unparse_src: src -> string list
+  val closure_src: src -> src
+  val pretty_value: Proof.context -> T -> Pretty.T
   val pretty_src: Proof.context -> src -> Pretty.T
-  val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
-  val transform_src: morphism -> src -> src
-  val init_assignable_src: src -> src
-  val closure_src: src -> src
-
   val ident_or_symbolic: string -> bool
   val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
   val source': {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
@@ -90,7 +90,6 @@
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
-
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
@@ -102,41 +101,13 @@
 
 (** tokens **)
 
-(* token values *)
-
-(*The value slot assigns an (optional) internal value to a token,
-  usually as a side-effect of special scanner setup (see also
-  args.ML).  Note that an assignable ref designates an intermediate
-  state of internalization -- it is NOT meant to persist.*)
-
-type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T};
-
-datatype value =
-  Literal of bool * Markup.T |
-  Name of string * morphism |
-  Typ of typ |
-  Term of term |
-  Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
-  Attribute of morphism -> attribute |
-  Files of file Exn.result list;
-
-fun name0 a = Name (a, Morphism.identity);
-
-datatype slot =
-  Slot |
-  Value of value option |
-  Assignable of value option Unsynchronized.ref;
-
-
-(* datatype token *)
+(* token kind *)
 
 datatype kind =
   Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
   Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
   Error of string | Sync | EOF;
 
-datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
-
 val str_of_kind =
  fn Command => "command"
   | Keyword => "keyword"
@@ -162,6 +133,41 @@
 val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment];
 
 
+(* datatype token *)
+
+(*The value slot assigns an (optional) internal value to a token,
+  usually as a side-effect of special scanner setup (see also
+  args.ML).  Note that an assignable ref designates an intermediate
+  state of internalization -- it is NOT meant to persist.*)
+
+type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T};
+
+datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot
+
+and src =
+  Src of
+   {name: string * Position.T,
+    args: T list,
+    output_info: (string * Markup.T) option}
+
+and slot =
+  Slot |
+  Value of value option |
+  Assignable of value option Unsynchronized.ref
+
+and value =
+  Source of src |
+  Literal of bool * Markup.T |
+  Name of string * morphism |
+  Typ of typ |
+  Term of term |
+  Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
+  Attribute of morphism -> attribute |
+  Files of file Exn.result list;
+
+fun name0 a = Name (a, Morphism.identity);
+
+
 (* position *)
 
 fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
@@ -173,6 +179,29 @@
   | range_of [] = Position.no_range;
 
 
+(* src *)
+
+fun src name args = Src {name = name, args = args, output_info = NONE};
+
+fun map_args f (Src {name, args, output_info}) =
+  Src {name = name, args = map f args, output_info = output_info};
+
+fun name_of_src (Src {name, ...}) = name;
+fun args_of_src (Src {args, ...}) = args;
+
+fun range_of_src (Src {name = (_, pos), args, ...}) =
+  if null args then pos
+  else Position.set_range (pos, #2 (range_of args));
+
+fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
+  let
+    val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
+    val space = Name_Space.space_of_table table;
+    val kind = Name_Space.kind_of space;
+    val markup = Name_Space.markup space name;
+  in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
+
+
 (* control tokens *)
 
 fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
@@ -315,6 +344,8 @@
   | EOF => ""
   | _ => x);
 
+fun unparse_src (Src {args, ...}) = map unparse args;
+
 fun print tok = Markup.markup (markup tok) (unparse tok);
 
 fun text_of tok =
@@ -367,7 +398,54 @@
   | _ => []);
 
 
-(* pretty value *)
+(* make values *)
+
+fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
+
+val mk_name = mk_value "<name>" o name0;
+val mk_typ = mk_value "<typ>" o Typ;
+val mk_term = mk_value "<term>" o Term;
+val mk_fact = mk_value "<fact>" o Fact;
+val mk_attribute = mk_value "<attribute>" o Attribute;
+
+
+(* transform *)
+
+fun transform phi =
+  map_value (fn v =>
+    (case v of
+      Source src => Source (transform_src phi src)
+    | Literal _ => v
+    | Name (a, psi) => Name (a, psi $> phi)
+    | Typ T => Typ (Morphism.typ phi T)
+    | Term t => Term (Morphism.term phi t)
+    | Fact (a, ths) => Fact (a, Morphism.fact phi ths)
+    | Attribute att => Attribute (Morphism.transform phi att)
+    | Files _ => v))
+and transform_src phi = map_args (transform phi);
+
+
+(* static binding *)
+
+(*1st stage: initialize assignable slots*)
+fun init_assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
+  | init_assignable (tok as Token (_, _, Assignable r)) = (r := NONE; tok)
+  | init_assignable tok = tok;
+
+val init_assignable_src = map_args init_assignable;
+
+(*2nd stage: assign values as side-effect of scanning*)
+fun assign v (Token (_, _, Assignable r)) = r := v
+  | assign _ _ = ();
+
+(*3rd stage: static closure of final values*)
+fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
+  | closure tok = tok;
+
+val closure_src = map_args closure;
+
+
+(* pretty *)
 
 fun pretty_value ctxt tok =
   (case get_value tok of
@@ -381,67 +459,6 @@
       Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
   | _ => Pretty.mark_str (markup tok, unparse tok));
 
-
-(* make values *)
-
-fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
-
-val mk_name = mk_value "<name>" o name0;
-val mk_typ = mk_value "<typ>" o Typ;
-val mk_term = mk_value "<term>" o Term;
-val mk_fact = mk_value "<fact>" o Fact;
-val mk_attribute = mk_value "<attribute>" o Attribute;
-
-
-(* transform value *)
-
-fun transform phi =
-  map_value (fn v =>
-    (case v of
-      Literal _ => v
-    | Name (a, psi) => Name (a, psi $> phi)
-    | Typ T => Typ (Morphism.typ phi T)
-    | Term t => Term (Morphism.term phi t)
-    | Fact (a, ths) => Fact (a, Morphism.fact phi ths)
-    | Attribute att => Attribute (Morphism.transform phi att)
-    | Files _ => v));
-
-
-(* static binding *)
-
-(*1st stage: initialize assignable slots*)
-fun init_assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
-  | init_assignable (tok as Token (_, _, Assignable r)) = (r := NONE; tok)
-  | init_assignable tok = tok;
-
-(*2nd stage: assign values as side-effect of scanning*)
-fun assign v (Token (_, _, Assignable r)) = r := v
-  | assign _ _ = ();
-
-(*3rd stage: static closure of final values*)
-fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
-  | closure tok = tok;
-
-
-
-(** src **)
-
-datatype src =
-  Src of
-   {name: string * Position.T,
-    args: T list,
-    output_info: (string * Markup.T) option};
-
-fun src name args = Src {name = name, args = args, output_info = NONE};
-
-fun name_of_src (Src {name, ...}) = name;
-
-fun range_of_src (Src {name = (_, pos), args, ...}) =
-  if null args then pos
-  else Position.set_range (pos, #2 (range_of args));
-
-fun unparse_src (Src {args, ...}) = map unparse args;
-
 fun pretty_src ctxt src =
   let
     val Src {name = (name, _), args, output_info} = src;
@@ -453,29 +470,6 @@
   in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
 
 
-(* check *)
-
-fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
-  let
-    val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
-    val space = Name_Space.space_of_table table;
-    val kind = Name_Space.kind_of space;
-    val markup = Name_Space.markup space name;
-  in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
-
-
-(* values *)
-
-fun map_args f (Src {name, args, output_info}) =
-  Src {name = name, args = map f args, output_info = output_info};
-
-val transform_src = map_args o transform;
-
-val init_assignable_src = map_args init_assignable;
-val closure_src = map_args closure;
-
-
-
 (** scanners **)
 
 open Basic_Symbol_Pos;