--- a/src/Pure/Isar/outer_parse.ML Wed Jan 02 23:00:54 2008 +0100
+++ b/src/Pure/Isar/outer_parse.ML Wed Jan 02 23:00:56 2008 +0100
@@ -49,6 +49,7 @@
val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
val and_list: (token list -> 'a * token list) -> token list -> 'a list * token list
val and_list1: (token list -> 'a * token list) -> token list -> 'a list * token list
+ val properties: token list -> Markup.property list * token list
val name: token list -> bstring * token list
val xname: token list -> xstring * token list
val text: token list -> string * token list
@@ -193,6 +194,8 @@
fun and_list1 scan = enum1 "and" scan;
fun and_list scan = enum "and" scan;
+val properties = $$$ "(" |-- !!! (list1 (string -- ($$$ "=" |-- string)) --| $$$ ")");
+
(* names and text *)