use bootstrap compiler earlier;
authorwenzelm
Tue, 01 Mar 2016 17:26:53 +0100
changeset 62489 36f11bc393a2
parent 62488 bd7358b3ab5e
child 62490 39d01eaf5292
use bootstrap compiler earlier;
src/Pure/RAW/compiler_polyml.ML
src/Pure/RAW/use_context.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;
--- 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};