src/Pure/Isar/value_parse.ML
changeset 30513 1796b8ea88aa
parent 29458 98d749ae5edc
child 32787 4271aab3aa4a
equal deleted inserted replaced
30512:17b2aad869fa 30513:1796b8ea88aa
     4 Outer syntax parsers for basic ML values.
     4 Outer syntax parsers for basic ML values.
     5 *)
     5 *)
     6 
     6 
     7 signature VALUE_PARSE =
     7 signature VALUE_PARSE =
     8 sig
     8 sig
     9   type 'a parser = 'a OuterParse.parser
       
    10   val comma: 'a parser -> 'a parser
     9   val comma: 'a parser -> 'a parser
    11   val equal: 'a parser -> 'a parser
    10   val equal: 'a parser -> 'a parser
    12   val parens: 'a parser -> 'a parser
    11   val parens: 'a parser -> 'a parser
    13   val pair: 'a parser -> 'b parser -> ('a * 'b) parser
    12   val pair: 'a parser -> 'b parser -> ('a * 'b) parser
    14   val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
    13   val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
    18 
    17 
    19 structure ValueParse: VALUE_PARSE =
    18 structure ValueParse: VALUE_PARSE =
    20 struct
    19 struct
    21 
    20 
    22 structure P = OuterParse;
    21 structure P = OuterParse;
    23 type 'a parser = 'a P.parser;
       
    24 
    22 
    25 
    23 
    26 (* syntax utilities *)
    24 (* syntax utilities *)
    27 
    25 
    28 fun comma p = P.$$$ "," |-- P.!!! p;
    26 fun comma p = P.$$$ "," |-- P.!!! p;