equal
deleted
inserted
replaced
|
1 (* Taken from ../Syntax/lexicon.ML, which otherwise pulls in whole |
|
2 term structure of Isabelle |
|
3 *) |
|
4 signature SYNTAX = |
|
5 sig |
|
6 val read_int: string -> int option |
|
7 val read_nat: string -> int option |
|
8 end |
|
9 |
|
10 structure Syntax : SYNTAX = |
|
11 struct |
|
12 |
|
13 local |
|
14 |
|
15 val scan_digits1 = Scan.many1 Symbol.is_digit; |
|
16 |
|
17 fun nat cs = |
|
18 Option.map (#1 o Library.read_int) |
|
19 (Scan.read Symbol.stopper scan_digits1 cs); |
|
20 |
|
21 in |
|
22 |
|
23 val read_nat = nat o Symbol.explode; |
|
24 |
|
25 fun read_int s = |
|
26 (case Symbol.explode s of |
|
27 "-" :: cs => Option.map ~ (nat cs) |
|
28 | cs => nat cs); |
|
29 |
|
30 end; |
|
31 |
|
32 end |
|
33 |