proper position information for Context.theory_data_size;
authorwenzelm
Sun, 15 Aug 2021 15:26:09 +0200
changeset 74418 a97d5356f1d9
parent 74417 d030b988d470
child 74419 46f66e821f5c
child 74420 9e73600ec75d
proper position information for Context.theory_data_size;
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;