# HG changeset patch
# User wenzelm
# Date 1124192561 -7200
# Node ID 3b29a01417f8bcd57abc114d1c3856948a897761
# Parent  ee08b2466a093a796ca2457ab330b8ee5e709144
added tags parser;

diff -r ee08b2466a09 -r 3b29a01417f8 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Tue Aug 16 13:42:40 2005 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Tue Aug 16 13:42:41 2005 +0200
@@ -35,6 +35,8 @@
   val semicolon: token list -> string * token list
   val underscore: token list -> string * token list
   val maybe: (token list -> 'a * token list) -> token list -> 'a option * token list
+  val tag_name: token list -> string * token list
+  val tags: token list -> string list * token list
   val opt_unit: token list -> unit * token list
   val opt_keyword: string -> token list -> bool * token list
   val nat: token list -> int * token list
@@ -162,8 +164,10 @@
 
 val nat = number >> (#1 o Library.read_int o Symbol.explode);
 
+val tag_name = group "tag name" (short_ident || string);
+val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
+
 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
-
 fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;