# HG changeset patch # User wenzelm # Date 1629033969 -7200 # Node ID a97d5356f1d9bbf78c70126346a7a015d518c74b # Parent d030b988d470061e400b8e4ed78ea337281e7001 proper position information for Context.theory_data_size; diff -r d030b988d470 -r a97d5356f1d9 src/Pure/ML/ml_compiler2.ML --- a/src/Pure/ML/ml_compiler2.ML Thu Aug 12 14:18:46 2021 +0200 +++ b/src/Pure/ML/ml_compiler2.ML Sun Aug 15 15:26:09 2021 +0200 @@ -7,8 +7,9 @@ val {ML_file, ML_file_debug, ML_file_no_debug} = ML_Compiler0.ML_file_operations (fn opt_debug => fn file => let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in - ML_Context.eval_file flags (Path.explode file) - handle ERROR msg => (writeln msg; error "ML error") + Position.setmp_thread_data (Position.file_only file) (fn () => + ML_Context.eval_file flags (Path.explode file) + handle ERROR msg => (writeln msg; error "ML error")) () end); val use = ML_file;