added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
authorwenzelm
Tue Jul 12 15:12:50 2011 +0200 (2011-07-12)
changeset 43775b361c7d184e7
parent 43774 6dfdb70496fe
child 43776 6dd13e111d30
added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/parse.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jul 12 14:54:29 2011 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 12 15:12:50 2011 +0200
     1.3 @@ -766,7 +766,7 @@
     1.4  (* nested commands *)
     1.5  
     1.6  val props_text =
     1.7 -  Scan.optional Parse_Value.properties [] -- Parse.position Parse.string
     1.8 +  Scan.optional Parse.properties [] -- Parse.position Parse.string
     1.9    >> (fn (props, (str, pos)) =>
    1.10        (Position.of_properties (Position.default_properties pos props), str));
    1.11  
     2.1 --- a/src/Pure/Isar/parse.ML	Tue Jul 12 14:54:29 2011 +0200
     2.2 +++ b/src/Pure/Isar/parse.ML	Tue Jul 12 15:12:50 2011 +0200
     2.3 @@ -60,6 +60,7 @@
     2.4    val and_list1': 'a context_parser -> 'a list context_parser
     2.5    val list: 'a parser -> 'a list parser
     2.6    val list1: 'a parser -> 'a list parser
     2.7 +  val properties: Properties.T parser
     2.8    val name: bstring parser
     2.9    val binding: binding parser
    2.10    val xname: xstring parser
    2.11 @@ -230,6 +231,8 @@
    2.12  fun list1 scan = enum1 "," scan;
    2.13  fun list scan = enum "," scan;
    2.14  
    2.15 +val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")");
    2.16 +
    2.17  
    2.18  (* names and text *)
    2.19