6 |
6 |
7 signature THY_HEADER = |
7 signature THY_HEADER = |
8 sig |
8 sig |
9 type header = |
9 type header = |
10 {name: string, imports: string list, |
10 {name: string, imports: string list, |
11 keywords: (string * (string * string list) option) list, |
11 keywords: (string * Keyword.spec option) list, |
12 uses: (Path.T * bool) list} |
12 uses: (Path.T * bool) list} |
13 val make: string -> string list -> (string * (string * string list) option) list -> |
13 val make: string -> string list -> (string * Keyword.spec option) list -> |
14 (Path.T * bool) list -> header |
14 (Path.T * bool) list -> header |
15 val define_keywords: header -> unit |
15 val define_keywords: header -> unit |
16 val declare_keyword: string * (string * string list) option -> theory -> theory |
16 val declare_keyword: string * Keyword.spec option -> theory -> theory |
17 val the_keyword: theory -> string -> Keyword.T option |
17 val the_keyword: theory -> string -> Keyword.spec option |
18 val args: header parser |
18 val args: header parser |
19 val read: Position.T -> string -> header |
19 val read: Position.T -> string -> header |
20 end; |
20 end; |
21 |
21 |
22 structure Thy_Header: THY_HEADER = |
22 structure Thy_Header: THY_HEADER = |
23 struct |
23 struct |
24 |
24 |
25 type header = |
25 type header = |
26 {name: string, imports: string list, |
26 {name: string, imports: string list, |
27 keywords: (string * (string * string list) option) list, |
27 keywords: (string * Keyword.spec option) list, |
28 uses: (Path.T * bool) list}; |
28 uses: (Path.T * bool) list}; |
29 |
29 |
30 fun make name imports keywords uses : header = |
30 fun make name imports keywords uses : header = |
31 {name = name, imports = imports, keywords = keywords, uses = uses}; |
31 {name = name, imports = imports, keywords = keywords, uses = uses}; |
32 |
32 |
33 |
33 |
34 |
34 |
35 (** keyword declarations **) |
35 (** keyword declarations **) |
36 |
36 |
37 fun define_keywords ({keywords, ...}: header) = |
37 fun define_keywords ({keywords, ...}: header) = |
38 List.app (fn (name, decl) => Keyword.define (name, Option.map Keyword.make decl)) keywords; |
38 List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords; |
39 |
39 |
40 fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name); |
40 fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name); |
41 |
41 |
42 structure Data = Theory_Data |
42 structure Data = Theory_Data |
43 ( |
43 ( |
44 type T = Keyword.T option Symtab.table; |
44 type T = Keyword.spec option Symtab.table; |
45 val empty = Symtab.empty; |
45 val empty = Symtab.empty; |
46 val extend = I; |
46 val extend = I; |
47 fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name; |
47 fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name; |
48 ); |
48 ); |
49 |
49 |
50 fun declare_keyword (name, decl) = Data.map (fn data => |
50 fun declare_keyword (name, spec) = |
51 let val kind = Option.map Keyword.make decl |
51 Data.map (fn data => |
52 in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end); |
52 (Option.map Keyword.spec spec; |
|
53 Symtab.update_new (name, spec) data handle Symtab.DUP dup => err_dup dup)); |
53 |
54 |
54 fun the_keyword thy name = |
55 fun the_keyword thy name = |
55 (case Symtab.lookup (Data.get thy) name of |
56 (case Symtab.lookup (Data.get thy) name of |
56 SOME kind => kind |
57 SOME spec => spec |
57 | NONE => error ("Unknown outer syntax keyword " ^ quote name)); |
58 | NONE => error ("Undeclared outer syntax keyword " ^ quote name)); |
58 |
59 |
59 |
60 |
60 |
61 |
61 (** concrete syntax **) |
62 (** concrete syntax **) |
62 |
63 |