author | nipkow |
Thu, 26 Nov 1998 12:18:08 +0100 | |
changeset 5974 | 6acf3ff0f486 |
parent 3620 | ed1416badb41 |
child 6206 | 7d2204fcc1e5 |
permissions | -rw-r--r-- |
411 | 1 |
(* Title: Pure/Thy/thy_syn.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
3619 | 5 |
Syntax for thy files. |
411 | 6 |
*) |
7 |
||
8 |
signature THY_SYN = |
|
3619 | 9 |
sig |
10 |
val add_syntax: string list -> |
|
11 |
(string * (ThyParse.token list -> (string * string) * ThyParse.token list)) list |
|
12 |
-> unit |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
411
diff
changeset
|
13 |
val parse: string -> string -> string |
3619 | 14 |
end; |
411 | 15 |
|
3619 | 16 |
structure ThySyn: THY_SYN = |
411 | 17 |
struct |
18 |
||
3619 | 19 |
(* current syntax *) |
20 |
||
21 |
val keywords = ref ThyParse.pure_keywords; |
|
22 |
val sections = ref ThyParse.pure_sections; |
|
23 |
||
24 |
fun make_syntax () = |
|
25 |
ThyParse.make_syntax (! keywords) (!sections); |
|
26 |
||
27 |
val syntax = ref (make_syntax ()); |
|
28 |
||
411 | 29 |
|
3619 | 30 |
(* augment syntax *) |
31 |
||
32 |
fun add_syntax keys sects = |
|
3620 | 33 |
(keywords := (keys union ! keywords); |
3619 | 34 |
sections := sects @ ! sections; |
35 |
syntax := make_syntax ()); |
|
36 |
||
37 |
||
38 |
(* parse *) |
|
39 |
||
40 |
fun parse name txt = |
|
41 |
ThyParse.parse_thy (! syntax) name txt; |
|
411 | 42 |
|
43 |
end; |