added properties;
authorwenzelm
Wed Jan 02 23:00:56 2008 +0100 (2008-01-02 ago)
changeset 25795216c8e70d804
parent 25794 11bec58fc289
child 25796 5df3607867c1
added properties;
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Jan 02 23:00:54 2008 +0100
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Wed Jan 02 23:00:56 2008 +0100
     1.3 @@ -49,6 +49,7 @@
     1.4    val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
     1.5    val and_list: (token list -> 'a * token list) -> token list -> 'a list * token list
     1.6    val and_list1: (token list -> 'a * token list) -> token list -> 'a list * token list
     1.7 +  val properties: token list -> Markup.property list * token list
     1.8    val name: token list -> bstring * token list
     1.9    val xname: token list -> xstring * token list
    1.10    val text: token list -> string * token list
    1.11 @@ -193,6 +194,8 @@
    1.12  fun and_list1 scan = enum1 "and" scan;
    1.13  fun and_list scan = enum "and" scan;
    1.14  
    1.15 +val properties = $$$ "(" |-- !!! (list1 (string -- ($$$ "=" |-- string)) --| $$$ ")");
    1.16 +
    1.17  
    1.18  (* names and text *)
    1.19