--- a/src/Pure/RAW/compiler_polyml.ML Tue Mar 01 16:19:56 2016 +0100
+++ b/src/Pure/RAW/compiler_polyml.ML Tue Mar 01 17:26:53 2016 +0100
@@ -55,4 +55,8 @@
val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
+fun use file =
+ use_file boot_context {verbose = true, debug = false} file
+ handle Fail msg => (#print boot_context msg; raise Fail "ML error");
+
end;
--- a/src/Pure/RAW/use_context.ML Tue Mar 01 16:19:56 2016 +0100
+++ b/src/Pure/RAW/use_context.ML Tue Mar 01 17:26:53 2016 +0100
@@ -10,3 +10,8 @@
print: string -> unit,
error: string -> unit};
+val boot_context: use_context =
+ {name_space = ML_Name_Space.global,
+ str_of_pos = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
+ print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
+ error = fn s => raise Fail s};