author | nipkow |
Tue, 05 Nov 2019 14:57:41 +0100 | |
changeset 71033 | c1b63124245c |
parent 69851 | 29a4f633609e |
child 72747 | 5f9d66155081 |
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 |
|
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
9 |
val command: string -> bool option -> (theory -> Token.file list) -> |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
67381
diff
changeset
|
10 |
Toplevel.transition -> Toplevel.transition |
62862 | 11 |
val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition |
12 |
val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition |
|
13 |
end; |
|
14 |
||
15 |
structure ML_File: ML_FILE = |
|
16 |
struct |
|
17 |
||
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
18 |
fun command environment debug files = Toplevel.generic_theory (fn gthy => |
62862 | 19 |
let |
69851 | 20 |
val [file: Token.file] = files (Context.theory_of gthy); |
21 |
val provide = Resources.provide_file file; |
|
22 |
val source = Token.file_source file; |
|
67377
143665524d8e
check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
wenzelm
parents:
62902
diff
changeset
|
23 |
|
67381 | 24 |
val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source); |
67377
143665524d8e
check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
wenzelm
parents:
62902
diff
changeset
|
25 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
67381
diff
changeset
|
26 |
val flags: ML_Compiler.flags = |
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
27 |
{environment = environment, redirect = true, verbose = true, |
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62873
diff
changeset
|
28 |
debug = debug, writeln = writeln, warning = warning}; |
62862 | 29 |
in |
30 |
gthy |
|
31 |
|> ML_Context.exec (fn () => ML_Context.eval_source flags source) |
|
32 |
|> Local_Theory.propagate_ml_env |
|
33 |
|> Context.mapping provide (Local_Theory.background_theory provide) |
|
34 |
end); |
|
35 |
||
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
36 |
val ML = command ""; |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
37 |
val SML = command ML_Env.SML; |
62862 | 38 |
|
39 |
end; |