21 val scan_int: string list -> string * string list |
21 val scan_int: string list -> string * string list |
22 val scan_hex: string list -> string * string list |
22 val scan_hex: string list -> string * string list |
23 val scan_bin: string list -> string * string list |
23 val scan_bin: string list -> string * string list |
24 val string_of_vname: indexname -> string |
24 val string_of_vname: indexname -> string |
25 val string_of_vname': indexname -> string |
25 val string_of_vname': indexname -> string |
26 val indexname: string -> indexname |
26 val read_indexname: string -> indexname |
27 val read_var: string -> term |
27 val read_var: string -> term |
28 val read_variable: string -> indexname option |
28 val read_variable: string -> indexname option |
29 val const: string -> term |
29 val const: string -> term |
30 val free: string -> term |
30 val free: string -> term |
31 val var: indexname -> term |
31 val var: indexname -> term |
32 val read_nat: string -> int option |
32 val read_nat: string -> int option |
|
33 val read_int: string -> int option |
33 val read_xnum: string -> IntInf.int |
34 val read_xnum: string -> IntInf.int |
34 val read_idents: string -> string list |
35 val read_idents: string -> string list |
35 val fixedN: string |
36 val fixedN: string |
36 val constN: string |
37 val constN: string |
37 end; |
38 end; |
359 |
360 |
360 val constN = "\\<^const>"; |
361 val constN = "\\<^const>"; |
361 val fixedN = "\\<^fixed>"; |
362 val fixedN = "\\<^fixed>"; |
362 |
363 |
363 |
364 |
364 (* read_nat *) |
365 (* read numbers *) |
365 |
366 |
366 fun read_nat s = |
367 local |
|
368 |
|
369 fun nat cs = |
367 Option.map (#1 o Library.read_int) |
370 Option.map (#1 o Library.read_int) |
368 (Scan.read Symbol.stopper scan_digits1 (Symbol.explode s)); |
371 (Scan.read Symbol.stopper scan_digits1 cs); |
|
372 |
|
373 in |
|
374 |
|
375 val read_nat = nat o Symbol.explode; |
|
376 |
|
377 fun read_int s = |
|
378 (case Symbol.explode s of |
|
379 "-" :: cs => Option.map ~ (nat cs) |
|
380 | cs => nat cs); |
|
381 |
|
382 end; |
369 |
383 |
370 |
384 |
371 (* read_xnum: hex/bin/decimal *) |
385 (* read_xnum: hex/bin/decimal *) |
372 |
386 |
373 local |
387 local |