1.1 --- a/src/Pure/Isar/args.ML	Thu Aug 14 21:06:07 2008 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Fri Aug 15 15:50:44 2008 +0200
     1.3 @@ -32,6 +32,8 @@
     1.4    val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
     1.5    val mode: string -> 'a * T list -> bool * ('a * T list)
     1.6    val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
     1.7 +  val name_source: T list -> string * T list
     1.8 +  val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
     1.9    val name: T list -> string * T list
    1.10    val alt_name: T list -> string * T list
    1.11    val symbol: T list -> string * T list
    1.12 @@ -164,6 +166,9 @@
    1.13  fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
    1.14  fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
    1.15  
    1.16 +val name_source = named >> T.source_of;
    1.17 +val name_source_position = named >> T.source_position_of;
    1.18 +
    1.19  val name = named >> T.content_of;
    1.20  val alt_name = alt_string >> T.content_of;
    1.21  val symbol = symbolic >> T.content_of;