author | wenzelm |
Tue, 29 Apr 1997 16:38:16 +0200 | |
changeset 3063 | 963e3bf01799 |
parent 1512 | ce37c64244c0 |
child 3619 | 0fc67ad6d62a |
permissions | -rw-r--r-- |
411 | 1 |
(* Title: Pure/Thy/thy_syn.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5 |
Interface for user syntax. |
|
6 |
*) |
|
7 |
||
8 |
signature THY_SYN_DATA = |
|
1512 | 9 |
sig |
411 | 10 |
val user_keywords: string list |
11 |
val user_sections: (string * (ThyParse.token list -> (string * string) |
|
12 |
* ThyParse.token list)) list |
|
1512 | 13 |
end; |
411 | 14 |
|
15 |
signature THY_SYN = |
|
1512 | 16 |
sig |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
411
diff
changeset
|
17 |
val parse: string -> string -> string |
1512 | 18 |
end; |
411 | 19 |
|
1512 | 20 |
functor ThySynFun (Data: THY_SYN_DATA): THY_SYN = |
411 | 21 |
struct |
22 |
||
1512 | 23 |
val syntax = |
24 |
ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords) |
|
25 |
(ThyParse.pure_sections @ Data.user_sections); |
|
411 | 26 |
|
1512 | 27 |
val parse = ThyParse.parse_thy syntax; |
411 | 28 |
|
29 |
end; |
|
30 |