# 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};