# HG changeset patch
# User wenzelm
# Date 1199311256 -3600
# Node ID 216c8e70d8049817102a1b0368ad5097dd363450
# Parent  11bec58fc289666e2737f283b08f8cb69fb36552
added properties;

diff -r 11bec58fc289 -r 216c8e70d804 src/Pure/Isar/outer_parse.ML
--- 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 *)