author | wenzelm |
Mon, 09 Nov 1998 15:34:41 +0100 | |
changeset 5831 | 996361157cfb |
parent 5822 | 3f824514ad88 |
child 5878 | 769abc29bb8e |
permissions | -rw-r--r-- |
5822
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/args.ML |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
4 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
5 |
Concrete argument syntax (for attributes, methods etc.). |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
6 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
7 |
TODO: |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
8 |
- sectioned: generalize sname to attributed thms; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
9 |
*) |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
10 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
11 |
signature ARGS = |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
12 |
sig |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
13 |
type T |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
14 |
val val_of: T -> string |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
15 |
val ident: string -> T |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
16 |
val string: string -> T |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
17 |
val keyword: string -> T |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
18 |
val stopper: T * (T -> bool) |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
19 |
val not_eof: T -> bool |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
20 |
val $$$ : string -> T list -> string * T list |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
21 |
val name: T list -> string * T list |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
22 |
val sectioned: string list -> T list -> (string list * (string * string list) list) * T list |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
23 |
type src |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
24 |
val syntax: string -> (T list -> 'a * T list) -> ('a -> 'b) -> src -> 'b |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
25 |
end; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
26 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
27 |
structure Args: ARGS = |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
28 |
struct |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
29 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
30 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
31 |
(** datatype T **) |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
32 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
33 |
datatype kind = Ident | String | Keyword | EOF; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
34 |
datatype T = Arg of kind * string; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
35 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
36 |
fun val_of (Arg (_, x)) = x; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
37 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
38 |
fun str_of (Arg (Ident, x)) = enclose "'" "'" x |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
39 |
| str_of (Arg (String, x)) = quote x |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
40 |
| str_of (Arg (Keyword, x)) = x; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
41 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
42 |
fun arg kind x = Arg (kind, x); |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
43 |
val ident = arg Ident; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
44 |
val string = arg String; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
45 |
val keyword = arg Keyword; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
46 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
47 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
48 |
(* eof *) |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
49 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
50 |
val eof = arg EOF ""; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
51 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
52 |
fun is_eof (Arg (EOF, _)) = true |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
53 |
| is_eof _ = false; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
54 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
55 |
val stopper = (eof, is_eof); |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
56 |
val not_eof = not o is_eof; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
57 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
58 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
59 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
60 |
(** scanners **) |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
61 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
62 |
(* basic *) |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
63 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
64 |
fun $$$ x = Scan.one (fn Arg (k, y) => (k = Ident orelse k = Keyword) andalso x = y) >> val_of; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
65 |
val name = Scan.one (fn (Arg (k, x)) => k = Ident orelse k = String) >> val_of; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
66 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
67 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
68 |
(* sections *) |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
69 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
70 |
val no_colon = Scan.one (fn Arg (k, x) => k = String orelse x <> ":"); |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
71 |
val sname = name --| Scan.ahead no_colon; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
72 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
73 |
fun sect s = ($$$ s --| $$$ ":") -- Scan.repeat sname; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
74 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
75 |
fun any_sect [] = Scan.fail |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
76 |
| any_sect (s :: ss) = sect s || any_sect ss; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
77 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
78 |
fun sectioned ss = |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
79 |
Scan.repeat sname -- Scan.repeat (any_sect ss); |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
80 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
81 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
82 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
83 |
(** type src **) |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
84 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
85 |
type src = (string * T list) * Position.T; |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
86 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
87 |
fun err_in_src kind msg ((s, args), pos) = |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
88 |
error (space_implode " " (kind :: s :: map str_of args) ^ Position.str_of pos ^ ": " ^ msg); |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
89 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
90 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
91 |
(* argument syntax *) |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
92 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
93 |
fun syntax kind scan f (src as ((s, args), pos)) = |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
94 |
(case handle_error (Scan.error (Scan.finite stopper scan)) args of |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
95 |
OK (x, []) => f x |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
96 |
| OK (_, args') => err_in_src kind "bad arguments" ((s, args'), pos) |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
97 |
| Error msg => err_in_src kind ("\n" ^ msg) src); |
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
98 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
99 |
|
3f824514ad88
Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff
changeset
|
100 |
end; |