equal
deleted
inserted
replaced
|
1 (* Title: Pure/ML/ml_compiler.ML |
|
2 Author: Makarius |
|
3 |
|
4 Runtime compilation -- generic version. |
|
5 *) |
|
6 |
|
7 signature ML_COMPILER = |
|
8 sig |
|
9 val eval: bool -> Position.T -> ML_Lex.token list -> unit |
|
10 end |
|
11 |
|
12 structure ML_Compiler: ML_COMPILER = |
|
13 struct |
|
14 |
|
15 fun eval verbose pos toks = |
|
16 let |
|
17 val line = the_default 1 (Position.line_of pos); |
|
18 val file = the_default "ML" (Position.file_of pos); |
|
19 val text = ML_Lex.flatten toks; |
|
20 in Secure.use_text ML_Env.local_context (line, file) verbose text end; |
|
21 |
|
22 end; |
|
23 |