--- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML Tue Mar 01 21:10:29 2016 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML Tue Mar 01 22:11:36 2016 +0100
@@ -184,7 +184,7 @@
in
compiled_rewriter := NONE;
- use_text ML_Env.local_context
+ ML_Compiler0.use_text ML_Env.local_context
{line = 1, file = "", verbose = false, debug = false} (!buffer);
case !compiled_rewriter of
NONE => raise (Compile "cannot communicate with compiled function")
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML Tue Mar 01 21:10:29 2016 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML Tue Mar 01 22:11:36 2016 +0100
@@ -486,7 +486,8 @@
fun writeTextFile name s = File.write (Path.explode name) s
fun use_source src =
- use_text ML_Env.local_context {line = 1, file = "", verbose = false, debug = false} src
+ ML_Compiler0.use_text ML_Env.local_context
+ {line = 1, file = "", verbose = false, debug = false} src
fun compile rules =
let
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Mar 01 21:10:29 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Mar 01 22:11:36 2016 +0100
@@ -206,7 +206,7 @@
fun exec verbose code =
ML_Context.exec (fn () =>
- use_text ML_Env.local_context
+ ML_Compiler0.use_text ML_Env.local_context
{line = 0, file = "generated code", verbose = verbose, debug = false} code)
fun with_overlord_dir name f =
--- a/src/Pure/ML/ml_env.ML Tue Mar 01 21:10:29 2016 +0100
+++ b/src/Pure/ML/ml_env.ML Tue Mar 01 22:11:36 2016 +0100
@@ -14,7 +14,7 @@
val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
- val local_context: use_context
+ val local_context: ML_Compiler0.context
val local_name_space: ML_Name_Space.T
val check_functor: string -> unit
end
@@ -162,7 +162,7 @@
allFunct = all #6 #allFunct}
end;
-val local_context: use_context =
+val local_context: ML_Compiler0.context =
{name_space = name_space {SML = false, exchange = false},
here = Position.here oo Position.line_file,
print = writeln,
--- a/src/Pure/RAW/ROOT_polyml.ML Tue Mar 01 21:10:29 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Tue Mar 01 22:11:36 2016 +0100
@@ -167,7 +167,7 @@
then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
use "RAW/ml_positions.ML";
-use "RAW/compiler_polyml.ML";
+use "RAW/ml_compiler0.ML";
PolyML.Compiler.reportUnreferencedIds := true;
PolyML.Compiler.printInAlphabeticalOrder := false;
--- a/src/Pure/RAW/compiler_polyml.ML Tue Mar 01 21:10:29 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-(* Title: Pure/RAW/compiler_polyml.ML
-
-Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
-*)
-
-type use_context =
- {name_space: ML_Name_Space.T,
- here: int -> string -> string,
- print: string -> unit,
- error: string -> unit};
-
-local
-
-val boot_context: use_context =
- {name_space = ML_Name_Space.global,
- here = 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 => error s};
-
-fun drop_newline s =
- if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
- else s;
-
-in
-
-fun use_text ({name_space, here, print, error, ...}: use_context)
- {line, file, verbose, debug} text =
- let
- val _ = Secure.deny_ml ();
-
- val current_line = Unsynchronized.ref line;
- val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
- val out_buffer = Unsynchronized.ref ([]: string list);
- fun output () = drop_newline (implode (rev (! out_buffer)));
-
- fun get () =
- (case ! in_buffer of
- [] => NONE
- | c :: cs =>
- (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
- fun put s = out_buffer := s :: ! out_buffer;
- fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
- (put (if hard then "Error: " else "Warning: ");
- PolyML.prettyPrint (put, 76) msg1;
- (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
- put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
-
- val parameters =
- [PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPNameSpace name_space,
- PolyML.Compiler.CPErrorMessageProc put_message,
- PolyML.Compiler.CPLineNo (fn () => ! current_line),
- PolyML.Compiler.CPFileName file,
- PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
- ML_Compiler_Parameters.debug debug;
- val _ =
- (while not (List.null (! in_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- if Exn.is_interrupt exn then reraise exn
- else
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); reraise exn);
- in if verbose then print (output ()) else () end;
-
-fun use_file context {verbose, debug} file =
- let
- val instream = TextIO.openIn file;
- 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_debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
- | use_debug_option (SOME debug) = debug;
-
-fun use_operations (use_ : bool option -> string -> unit) =
- {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
-
-val {use, use_debug, use_no_debug} =
- use_operations (fn opt_debug => fn file =>
- use_file boot_context {verbose = true, debug = use_debug_option opt_debug} file
- handle ERROR msg => (#print boot_context msg; raise error "ML error"));
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_compiler0.ML Tue Mar 01 22:11:36 2016 +0100
@@ -0,0 +1,100 @@
+(* Title: Pure/RAW/ml_compiler0.ML
+
+Runtime compilation and evaluation (bootstrap version of
+Pure/ML/ml_compiler.ML).
+*)
+
+signature ML_COMPILER0 =
+sig
+ type context =
+ {name_space: ML_Name_Space.T,
+ here: int -> string -> string,
+ print: string -> unit,
+ error: string -> unit}
+ val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
+ val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
+ val debug_option: bool option -> bool
+ val use_operations: (bool option -> string -> unit) ->
+ {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
+end;
+
+structure ML_Compiler0: ML_COMPILER0 =
+struct
+
+type context =
+ {name_space: ML_Name_Space.T,
+ here: int -> string -> string,
+ print: string -> unit,
+ error: string -> unit};
+
+fun drop_newline s =
+ if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
+ else s;
+
+fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
+ let
+ val _ = Secure.deny_ml ();
+
+ val current_line = Unsynchronized.ref line;
+ val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
+ val out_buffer = Unsynchronized.ref ([]: string list);
+ fun output () = drop_newline (implode (rev (! out_buffer)));
+
+ fun get () =
+ (case ! in_buffer of
+ [] => NONE
+ | c :: cs =>
+ (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
+ fun put s = out_buffer := s :: ! out_buffer;
+ fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
+ (put (if hard then "Error: " else "Warning: ");
+ PolyML.prettyPrint (put, 76) msg1;
+ (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
+ put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream put,
+ PolyML.Compiler.CPNameSpace name_space,
+ PolyML.Compiler.CPErrorMessageProc put_message,
+ PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPFileName file,
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
+ ML_Compiler_Parameters.debug debug;
+ val _ =
+ (while not (List.null (! in_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ error (output ()); reraise exn);
+ in if verbose then print (output ()) else () end;
+
+fun use_file context {verbose, debug} file =
+ let
+ val instream = TextIO.openIn file;
+ 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 debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
+ | debug_option (SOME debug) = debug;
+
+fun use_operations (use_ : bool option -> string -> unit) =
+ {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
+
+end;
+
+val {use, use_debug, use_no_debug} =
+ let
+ val context: ML_Compiler0.context =
+ {name_space = ML_Name_Space.global,
+ here = 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 => error s};
+ in
+ ML_Compiler0.use_operations (fn opt_debug => fn file =>
+ ML_Compiler0.use_file context
+ {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
+ handle ERROR msg => (#print context msg; raise error "ML error"))
+ end;
--- a/src/Pure/ROOT Tue Mar 01 21:10:29 2016 +0100
+++ b/src/Pure/ROOT Tue Mar 01 22:11:36 2016 +0100
@@ -5,11 +5,11 @@
files
"RAW/ROOT_polyml-5.6.ML"
"RAW/ROOT_polyml.ML"
- "RAW/compiler_polyml.ML"
"RAW/exn.ML"
"RAW/exn_trace.ML"
"RAW/exn_trace_raw.ML"
"RAW/fixed_int_dummy.ML"
+ "RAW/ml_compiler0.ML"
"RAW/ml_compiler_parameters.ML"
"RAW/ml_compiler_parameters_polyml-5.6.ML"
"RAW/ml_debugger.ML"
@@ -37,11 +37,11 @@
files
"RAW/ROOT_polyml-5.6.ML"
"RAW/ROOT_polyml.ML"
- "RAW/compiler_polyml.ML"
"RAW/exn.ML"
"RAW/exn_trace.ML"
"RAW/exn_trace_raw.ML"
"RAW/fixed_int_dummy.ML"
+ "RAW/ml_compiler0.ML"
"RAW/ml_compiler_parameters.ML"
"RAW/ml_compiler_parameters_polyml-5.6.ML"
"RAW/ml_debugger.ML"
--- a/src/Pure/ROOT.ML Tue Mar 01 21:10:29 2016 +0100
+++ b/src/Pure/ROOT.ML Tue Mar 01 22:11:36 2016 +0100
@@ -36,17 +36,18 @@
val {use, use_debug, use_no_debug} =
let
- val global_context: use_context =
+ val context: ML_Compiler0.context =
{name_space = ML_Name_Space.global,
here = Position.here oo Position.line_file,
print = writeln,
- error = error}
+ error = error};
in
- use_operations (fn opt_debug => fn file =>
+ ML_Compiler0.use_operations (fn opt_debug => fn file =>
Position.setmp_thread_data (Position.file_only file)
(fn () =>
- use_file global_context {verbose = true, debug = use_debug_option opt_debug} file
- handle ERROR msg => (writeln msg; error "ML error")) ())
+ ML_Compiler0.use_file context
+ {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
+ handle ERROR msg => (writeln msg; error "ML error")) ())
end;
@@ -228,7 +229,7 @@
use "ML/ml_antiquotation.ML";
val {use, use_debug, use_no_debug} =
- use_operations (fn opt_debug => fn file =>
+ ML_Compiler0.use_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")
--- a/src/Tools/Code/code_runtime.ML Tue Mar 01 21:10:29 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML Tue Mar 01 22:11:36 2016 +0100
@@ -82,7 +82,7 @@
fun exec ctxt verbose code =
(if Config.get ctxt trace then tracing code else ();
ML_Context.exec (fn () =>
- use_text ML_Env.local_context
+ ML_Compiler0.use_text ML_Env.local_context
{line = 0, file = "generated code", verbose = verbose, debug = false} code));
fun value ctxt (get, put, put_ml) (prelude, value) =
@@ -509,7 +509,7 @@
fun abort _ = error "Only value bindings allowed.";
-val notifying_context : use_context =
+val notifying_context : ML_Compiler0.context =
{name_space =
{lookupVal = #lookupVal ML_Env.local_name_space,
lookupType = #lookupType ML_Env.local_name_space,
@@ -540,7 +540,7 @@
val thy' = Loaded_Values.put [] thy;
val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
val _ =
- use_text notifying_context
+ ML_Compiler0.use_text notifying_context
{line = 0, file = Path.implode filepath, verbose = false, debug = false}
(File.read filepath);
val thy'' = Context.the_theory (Context.the_thread_data ());
--- a/src/Tools/Spec_Check/spec_check.ML Tue Mar 01 21:10:29 2016 +0100
+++ b/src/Tools/Spec_Check/spec_check.ML Tue Mar 01 22:11:36 2016 +0100
@@ -127,7 +127,7 @@
fun determine_type ctxt s =
let
val return = Unsynchronized.ref "return"
- val use_context : use_context =
+ val context : ML_Compiler0.context =
{name_space = #name_space ML_Env.local_context,
here = #here ML_Env.local_context,
print = fn r => return := r,
@@ -135,7 +135,7 @@
val _ =
Context.setmp_thread_data (SOME (Context.Proof ctxt))
(fn () =>
- use_text use_context
+ ML_Compiler0.use_text context
{line = 0, file = "generated code", verbose = true, debug = false} s) ()
in
Gen_Construction.parse_pred (! return)
@@ -145,7 +145,7 @@
fun run_test ctxt s =
Context.setmp_thread_data (SOME (Context.Proof ctxt))
(fn () =>
- use_text ML_Env.local_context
+ ML_Compiler0.use_text ML_Env.local_context
{line = 0, file = "generated code", verbose = false, debug = false} s) ();
(*split input into tokens*)