# HG changeset patch
# User wenzelm
# Date 1456849613 -3600
# Node ID 36f11bc393a26b0dbcf417f5ce75d9177367b2db
# Parent  bd7358b3ab5ef92b71a22ed528442e98365e8a3c
use bootstrap compiler earlier;

diff -r bd7358b3ab5e -r 36f11bc393a2 src/Pure/RAW/compiler_polyml.ML
--- 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;
diff -r bd7358b3ab5e -r 36f11bc393a2 src/Pure/RAW/use_context.ML
--- 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};