author | wenzelm |
Sun, 10 Apr 2016 21:46:12 +0200 | |
changeset 62944 | 3ee643c5ed00 |
parent 62902 | 3c0f53eae166 |
child 67377 | 143665524d8e |
permissions | -rw-r--r-- |
62862 | 1 |
(* Title: Pure/ML/ml_file.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Commands to load ML files. |
|
5 |
*) |
|
6 |
||
7 |
signature ML_FILE = |
|
8 |
sig |
|
9 |
val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition |
|
10 |
val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition |
|
11 |
end; |
|
12 |
||
13 |
structure ML_File: ML_FILE = |
|
14 |
struct |
|
15 |
||
16 |
fun command SML debug files = Toplevel.generic_theory (fn gthy => |
|
17 |
let |
|
18 |
val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy); |
|
19 |
val provide = Resources.provide (src_path, digest); |
|
20 |
val source = Input.source true (cat_lines lines) (pos, pos); |
|
21 |
val flags = |
|
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62873
diff
changeset
|
22 |
{SML = SML, exchange = false, redirect = true, verbose = true, |
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62873
diff
changeset
|
23 |
debug = debug, writeln = writeln, warning = warning}; |
62862 | 24 |
in |
25 |
gthy |
|
26 |
|> ML_Context.exec (fn () => ML_Context.eval_source flags source) |
|
27 |
|> Local_Theory.propagate_ml_env |
|
28 |
|> Context.mapping provide (Local_Theory.background_theory provide) |
|
29 |
end); |
|
30 |
||
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62873
diff
changeset
|
31 |
val ML = command false; |
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62873
diff
changeset
|
32 |
val SML = command true; |
62862 | 33 |
|
34 |
end; |