--- a/src/Pure/Isar/args.ML Thu Aug 14 21:06:07 2008 +0200
+++ b/src/Pure/Isar/args.ML Fri Aug 15 15:50:44 2008 +0200
@@ -32,6 +32,8 @@
val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
val mode: string -> 'a * T list -> bool * ('a * T list)
val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
+ val name_source: T list -> string * T list
+ val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
val name: T list -> string * T list
val alt_name: T list -> string * T list
val symbol: T list -> string * T list
@@ -164,6 +166,9 @@
fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
+val name_source = named >> T.source_of;
+val name_source_position = named >> T.source_position_of;
+
val name = named >> T.content_of;
val alt_name = alt_string >> T.content_of;
val symbol = symbolic >> T.content_of;