# HG changeset patch
# User wenzelm
# Date 1310476370 -7200
# Node ID b361c7d184e7bfa7dd1edb89c5192088c88c7919
# Parent  6dfdb70496fece6db8d1b84de03932603e89943c
added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;

diff -r 6dfdb70496fe -r b361c7d184e7 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 12 14:54:29 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 12 15:12:50 2011 +0200
@@ -766,7 +766,7 @@
 (* nested commands *)
 
 val props_text =
-  Scan.optional Parse_Value.properties [] -- Parse.position Parse.string
+  Scan.optional Parse.properties [] -- Parse.position Parse.string
   >> (fn (props, (str, pos)) =>
       (Position.of_properties (Position.default_properties pos props), str));
 
diff -r 6dfdb70496fe -r b361c7d184e7 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue Jul 12 14:54:29 2011 +0200
+++ b/src/Pure/Isar/parse.ML	Tue Jul 12 15:12:50 2011 +0200
@@ -60,6 +60,7 @@
   val and_list1': 'a context_parser -> 'a list context_parser
   val list: 'a parser -> 'a list parser
   val list1: 'a parser -> 'a list parser
+  val properties: Properties.T parser
   val name: bstring parser
   val binding: binding parser
   val xname: xstring parser
@@ -230,6 +231,8 @@
 fun list1 scan = enum1 "," scan;
 fun list scan = enum "," scan;
 
+val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")");
+
 
 (* names and text *)