| author | wenzelm |
| Thu, 15 Aug 2024 12:43:17 +0200 | |
| changeset 80712 | 05b16602a683 |
| parent 74148 | a97d5356f1d9 |
| permissions | -rw-r--r-- |
| 62817 | 1 |
(* Title: Pure/ML/ml_compiler2.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 |
Isabelle/ML file operations. |
| 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} =
|
|
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62817
diff
changeset
|
8 |
ML_Compiler0.ML_file_operations (fn opt_debug => fn file => |
| 62817 | 9 |
let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in |
|
74148
a97d5356f1d9
proper position information for Context.theory_data_size;
wenzelm
parents:
62944
diff
changeset
|
10 |
Position.setmp_thread_data (Position.file_only file) (fn () => |
|
a97d5356f1d9
proper position information for Context.theory_data_size;
wenzelm
parents:
62944
diff
changeset
|
11 |
ML_Context.eval_file flags (Path.explode file) |
|
a97d5356f1d9
proper position information for Context.theory_data_size;
wenzelm
parents:
62944
diff
changeset
|
12 |
handle ERROR msg => (writeln msg; error "ML error")) () |
| 62817 | 13 |
end); |
|
62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62902
diff
changeset
|
14 |
|
|
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62902
diff
changeset
|
15 |
val use = ML_file; |