added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
--- 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));
--- 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 *)