# HG changeset patch
# User wenzelm
# Date 1117533211 -7200
# Node ID fc51e61d45fb4de32ed22ce6a2d4a432073b4052
# Parent  21ce46ca61cc6521b063bb0694e7d65c34d64fb7
added symbol scanner;

diff -r 21ce46ca61cc -r fc51e61d45fb src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue May 31 11:53:30 2005 +0200
+++ b/src/Pure/Isar/args.ML	Tue May 31 11:53:31 2005 +0200
@@ -46,6 +46,7 @@
   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: T list -> string * T list
+  val symbol: T list -> string * T list
   val nat: T list -> int * T list
   val int: T list -> int * T list
   val var: T list -> indexname * T list
@@ -232,7 +233,8 @@
   touch (Scan.one (fn Arg ((k, y, _), _) => k = Keyword andalso x = y));
 
 fun $$$ x =
-  touch (Scan.one (fn Arg ((k, y, _), _) => (k = Ident orelse k = Keyword) andalso x = y) >> sym_of);
+  touch (Scan.one (fn Arg ((k, y, _), _) => (k = Ident orelse k = Keyword) andalso x = y))
+  >> sym_of;
 
 val add = $$$ "add";
 val del = $$$ "del";
@@ -248,6 +250,7 @@
 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
 
 val name = named >> sym_of;
+val symbol = symbolic >> sym_of;
 
 val nat = some_ident Syntax.read_nat;
 val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;