author | wenzelm |
Wed, 02 Mar 2022 21:14:09 +0100 | |
changeset 75189 | f304a2a5080f |
parent 62902 | 3c0f53eae166 |
permissions | -rw-r--r-- |
62817 | 1 |
(* Title: Pure/ML/ml_compiler1.ML |
2 |
Author: Makarius |
|
3 |
||
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62817
diff
changeset
|
4 |
Refined ML file operations for bootstrap. |
62817 | 5 |
*) |
6 |
||
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62817
diff
changeset
|
7 |
val {ML_file, ML_file_debug, ML_file_no_debug} = |
62817 | 8 |
let |
9 |
val context: ML_Compiler0.context = |
|
10 |
{name_space = ML_Name_Space.global, |
|
11 |
print_depth = NONE, |
|
12 |
here = Position.here oo Position.line_file, |
|
13 |
print = writeln, |
|
14 |
error = error}; |
|
15 |
in |
|
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62817
diff
changeset
|
16 |
ML_Compiler0.ML_file_operations (fn opt_debug => fn file => |
62817 | 17 |
Position.setmp_thread_data (Position.file_only file) |
18 |
(fn () => |
|
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62817
diff
changeset
|
19 |
ML_Compiler0.ML_file context |
62817 | 20 |
{verbose = true, debug = ML_Compiler0.debug_option opt_debug} file |
21 |
handle ERROR msg => (writeln msg; error "ML error")) ()) |
|
22 |
end; |