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