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;
wenzelm@36951
     1
(*  Title:      Pure/Isar/parse_value.ML
wenzelm@29308
     2
    Author:     Makarius
wenzelm@29308
     3
wenzelm@29308
     4
Outer syntax parsers for basic ML values.
wenzelm@29308
     5
*)
wenzelm@29308
     6
wenzelm@36951
     7
signature PARSE_VALUE =
wenzelm@29308
     8
sig
wenzelm@29308
     9
  val comma: 'a parser -> 'a parser
wenzelm@29308
    10
  val equal: 'a parser -> 'a parser
wenzelm@29308
    11
  val parens: 'a parser -> 'a parser
wenzelm@32787
    12
  val unit: unit parser
wenzelm@29308
    13
  val pair: 'a parser -> 'b parser -> ('a * 'b) parser
wenzelm@29308
    14
  val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
wenzelm@29458
    15
  val list: 'a parser -> 'a list parser
wenzelm@29308
    16
  val properties: Properties.T parser
wenzelm@29308
    17
end;
wenzelm@29308
    18
wenzelm@36951
    19
structure Parse_Value: PARSE_VALUE =
wenzelm@29308
    20
struct
wenzelm@29308
    21
wenzelm@29308
    22
(* syntax utilities *)
wenzelm@29308
    23
wenzelm@36950
    24
fun comma p = Parse.$$$ "," |-- Parse.!!! p;
wenzelm@36950
    25
fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
wenzelm@36950
    26
fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
wenzelm@29308
    27
wenzelm@29308
    28
wenzelm@29308
    29
(* tuples *)
wenzelm@29308
    30
wenzelm@29308
    31
val unit = parens (Scan.succeed ());
wenzelm@29308
    32
fun pair p1 p2 = parens (p1 -- comma p2);
wenzelm@36950
    33
fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
wenzelm@29308
    34
wenzelm@29308
    35
wenzelm@29308
    36
(* lists *)
wenzelm@29308
    37
wenzelm@36950
    38
fun list p = parens (Parse.enum "," p);
wenzelm@36950
    39
val properties = list (Parse.string -- equal Parse.string);
wenzelm@29308
    40
wenzelm@29308
    41
end;
wenzelm@29308
    42