author | clasohm |
Fri, 15 Jul 1994 13:30:42 +0200 | |
changeset 476 | 836cad329311 |
parent 411 | 4860901706db |
child 1512 | ce37c64244c0 |
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 = |
|
9 |
sig |
|
10 |
val user_keywords: string list |
|
11 |
val user_sections: (string * (ThyParse.token list -> (string * string) |
|
12 |
* ThyParse.token list)) list |
|
13 |
end; |
|
14 |
||
15 |
signature THY_SYN = |
|
16 |
sig |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
411
diff
changeset
|
17 |
val parse: string -> string -> string |
411 | 18 |
end; |
19 |
||
20 |
functor ThySynFun(ThySynData: THY_SYN_DATA): THY_SYN = |
|
21 |
struct |
|
22 |
||
23 |
open ThyParse ThySynData; |
|
24 |
||
25 |
val syntax = |
|
26 |
make_syntax (pure_keywords @ user_keywords) (pure_sections @ user_sections); |
|
27 |
||
28 |
val parse = parse_thy syntax; |
|
29 |
||
30 |
end; |
|
31 |