--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Mar 01 21:00:38 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Mar 01 21:10:29 2016 +0100
@@ -206,7 +206,7 @@
fun exec verbose code =
ML_Context.exec (fn () =>
- Secure.use_text ML_Env.local_context
+ 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/General/secure.ML Tue Mar 01 21:00:38 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(* Title: Pure/General/secure.ML
- Author: Makarius
-
-Secure critical operations.
-*)
-
-signature SECURE =
-sig
- val set_secure: unit -> unit
- val is_secure: unit -> bool
- val deny_secure: string -> unit
- val secure_mltext: unit -> 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
-end;
-
-structure Secure: SECURE =
-struct
-
-(** secure flag **)
-
-val secure = Unsynchronized.ref false;
-
-fun set_secure () = secure := true;
-fun is_secure () = ! secure;
-
-fun deny_secure msg = if is_secure () then error msg else ();
-
-
-
-(** critical operations **)
-
-fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
-
-val raw_use_text = use_text;
-val raw_use_file = use_file;
-
-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);
-
-end;
--- a/src/Pure/ML/ml_compiler.ML Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Tue Mar 01 21:10:29 2016 +0100
@@ -148,7 +148,7 @@
fun eval (flags: flags) pos toks =
let
- val _ = Secure.secure_mltext ();
+ val _ = Secure.deny_ml ();
val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags};
val opt_context = Context.thread_data ();
--- a/src/Pure/ML/ml_env.ML Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/ML/ml_env.ML Tue Mar 01 21:10:29 2016 +0100
@@ -164,7 +164,7 @@
val local_context: use_context =
{name_space = name_space {SML = false, exchange = false},
- str_of_pos = Position.here oo Position.line_file,
+ here = Position.here oo Position.line_file,
print = writeln,
error = error};
--- a/src/Pure/ML/ml_parse.ML Tue Mar 01 21:00:38 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(* Title: Pure/ML/ml_parse.ML
- Author: Makarius
-
-Minimal parsing for SML -- fixing integer numerals.
-*)
-
-signature ML_PARSE =
-sig
- val global_context: use_context
-end;
-
-structure ML_Parse: ML_PARSE =
-struct
-
-(** error handling **)
-
-fun !!! scan =
- let
- fun get_pos [] = " (end-of-input)"
- | get_pos (tok :: _) = Position.here (ML_Lex.pos_of tok);
-
- fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks)
- | err (toks, SOME msg) = (fn () => "SML syntax error" ^ get_pos toks ^ ": " ^ msg ());
- in Scan.!! err scan end;
-
-fun bad_input x =
- (Scan.some (fn tok => (case ML_Lex.kind_of tok of ML_Lex.Error msg => SOME msg | _ => NONE)) :|--
- (fn msg => Scan.fail_with (K (fn () => msg)))) x;
-
-
-(** basic parsers **)
-
-fun $$$ x =
- Scan.one (fn tok => ML_Lex.kind_of tok = ML_Lex.Keyword andalso ML_Lex.content_of tok = x)
- >> ML_Lex.content_of;
-
-val int = Scan.one (fn tok => ML_Lex.kind_of tok = ML_Lex.Int) >> ML_Lex.content_of;
-
-val regular = Scan.one ML_Lex.is_regular >> ML_Lex.content_of;
-val improper = Scan.one ML_Lex.is_improper >> ML_Lex.content_of;
-
-val blanks = Scan.repeat improper >> implode;
-
-
-(* global use_context *)
-
-val global_context: use_context =
- {name_space = ML_Name_Space.global,
- str_of_pos = Position.here oo Position.line_file,
- print = writeln,
- error = error};
-
-end;
--- a/src/Pure/RAW/ROOT_polyml.ML Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Tue Mar 01 21:10:29 2016 +0100
@@ -154,6 +154,8 @@
(* ML compiler *)
+use "RAW/secure.ML";
+
structure ML_Name_Space =
struct
open ML_Name_Space;
--- a/src/Pure/RAW/compiler_polyml.ML Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/RAW/compiler_polyml.ML Tue Mar 01 21:10:29 2016 +0100
@@ -5,7 +5,7 @@
type use_context =
{name_space: ML_Name_Space.T,
- str_of_pos: int -> string -> string,
+ here: int -> string -> string,
print: string -> unit,
error: string -> unit};
@@ -13,9 +13,9 @@
val boot_context: use_context =
{name_space = ML_Name_Space.global,
- str_of_pos = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
+ 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 => raise Fail s};
+ error = fn s => error s};
fun drop_newline s =
if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
@@ -23,9 +23,11 @@
in
-fun use_text ({name_space, str_of_pos, print, error, ...}: use_context)
+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);
@@ -41,7 +43,7 @@
(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" ^ str_of_pos (FixedInt.toInt message_line) file ^ "\n"));
+ put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
val parameters =
[PolyML.Compiler.CPOutStream put,
@@ -71,18 +73,12 @@
fun use_debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
| use_debug_option (SOME debug) = debug;
-local
-
-fun use_ opt_debug file =
- use_file boot_context {verbose = true, debug = use_debug_option opt_debug} file
- handle Fail msg => (#print boot_context msg; raise Fail "ML error");
+fun use_operations (use_ : bool option -> string -> unit) =
+ {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
-in
-
-val use = use_ NONE;
-val use_debug = use_ (SOME true);
-val 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;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/secure.ML Tue Mar 01 21:10:29 2016 +0100
@@ -0,0 +1,27 @@
+(* Title: Pure/RAW/secure.ML
+ Author: Makarius
+
+Secure critical operations.
+*)
+
+signature SECURE =
+sig
+ val set_secure: unit -> unit
+ val is_secure: unit -> bool
+ val deny: string -> unit
+ val deny_ml: unit -> unit
+end;
+
+structure Secure: SECURE =
+struct
+
+val secure = Unsynchronized.ref false;
+
+fun set_secure () = secure := true;
+fun is_secure () = ! secure;
+
+fun deny msg = if is_secure () then error msg else ();
+
+fun deny_ml () = deny "Cannot evaluate ML source in secure mode";
+
+end;
--- a/src/Pure/ROOT Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/ROOT Tue Mar 01 21:10:29 2016 +0100
@@ -28,6 +28,7 @@
"RAW/ml_stack_polyml-5.6.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
+ "RAW/secure.ML"
"RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
@@ -59,6 +60,7 @@
"RAW/ml_stack_polyml-5.6.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
+ "RAW/secure.ML"
"RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
@@ -105,7 +107,6 @@
"General/queue.ML"
"General/same.ML"
"General/scan.ML"
- "General/secure.ML"
"General/seq.ML"
"General/sha1.ML"
"General/sha1_polyml.ML"
@@ -166,7 +167,6 @@
"ML/ml_file.ML"
"ML/ml_lex.ML"
"ML/ml_options.ML"
- "ML/ml_parse.ML"
"ML/ml_statistics.ML"
"ML/ml_statistics_dummy.ML"
"ML/ml_syntax.ML"
--- a/src/Pure/ROOT.ML Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/ROOT.ML Tue Mar 01 21:10:29 2016 +0100
@@ -1,6 +1,6 @@
(*** Isabelle/Pure bootstrap from "RAW" environment ***)
-(** bootstrap phase 0: towards secure ML barrier *)
+(** bootstrap phase 0: towards ML within position context *)
structure Distribution = (*filled-in by makedist*)
struct
@@ -33,24 +33,21 @@
use "General/input.ML";
use "General/antiquote.ML";
use "ML/ml_lex.ML";
-use "ML/ml_parse.ML";
-use "General/secure.ML";
-val use_text = Secure.use_text;
-val use_file = Secure.use_file;
-
-local
- fun use_ opt_debug file =
- Position.setmp_thread_data (Position.file_only file)
- (fn () =>
- Secure.use_file ML_Parse.global_context
- {verbose = true, debug = use_debug_option opt_debug} file
- handle ERROR msg => (writeln msg; error "ML error")) ();
-in
- val use = use_ NONE;
- val use_debug = use_ (SOME true);
- val use_no_debug = use_ (SOME false);
-end;
+val {use, use_debug, use_no_debug} =
+ let
+ val global_context: use_context =
+ {name_space = ML_Name_Space.global,
+ here = Position.here oo Position.line_file,
+ print = writeln,
+ error = error}
+ in
+ 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")) ())
+ end;
@@ -230,19 +227,12 @@
use "ML/ml_context.ML";
use "ML/ml_antiquotation.ML";
-local
- fun use_ opt_debug file =
- let val flags = ML_Compiler.debug_flags opt_debug |> ML_Compiler.verbose true in
+val {use, use_debug, use_no_debug} =
+ 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")
- end;
-in
-
-val use = use_ NONE;
-val use_debug = use_ (SOME true);
-val use_no_debug = use_ (SOME false);
-
-end;
+ end);
--- a/src/Tools/Code/code_runtime.ML Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML Tue Mar 01 21:10:29 2016 +0100
@@ -82,7 +82,7 @@
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
+ 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) =
@@ -529,7 +529,7 @@
allStruct = #allStruct ML_Env.local_name_space,
allSig = #allSig ML_Env.local_name_space,
allFunct = #allFunct ML_Env.local_name_space},
- str_of_pos = #str_of_pos ML_Env.local_context,
+ here = #here ML_Env.local_context,
print = #print ML_Env.local_context,
error = #error ML_Env.local_context};
@@ -540,7 +540,7 @@
val thy' = Loaded_Values.put [] thy;
val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
val _ =
- Secure.use_text notifying_context
+ 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:00:38 2016 +0100
+++ b/src/Tools/Spec_Check/spec_check.ML Tue Mar 01 21:10:29 2016 +0100
@@ -129,13 +129,13 @@
val return = Unsynchronized.ref "return"
val use_context : use_context =
{name_space = #name_space ML_Env.local_context,
- str_of_pos = #str_of_pos ML_Env.local_context,
+ here = #here ML_Env.local_context,
print = fn r => return := r,
error = #error ML_Env.local_context}
val _ =
Context.setmp_thread_data (SOME (Context.Proof ctxt))
(fn () =>
- Secure.use_text use_context
+ use_text use_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 () =>
- Secure.use_text ML_Env.local_context
+ use_text ML_Env.local_context
{line = 0, file = "generated code", verbose = false, debug = false} s) ();
(*split input into tokens*)