--- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML Mon Aug 17 16:27:12 2015 +0200
@@ -184,7 +184,8 @@
in
compiled_rewriter := NONE;
- use_text ML_Env.local_context (1, "") false (!buffer);
+ 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")
| SOME r => (compiled_rewriter := NONE; r)
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML Mon Aug 17 16:27:12 2015 +0200
@@ -485,7 +485,8 @@
fun writeTextFile name s = File.write (Path.explode name) s
-fun use_source src = use_text ML_Env.local_context (1, "") false src
+fun use_source src =
+ 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 Mon Aug 17 15:29:30 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Aug 17 16:27:12 2015 +0200
@@ -205,7 +205,9 @@
File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
fun exec verbose code =
- ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
+ ML_Context.exec (fn () =>
+ Secure.use_text ML_Env.local_context
+ {line = 0, file = "generated code", verbose = verbose, debug = false} code)
fun with_overlord_dir name f =
let
--- a/src/Pure/General/secure.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/General/secure.ML Mon Aug 17 16:27:12 2015 +0200
@@ -10,8 +10,9 @@
val is_secure: unit -> bool
val deny_secure: string -> unit
val secure_mltext: unit -> unit
- val use_text: use_context -> int * string -> bool -> string -> unit
- val use_file: use_context -> bool -> string -> unit
+ val use_text: use_context ->
+ {line: int, file: string, verbose: bool, debug: bool} -> string -> unit
+ val use_file: use_context -> {verbose: bool, debug: bool} -> string -> unit
val toplevel_pp: string list -> string -> unit
end;
@@ -37,10 +38,9 @@
val raw_use_file = use_file;
val raw_toplevel_pp = toplevel_pp;
-fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt);
-fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name);
+fun use_text context flags (text: string) = (secure_mltext (); raw_use_text context flags text);
+fun use_file context flags (file: string) = (secure_mltext (); raw_use_file context flags file);
fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
end;
-
--- a/src/Pure/Isar/isar_syn.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Aug 17 16:27:12 2015 +0200
@@ -209,9 +209,9 @@
let
val ([{lines, pos, ...}], thy') = files thy;
val source = Input.source true (cat_lines lines) (pos, pos);
- val flags =
+ val flags: ML_Compiler.flags =
{SML = true, exchange = false, redirect = true, verbose = true,
- writeln = writeln, warning = warning};
+ debug = NONE, writeln = writeln, warning = warning};
in
thy' |> Context.theory_map
(ML_Context.exec (fn () => ML_Context.eval_source flags source))
@@ -221,9 +221,9 @@
Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
(Parse.ML_source >> (fn source =>
let
- val flags =
+ val flags: ML_Compiler.flags =
{SML = true, exchange = true, redirect = false, verbose = true,
- writeln = writeln, warning = warning};
+ debug = NONE, writeln = writeln, warning = warning};
in
Toplevel.theory
(Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
@@ -233,9 +233,9 @@
Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment"
(Parse.ML_source >> (fn source =>
let
- val flags =
+ val flags: ML_Compiler.flags =
{SML = false, exchange = true, redirect = false, verbose = true,
- writeln = writeln, warning = warning};
+ debug = NONE, writeln = writeln, warning = warning};
in
Toplevel.generic_theory
(ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
--- a/src/Pure/ML-Systems/compiler_polyml.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml.ML Mon Aug 17 16:27:12 2015 +0200
@@ -12,11 +12,11 @@
in
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
- (line, file) verbose txt =
+ {line, file, verbose, debug} text =
let
val current_line = Unsynchronized.ref line;
val in_buffer =
- Unsynchronized.ref (String.explode (tune_source (ml_positions line file txt)));
+ Unsynchronized.ref (String.explode (tune_source (ml_positions line file text)));
val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
@@ -38,7 +38,8 @@
PolyML.Compiler.CPErrorMessageProc put_message,
PolyML.Compiler.CPLineNo (fn () => ! current_line),
PolyML.Compiler.CPFileName file,
- PolyML.Compiler.CPPrintInAlphabeticalOrder false];
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
+ ML_Compiler_Parameters.debug debug;
val _ =
(while not (List.null (! in_buffer)) do
PolyML.compiler (get, parameters) ())
@@ -49,10 +50,10 @@
error (output ()); reraise exn);
in if verbose then print (output ()) else () end;
-fun use_file context verbose file =
+fun use_file context {verbose, debug} file =
let
val instream = TextIO.openIn file;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, file) verbose txt end;
+ 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;
end;
--- a/src/Pure/ML-Systems/polyml.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Mon Aug 17 16:27:12 2015 +0200
@@ -177,6 +177,10 @@
val display_val = pretty_ml o PolyML.NameSpace.displayVal;
end;
+use "ML-Systems/ml_compiler_parameters.ML";
+if ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
+
use "ML-Systems/use_context.ML";
use "ML-Systems/ml_positions.ML";
use "ML-Systems/compiler_polyml.ML";
@@ -191,12 +195,8 @@
if ML_System.name = "polyml-5.5.3"
then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
-use "ML-Systems/ml_compiler_parameters.ML";
-if ML_System.name = "polyml-5.5.3"
-then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
-
fun toplevel_pp context (_: string list) pp =
- use_text context (1, "pp") false
+ use_text context {line = 1, file = "pp", verbose = false, debug = false}
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
fun ml_make_string struct_name =
--- a/src/Pure/ML-Systems/smlnj.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Mon Aug 17 16:27:12 2015 +0200
@@ -82,7 +82,8 @@
(* ML command execution *)
-fun use_text ({tune_source, print, error, ...}: use_context) (line, file) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context)
+ {line, file, verbose, debug = _: bool} text =
let
val ref out_orig = Control.Print.out;
@@ -93,7 +94,7 @@
in String.substring (str, 0, Int.max (0, size str - 1)) end;
in
Control.Print.out := out;
- Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file txt)))
+ Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file text)))
handle exn =>
(Control.Print.out := out_orig;
error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
@@ -101,11 +102,11 @@
if verbose then print (output ()) else ()
end;
-fun use_file context verbose file =
+fun use_file context {verbose, debug} file =
let
val instream = TextIO.openIn file;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, file) verbose txt end;
+ 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;
(* toplevel pretty printing *)
@@ -123,7 +124,7 @@
in pprint end;
fun toplevel_pp context path pp =
- use_text context (1, "pp") false
+ use_text context {line = 1, file = "pp", verbose = false, debug = false}
("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"") path) ^
"] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
--- a/src/Pure/ML/ml_compiler.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML/ml_compiler.ML Mon Aug 17 16:27:12 2015 +0200
@@ -8,7 +8,7 @@
sig
type flags =
{SML: bool, exchange: bool, redirect: bool, verbose: bool,
- writeln: string -> unit, warning: string -> unit}
+ debug: bool option, writeln: string -> unit, warning: string -> unit}
val flags: flags
val verbose: bool -> flags -> flags
val eval: flags -> Position.T -> ML_Lex.token list -> unit
@@ -19,23 +19,26 @@
type flags =
{SML: bool, exchange: bool, redirect: bool, verbose: bool,
- writeln: string -> unit, warning: string -> unit};
+ debug: bool option, writeln: string -> unit, warning: string -> unit};
val flags: flags =
{SML = false, exchange = false, redirect = false, verbose = false,
- writeln = writeln, warning = warning};
+ debug = NONE, writeln = writeln, warning = warning};
fun verbose b (flags: flags) =
- {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b,
- writeln = #writeln flags, warning = #warning flags};
+ {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
+ verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
fun eval (flags: flags) pos toks =
let
val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
val line = the_default 1 (Position.line_of pos);
val file = the_default "ML" (Position.file_of pos);
+ val debug = the_default false (#debug flags);
val text = ML_Lex.flatten toks;
- in Secure.use_text ML_Env.local_context (line, file) (#verbose flags) text end;
+ in
+ Secure.use_text ML_Env.local_context
+ {line = line, file = file, verbose = #verbose flags, debug = debug} text
+ end;
end;
-
--- a/src/Pure/ML/ml_compiler_polyml.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML Mon Aug 17 16:27:12 2015 +0200
@@ -225,6 +225,11 @@
(* compiler invocation *)
+ val debug =
+ (case #debug flags of
+ SOME debug => debug
+ | NONE => ML_Options.debugger_enabled opt_context);
+
val parameters =
[PolyML.Compiler.CPOutStream write,
PolyML.Compiler.CPNameSpace space,
@@ -235,7 +240,8 @@
PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
PolyML.Compiler.CPCompilerResultFun result_fun,
PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
- ML_Compiler_Parameters.debug (ML_Options.debugger_enabled opt_context);
+ ML_Compiler_Parameters.debug debug;
+
val _ =
(while not (List.null (! input_buffer)) do
PolyML.compiler (get, parameters) ())
@@ -257,4 +263,3 @@
end;
end;
-
--- a/src/Pure/ML/ml_file.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML/ml_file.ML Mon Aug 17 16:27:12 2015 +0200
@@ -14,9 +14,9 @@
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
val provide = Resources.provide (src_path, digest);
val source = Input.source true (cat_lines lines) (pos, pos);
- val flags =
+ val flags: ML_Compiler.flags =
{SML = false, exchange = false, redirect = true, verbose = true,
- writeln = writeln, warning = warning};
+ debug = NONE, writeln = writeln, warning = warning};
in
gthy
|> ML_Context.exec (fn () => ML_Context.eval_source flags source)
--- a/src/Pure/ROOT.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ROOT.ML Mon Aug 17 16:27:12 2015 +0200
@@ -41,10 +41,10 @@
val use_text = Secure.use_text;
val use_file = Secure.use_file;
-fun use s =
- Position.setmp_thread_data (Position.file_only s)
+fun use file =
+ Position.setmp_thread_data (Position.file_only file)
(fn () =>
- Secure.use_file ML_Parse.global_context true s
+ Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
handle ERROR msg => (writeln msg; error "ML error")) ();
val toplevel_pp = Secure.toplevel_pp;
--- a/src/Pure/Tools/debugger.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/Tools/debugger.ML Mon Aug 17 16:27:12 2015 +0200
@@ -144,13 +144,12 @@
fun evaluate {SML, verbose} =
ML_Context.eval
{SML = SML, exchange = false, redirect = false, verbose = verbose,
- writeln = writeln_message, warning = warning_message}
+ debug = SOME false, writeln = writeln_message, warning = warning_message}
Position.none;
fun eval_setup thread_name index SML context =
context
|> Context_Position.set_visible_generic false
- |> Config.put_generic ML_Options.debugger false
|> ML_Env.add_name_space {SML = SML}
(ML_Debugger.debug_name_space (the_debug_state thread_name index));
--- a/src/Tools/Code/code_runtime.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Tools/Code/code_runtime.ML Mon Aug 17 16:27:12 2015 +0200
@@ -80,8 +80,10 @@
val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
fun exec ctxt verbose code =
- (if Config.get ctxt trace then tracing code else ();
- ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));
+ (if Config.get ctxt trace then tracing code else ();
+ ML_Context.exec (fn () =>
+ Secure.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) =
let
@@ -538,8 +540,10 @@
let
val thy' = Loaded_Values.put [] thy;
val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
- val _ = Secure.use_text notifying_context
- (0, Path.implode filepath) false (File.read filepath);
+ val _ =
+ Secure.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 ());
val names = Loaded_Values.get thy'';
in (names, thy'') end;
--- a/src/Tools/Spec_Check/spec_check.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Tools/Spec_Check/spec_check.ML Mon Aug 17 16:27:12 2015 +0200
@@ -135,7 +135,9 @@
error = #error ML_Env.local_context}
val _ =
Context.setmp_thread_data (SOME (Context.Proof ctxt))
- (fn () => Secure.use_text use_context (0, "generated code") true s) ()
+ (fn () =>
+ Secure.use_text use_context
+ {line = 0, file = "generated code", verbose = true, debug = false} s) ()
in
Gen_Construction.parse_pred (! return)
end;
@@ -143,7 +145,9 @@
(*call the compiler and run the test*)
fun run_test ctxt s =
Context.setmp_thread_data (SOME (Context.Proof ctxt))
- (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false s) ();
+ (fn () =>
+ Secure.use_text ML_Env.local_context
+ {line = 0, file = "generated code", verbose = false, debug = false} s) ();
(*split input into tokens*)
fun input_split s =