src/Pure/Isar/parse_value.ML
author wenzelm
Fri Apr 08 16:34:14 2011 +0200 (2011-04-08)
changeset 42290 b1f544c84040
parent 36951 985c197f2fe9
permissions -rw-r--r--
discontinued special treatment of structure Lexicon;
     1 (*  Title:      Pure/Isar/parse_value.ML
     2     Author:     Makarius
     3 
     4 Outer syntax parsers for basic ML values.
     5 *)
     6 
     7 signature PARSE_VALUE =
     8 sig
     9   val comma: 'a parser -> 'a parser
    10   val equal: 'a parser -> 'a parser
    11   val parens: 'a parser -> 'a parser
    12   val unit: unit parser
    13   val pair: 'a parser -> 'b parser -> ('a * 'b) parser
    14   val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
    15   val list: 'a parser -> 'a list parser
    16   val properties: Properties.T parser
    17 end;
    18 
    19 structure Parse_Value: PARSE_VALUE =
    20 struct
    21 
    22 (* syntax utilities *)
    23 
    24 fun comma p = Parse.$$$ "," |-- Parse.!!! p;
    25 fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
    26 fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
    27 
    28 
    29 (* tuples *)
    30 
    31 val unit = parens (Scan.succeed ());
    32 fun pair p1 p2 = parens (p1 -- comma p2);
    33 fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
    34 
    35 
    36 (* lists *)
    37 
    38 fun list p = parens (Parse.enum "," p);
    39 val properties = list (Parse.string -- equal Parse.string);
    40 
    41 end;
    42