author | wenzelm |
Sat, 02 Apr 2016 20:23:51 +0200 | |
changeset 62817 | 744bfd770123 |
child 62902 | 3c0f53eae166 |
permissions | -rw-r--r-- |
62817 | 1 |
(* Title: Pure/ML/ml_compiler2.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Isabelle/ML use operations. |
|
5 |
*) |
|
6 |
||
7 |
val {use, use_debug, use_no_debug} = |
|
8 |
ML_Compiler0.use_operations (fn opt_debug => fn file => |
|
9 |
let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in |
|
10 |
ML_Context.eval_file flags (Path.explode file) |
|
11 |
handle ERROR msg => (writeln msg; error "ML error") |
|
12 |
end); |