--- a/NEWS Tue Apr 05 09:54:17 2016 +0200
+++ b/NEWS Tue Apr 05 22:31:28 2016 +0200
@@ -235,7 +235,7 @@
requiring separate files.
* Low-level ML system structures (like PolyML and RunCall) are no longer
-exposed to Isabelle/ML user-space. The system option ML_system_unsafe
+exposed to Isabelle/ML user-space. The system option ML_system_bootstrap
allows to override this for special test situations.
* Antiquotation @{make_string} is available during Pure bootstrap --
--- a/etc/options Tue Apr 05 09:54:17 2016 +0200
+++ b/etc/options Tue Apr 05 22:31:28 2016 +0200
@@ -126,8 +126,8 @@
public option ML_system_64 : bool = false
-- "ML system for 64bit platform is used if possible (change requires restart)"
-option ML_system_unsafe : bool = false
- -- "provide access to low-level ML system structures"
+option ML_system_bootstrap : bool = false
+ -- "provide access to low-level ML system structures (unsafe!)"
section "Editor Reactivity"
--- a/lib/scripts/isabelle-platform Tue Apr 05 09:54:17 2016 +0200
+++ b/lib/scripts/isabelle-platform Tue Apr 05 22:31:28 2016 +0200
@@ -4,6 +4,7 @@
#
# NOTE: The ML system or JVM may have their own idea about the platform!
+ISABELLE_WINDOWS_PREFIX=""
ISABELLE_PLATFORM_FAMILY=""
ISABELLE_PLATFORM32=""
ISABELLE_PLATFORM64=""
@@ -11,6 +12,7 @@
case $(uname -s) in
Linux)
ISABELLE_PLATFORM_FAMILY="linux"
+ ISABELLE_WINDOWS_PREFIX="."
case $(uname -m) in
i?86)
ISABELLE_PLATFORM32=x86-linux
@@ -23,6 +25,7 @@
;;
Darwin)
ISABELLE_PLATFORM_FAMILY="macos"
+ ISABELLE_WINDOWS_PREFIX="."
case $(uname -m) in
i?86)
ISABELLE_PLATFORM32=x86-darwin
@@ -38,6 +41,7 @@
;;
CYGWIN_NT*)
ISABELLE_PLATFORM_FAMILY="windows"
+ ISABELLE_WINDOWS_PREFIX="windows"
case $(uname -m) in
i?86 | x86_64)
ISABELLE_PLATFORM32=x86-cygwin
--- a/src/Doc/Implementation/ML.thy Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Doc/Implementation/ML.thy Tue Apr 05 22:31:28 2016 +0200
@@ -616,15 +616,15 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
+ @{index_ML Context.the_generic_context: "unit -> Context.generic"} \\
@{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
@{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
@{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
\end{mldecls}
- \<^descr> @{ML "ML_Context.the_generic_context ()"} refers to the theory context of
+ \<^descr> @{ML "Context.the_generic_context ()"} refers to the theory context of
the ML toplevel --- at compile time. ML code needs to take care to refer to
- @{ML "ML_Context.the_generic_context ()"} correctly. Recall that evaluation
+ @{ML "Context.the_generic_context ()"} correctly. Recall that evaluation
of a function body is delayed until actual run-time.
\<^descr> @{ML "Context.>>"}~\<open>f\<close> applies context transformation \<open>f\<close> to the implicit
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Tue Apr 05 22:31:28 2016 +0200
@@ -582,7 +582,7 @@
case match_aterms varsubst b' a' of
NONE =>
let
- fun mk s = Syntax.string_of_term_global Pure.thy
+ fun mk s = Syntax.string_of_term_global @{theory Pure}
(infer_types (naming_of computer) (encoding_of computer) ty s)
val left = "computed left side: "^(mk a')
val right = "computed right side: "^(mk b')
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Apr 05 22:31:28 2016 +0200
@@ -280,7 +280,7 @@
val output_value = the_default "NONE"
(try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
- ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
+ ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))";
val ctxt' = ctxt
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
|> Context.proof_map (exec false ml_code);
--- a/src/Provers/splitter.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Provers/splitter.ML Tue Apr 05 22:31:28 2016 +0200
@@ -98,9 +98,9 @@
val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *)
-val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
- [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
- (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
+val lift = Goal.prove_global @{theory Pure} ["P", "Q", "R"]
+ [Syntax.read_prop_global @{theory Pure} "!!x :: 'b. Q(x) == R(x) :: 'c"]
+ (Syntax.read_prop_global @{theory Pure} "P(%x. Q(x)) == P(%x. R(x))")
(fn {context = ctxt, prems} =>
rewrite_goals_tac ctxt prems THEN resolve_tac ctxt [reflexive_thm] 1)
--- a/src/Pure/General/symbol.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/General/symbol.ML Tue Apr 05 22:31:28 2016 +0200
@@ -119,7 +119,7 @@
fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
fun raw_symbolic s =
- String.isPrefix "\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\<^" s);
+ String.isPrefix "\092<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\092<^" s);
fun is_symbolic s =
s <> open_ andalso s <> close andalso raw_symbolic s;
@@ -131,7 +131,7 @@
else is_utf8 s orelse raw_symbolic s;
fun is_control s =
- String.isPrefix "\<^" s andalso String.isSuffix ">" s;
+ String.isPrefix "\092<^" s andalso String.isSuffix ">" s;
(* input source control *)
@@ -142,8 +142,8 @@
val stopper = Scan.stopper (K eof) is_eof;
fun is_malformed s =
- String.isPrefix "\<" s andalso not (String.isSuffix ">" s)
- orelse s = "\<>" orelse s = "\<^>";
+ String.isPrefix "\092<" s andalso not (String.isSuffix ">" s)
+ orelse s = "\092<>" orelse s = "\092<^>";
fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
@@ -201,9 +201,9 @@
fun encode_raw "" = ""
| encode_raw str =
let
- val raw0 = enclose "\<^raw:" ">";
+ val raw0 = enclose "\092<^raw:" ">";
val raw1 = raw0 o implode;
- val raw2 = enclose "\<^raw" ">" o string_of_int o ord;
+ val raw2 = enclose "\092<^raw" ">" o string_of_int o ord;
fun encode cs = enc (take_prefix raw_chr cs)
and enc ([], []) = []
@@ -233,11 +233,11 @@
(* decode_raw *)
fun is_raw s =
- String.isPrefix "\<^raw" s andalso String.isSuffix ">" s;
+ String.isPrefix "\092<^raw" s andalso String.isSuffix ">" s;
fun decode_raw s =
if not (is_raw s) then error (malformed_msg s)
- else if String.isPrefix "\<^raw:" s then String.substring (s, 7, size s - 8)
+ else if String.isPrefix "\092<^raw:" s then String.substring (s, 7, size s - 8)
else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
@@ -563,8 +563,8 @@
fun sym_len s =
if not (is_printable s) then (0: int)
- else if String.isPrefix "\<long" s then 2
- else if String.isPrefix "\<Long" s then 2
+ else if String.isPrefix "\092<long" s then 2
+ else if String.isPrefix "\092<Long" s then 2
else 1;
fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
--- a/src/Pure/Isar/attrib.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Apr 05 22:31:28 2016 +0200
@@ -515,11 +515,11 @@
register_config Name_Space.names_long_raw #>
register_config Name_Space.names_short_raw #>
register_config Name_Space.names_unique_raw #>
+ register_config ML_Print_Depth.print_depth_raw #>
register_config ML_Options.source_trace_raw #>
register_config ML_Options.exception_trace_raw #>
register_config ML_Options.exception_debugger_raw #>
register_config ML_Options.debugger_raw #>
- register_config ML_Options.print_depth_raw #>
register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
register_config Goal_Display.show_main_goal_raw #>
--- a/src/Pure/Isar/isar_syn.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Apr 05 22:31:28 2016 +0200
@@ -197,8 +197,8 @@
val provide = Resources.provide (src_path, digest);
val source = Input.source true (cat_lines lines) (pos, pos);
val flags: ML_Compiler.flags =
- {SML = false, exchange = false, redirect = true, verbose = true,
- debug = debug, writeln = writeln, warning = warning};
+ {SML_syntax = false, SML_env = false, exchange = false, redirect = true,
+ verbose = true, debug = debug, writeln = writeln, warning = warning};
in
gthy
|> ML_Context.exec (fn () => ML_Context.eval_source flags source)
@@ -211,8 +211,8 @@
val ([{lines, pos, ...}: Token.file], thy') = files thy;
val source = Input.source true (cat_lines lines) (pos, pos);
val flags: ML_Compiler.flags =
- {SML = true, exchange = false, redirect = true, verbose = true,
- debug = debug, writeln = writeln, warning = warning};
+ {SML_syntax = true, SML_env = true, exchange = false, redirect = true,
+ verbose = true, debug = debug, writeln = writeln, warning = warning};
in
thy' |> Context.theory_map
(ML_Context.exec (fn () => ML_Context.eval_source flags source))
@@ -255,8 +255,8 @@
(Parse.ML_source >> (fn source =>
let
val flags: ML_Compiler.flags =
- {SML = true, exchange = true, redirect = false, verbose = true,
- debug = NONE, writeln = writeln, warning = warning};
+ {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
+ verbose = true, debug = NONE, writeln = writeln, warning = warning};
in
Toplevel.theory
(Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
@@ -267,8 +267,8 @@
(Parse.ML_source >> (fn source =>
let
val flags: ML_Compiler.flags =
- {SML = false, exchange = true, redirect = false, verbose = true,
- debug = NONE, writeln = writeln, warning = warning};
+ {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
+ verbose = true, debug = NONE, writeln = writeln, warning = warning};
in
Toplevel.generic_theory
(ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
--- a/src/Pure/Isar/outer_syntax.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Tue Apr 05 22:31:28 2016 +0200
@@ -120,7 +120,7 @@
NONE => ()
| SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
val _ =
- Context_Position.report_generic (ML_Context.the_generic_context ())
+ Context_Position.report_generic (Context.the_generic_context ())
(command_pos cmd) (command_markup true (name, cmd));
in Data.map (Symtab.update (name, cmd)) thy end;
--- a/src/Pure/Isar/runtime.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Isar/runtime.ML Tue Apr 05 22:31:28 2016 +0200
@@ -43,7 +43,7 @@
fun pretty_exn (exn: exn) =
Pretty.from_ML
(ML_Pretty.from_polyml
- (ML_system_pretty (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
+ (ML_system_pretty (exn, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))));
(* exn_context *)
--- a/src/Pure/ML/ml_compiler.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML Tue Apr 05 22:31:28 2016 +0200
@@ -7,7 +7,7 @@
signature ML_COMPILER =
sig
type flags =
- {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+ {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
debug: bool option, writeln: string -> unit, warning: string -> unit}
val debug_flags: bool option -> flags
val flags: flags
@@ -21,18 +21,19 @@
(* flags *)
type flags =
- {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+ {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
debug: bool option, writeln: string -> unit, warning: string -> unit};
fun debug_flags opt_debug : flags =
- {SML = false, exchange = false, redirect = false, verbose = false,
+ {SML_syntax = false, SML_env = false, exchange = false, redirect = false, verbose = false,
debug = opt_debug, writeln = writeln, warning = warning};
val flags = debug_flags NONE;
fun verbose b (flags: flags) =
- {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
- verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
+ {SML_syntax = #SML_syntax flags, SML_env = #SML_env flags, exchange = #exchange flags,
+ redirect = #redirect flags, verbose = b, debug = #debug flags,
+ writeln = #writeln flags, warning = #warning flags};
(* parse trees *)
@@ -144,7 +145,7 @@
fun eval (flags: flags) pos toks =
let
- val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
+ val space = ML_Env.make_name_space {SML = #SML_env flags, exchange = #exchange flags};
val opt_context = Context.thread_data ();
@@ -153,7 +154,7 @@
val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
val input_explode =
- if #SML flags then String.explode
+ if #SML_syntax flags then String.explode
else maps (String.explode o Symbol.esc) o Symbol.explode;
val input_buffer =
@@ -198,7 +199,7 @@
(* results *)
- val depth = FixedInt.fromInt (ML_Options.get_print_depth ());
+ val depth = FixedInt.fromInt (ML_Print_Depth.get_print_depth ());
fun apply_result {fixes, types, signatures, structures, functors, values} =
let
@@ -257,7 +258,7 @@
PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
PolyML.Compiler.CPFileName location_props,
- PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
+ PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth,
PolyML.Compiler.CPCompilerResultFun result_fun,
PolyML.Compiler.CPPrintInAlphabeticalOrder false,
PolyML.Compiler.CPDebug debug];
--- a/src/Pure/ML/ml_compiler0.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML Tue Apr 05 22:31:28 2016 +0200
@@ -69,7 +69,7 @@
| input line (#"@" :: #"{" :: #"m" :: #"a" :: #"k" :: #"e" :: #"_" ::
#"s" :: #"t" :: #"r" :: #"i" :: #"n" :: #"g" :: #"}" :: cs) res =
input line cs (ML_Pretty.make_string_fn "" :: res)
- | input line (#"\\" :: #"<" :: cs) res = input line cs ("\\\\<" :: res)
+ | input line (#"\\" :: #"<" :: cs) res = input line cs ("\092\092<" :: res)
| input line (#"\n" :: cs) res = input (line + 1) cs ("\n" :: res)
| input line (c :: cs) res = input line cs (str c :: res)
| input _ [] res = rev res;
--- a/src/Pure/ML/ml_context.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_context.ML Tue Apr 05 22:31:28 2016 +0200
@@ -6,9 +6,6 @@
signature ML_CONTEXT =
sig
- val the_generic_context: unit -> Context.generic
- val the_global_context: unit -> theory
- val the_local_context: unit -> Proof.context
val thm: xstring -> thm
val thms: xstring -> thm list
val exec: (unit -> unit) -> Context.generic -> Context.generic
@@ -35,12 +32,8 @@
(** implicit ML context **)
-val the_generic_context = Context.the_thread_data;
-val the_global_context = Context.theory_of o the_generic_context;
-val the_local_context = Context.proof_of o the_generic_context;
-
-fun thm name = Proof_Context.get_thm (the_local_context ()) name;
-fun thms name = Proof_Context.get_thms (the_local_context ()) name;
+fun thm name = Proof_Context.get_thm (Context.the_local_context ()) name;
+fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name;
fun exec (e: unit -> unit) context =
(case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
@@ -123,10 +116,10 @@
(ML_Lex.tokenize
("structure " ^ name ^ " =\nstruct\n\
\val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
- " (ML_Context.the_local_context ());\n\
+ " (Context.the_local_context ());\n\
\val ML_print_depth =\n\
- \ let val default = ML_Options.get_print_depth ()\n\
- \ in fn () => ML_Options.get_print_depth_default default end;\n"),
+ \ let val default = ML_Print_Depth.get_print_depth ()\n\
+ \ in fn () => ML_Print_Depth.get_print_depth_default default end;\n"),
ML_Lex.tokenize "end;");
fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");
@@ -218,7 +211,7 @@
in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
fun eval_source flags source =
- eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
+ eval flags (Input.pos_of source) (ML_Lex.read_source (#SML_syntax flags) source);
fun eval_in ctxt flags pos ants =
Context.setmp_thread_data (Option.map Context.Proof ctxt)
@@ -233,7 +226,7 @@
eval ML_Compiler.flags (#1 range)
(ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @
ML_Lex.read (": " ^ constraint ^ " =") @ ants @
- ML_Lex.read ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
+ ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
end;
--- a/src/Pure/ML/ml_env.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_env.ML Tue Apr 05 22:31:28 2016 +0200
@@ -12,6 +12,7 @@
val add_breakpoint: serial * (bool Unsynchronized.ref * Position.T) ->
Context.generic -> Context.generic
val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
+ val init_bootstrap: Context.generic -> Context.generic
val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
val context: ML_Compiler0.context
@@ -92,6 +93,23 @@
(* name space *)
+val init_bootstrap =
+ Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
+ let
+ val sml_tables' =
+ sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
+ let
+ val val2 =
+ fold (fn (x, y) =>
+ member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
+ (#allVal ML_Name_Space.global ()) val1;
+ val structure2 =
+ fold (fn (x, y) =>
+ member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
+ (#allStruct ML_Name_Space.global ()) structure1;
+ in (val2, type1, fixity1, structure2, signature1, functor1) end);
+ in make_data (bootstrap, tables, sml_tables', breakpoints) end);
+
fun add_name_space {SML} (space: ML_Name_Space.T) =
Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
let
@@ -112,7 +130,7 @@
let
fun lookup sel1 sel2 name =
if SML then
- Context.the_thread_data ()
+ Context.the_generic_context ()
|> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
else
Context.thread_data ()
@@ -121,7 +139,7 @@
fun all sel1 sel2 () =
(if SML then
- Context.the_thread_data ()
+ Context.the_generic_context ()
|> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
else
Context.thread_data ()
--- a/src/Pure/ML/ml_file.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_file.ML Tue Apr 05 22:31:28 2016 +0200
@@ -8,7 +8,7 @@
sig
val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
- val any: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
+ val use: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
end;
structure ML_File: ML_FILE =
@@ -19,9 +19,10 @@
val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
val provide = Resources.provide (src_path, digest);
val source = Input.source true (cat_lines lines) (pos, pos);
+ val (SML_syntax, SML_env) = SML src_path;
val flags =
- {SML = SML src_path, exchange = false, redirect = true, verbose = true,
- debug = debug, writeln = writeln, warning = warning};
+ {SML_syntax = SML_syntax, SML_env = SML_env, exchange = false, redirect = true,
+ verbose = true, debug = debug, writeln = writeln, warning = warning};
in
gthy
|> ML_Context.exec (fn () => ML_Context.eval_source flags source)
@@ -29,15 +30,15 @@
|> Context.mapping provide (Local_Theory.background_theory provide)
end);
-val ML = command (K false);
-val SML = command (K true);
+val ML = command (K (false, false));
+val SML = command (K (true, true));
-val any =
+val use =
command (fn path =>
(case try (#2 o Path.split_ext) path of
- SOME "ML" => false
- | SOME "sml" => true
- | SOME "sig" => true
+ SOME "ML" => (false, true)
+ | SOME "sml" => (true, true)
+ | SOME "sig" => (true, true)
| _ =>
error ("Bad file name " ^ Path.print path ^
"\nExpected .ML for Isabelle/ML or .sml/.sig for Standard ML")));
--- a/src/Pure/ML/ml_name_space.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML Tue Apr 05 22:31:28 2016 +0200
@@ -58,15 +58,22 @@
fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
- (* Standard ML name space *)
+ (* bootstrap environment *)
- val exclude_structures = ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
+ val bootstrap_values =
+ ["use", "exit", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
+ val bootstrap_structures =
+ ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
- val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
+
+ (* Standard ML environment *)
+
+ val sml_val =
+ List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_values) (#allVal global ());
val sml_type = #allType global ();
val sml_fixity = #allFix global ();
val sml_structure =
- List.filter (fn (a, _) => List.all (fn b => a <> b) exclude_structures) (#allStruct global ());
+ List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ());
val sml_signature = #allSig global ();
val sml_functor = #allFunct global ();
end;
--- a/src/Pure/ML/ml_options.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_options.ML Tue Apr 05 22:31:28 2016 +0200
@@ -17,10 +17,6 @@
val debugger_raw: Config.raw
val debugger: bool Config.T
val debugger_enabled: Context.generic option -> bool
- val print_depth_raw: Config.raw
- val print_depth: int Config.T
- val get_print_depth: unit -> int
- val get_print_depth_default: int -> int
end;
structure ML_Options: ML_OPTIONS =
@@ -62,21 +58,4 @@
(Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
| debugger_enabled (SOME context) = Config.get_generic context debugger;
-
-(* print depth *)
-
-val print_depth_raw =
- Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (ML_Pretty.get_print_depth ()));
-val print_depth = Config.int print_depth_raw;
-
-fun get_print_depth () =
- (case Context.thread_data () of
- NONE => ML_Pretty.get_print_depth ()
- | SOME context => Config.get_generic context print_depth);
-
-fun get_print_depth_default default =
- (case Context.thread_data () of
- NONE => default
- | SOME context => Config.get_generic context print_depth);
-
end;
--- a/src/Pure/ML/ml_pervasive_final.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_pervasive_final.ML Tue Apr 05 22:31:28 2016 +0200
@@ -4,15 +4,14 @@
Pervasive ML environment: final setup.
*)
-if Options.default_bool "ML_system_unsafe" then ()
+if Options.default_bool "ML_system_bootstrap" then ()
else
- (List.app ML_Name_Space.forget_structure (remove (op =) "PolyML" ML_Name_Space.exclude_structures);
- ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
+ (List.app ML_Name_Space.forget_structure
+ (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
+ ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
structure Output: OUTPUT = Output; (*seal system channels!*)
-structure Pure = struct val thy = Thy_Info.pure_theory () end;
-
Proofterm.proofs := 0;
Context.set_thread_data NONE;
--- a/src/Pure/ML/ml_pretty.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML Tue Apr 05 22:31:28 2016 +0200
@@ -19,8 +19,6 @@
'a list * FixedInt.int -> pretty
val to_polyml: pretty -> PolyML_Pretty.pretty
val from_polyml: PolyML_Pretty.pretty -> pretty
- val get_print_depth: unit -> int
- val print_depth: int -> unit
val format_polyml: int -> PolyML_Pretty.pretty -> string
val format: int -> pretty -> string
val make_string_fn: string -> string
@@ -91,16 +89,6 @@
in convert "" end;
-(* default print depth *)
-
-local
- val depth = Unsynchronized.ref 0;
-in
- fun get_print_depth () = ! depth;
- fun print_depth n = (depth := n; PolyML.print_depth n);
-end;
-
-
(* format *)
fun format_polyml margin prt =
@@ -123,8 +111,8 @@
if local_env <> "" then
pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()"))
else if List.exists (fn (a, _) => a = "Pretty") (#allStruct ML_Name_Space.global ()) then
- pretty_string_of (pretty_value "ML_Pretty.get_print_depth ()")
- else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Pretty.get_print_depth ()" ^ "))";
+ pretty_string_of (pretty_value "ML_Print_Depth.get_print_depth ()")
+ else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Print_Depth.get_print_depth ()" ^ "))";
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_print_depth.ML Tue Apr 05 22:31:28 2016 +0200
@@ -0,0 +1,37 @@
+(* Title: Pure/ML/ml_print_depth0.ML
+ Author: Makarius
+
+Print depth for ML toplevel pp: context option with global default.
+*)
+
+signature ML_PRINT_DEPTH =
+sig
+ val set_print_depth: int -> unit
+ val print_depth_raw: Config.raw
+ val print_depth: int Config.T
+ val get_print_depth: unit -> int
+ val get_print_depth_default: int -> int
+end;
+
+structure ML_Print_Depth: ML_PRINT_DEPTH =
+struct
+
+val set_print_depth = ML_Print_Depth.set_print_depth;
+
+val print_depth_raw =
+ Config.declare ("ML_print_depth", @{here})
+ (fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
+
+val print_depth = Config.int print_depth_raw;
+
+fun get_print_depth () =
+ (case Context.thread_data () of
+ NONE => ML_Print_Depth.get_print_depth ()
+ | SOME context => Config.get_generic context print_depth);
+
+fun get_print_depth_default default =
+ (case Context.thread_data () of
+ NONE => default
+ | SOME context => Config.get_generic context print_depth);
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_print_depth0.ML Tue Apr 05 22:31:28 2016 +0200
@@ -0,0 +1,23 @@
+(* Title: Pure/ML/ml_print_depth0.ML
+ Author: Makarius
+
+Print depth for ML toplevel pp -- global default (unsynchronized).
+*)
+
+signature ML_PRINT_DEPTH =
+sig
+ val set_print_depth: int -> unit
+ val get_print_depth: unit -> int
+ val get_print_depth_default: int -> int
+end;
+
+structure ML_Print_Depth: ML_PRINT_DEPTH =
+struct
+
+val depth = Unsynchronized.ref 0;
+
+fun set_print_depth n = (depth := n; PolyML.print_depth n);
+fun get_print_depth () = ! depth;
+fun get_print_depth_default _ = ! depth;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_root.scala Tue Apr 05 22:31:28 2016 +0200
@@ -0,0 +1,54 @@
+/* Title: Pure/ML/ml_root.scala
+ Author: Makarius
+
+Support for ML project ROOT file, with imitation of ML "use" commands.
+*/
+
+package isabelle
+
+
+object ML_Root
+{
+ /* parser */
+
+ val ROOT_ML = Path.explode("ROOT.ML")
+
+ val USE = "use"
+ val USE_DEBUG = "use_debug"
+ val USE_NO_DEBUG = "use_no_debug"
+ val USE_THY = "use_thy"
+
+ lazy val syntax =
+ Outer_Syntax.init() + ";" +
+ (USE, Some((Keyword.THY_LOAD, Nil)), None) +
+ (USE_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
+ (USE_NO_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
+ (USE_THY, Some((Keyword.THY_LOAD, List("thy"))), None)
+
+ private object Parser extends Parse.Parser
+ {
+ val entry: Parser[(String, String)] =
+ (command(USE) | command(USE_DEBUG) | command(USE_NO_DEBUG) | command(USE_THY)) ~!
+ (string ~ $$$(";")) ^^ { case a ~ (b ~ _) => (a, b) }
+
+ def parse(in: Token.Reader): ParseResult[List[(String, String)]] =
+ parse_all(rep(entry), in)
+ }
+
+ def read(dir: Path): List[(String, Path)] =
+ {
+ val root = dir + ROOT_ML
+
+ val toks = Token.explode(syntax.keywords, File.read(root))
+ val start = Token.Pos.file(root.implode)
+
+ Parser.parse(Token.reader(toks, start)) match {
+ case Parser.Success(entries, _) =>
+ for ((a, b) <- entries) yield {
+ val path = dir + Path.explode(b)
+ (a, if (a == USE_THY) Resources.thy_path(path) else path)
+ }
+ case bad => error(bad.toString)
+ }
+ }
+}
--- a/src/Pure/ML/ml_thms.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_thms.ML Tue Apr 05 22:31:28 2016 +0200
@@ -113,7 +113,7 @@
fun merge _ = [];
);
-fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ());
+fun get_stored_thms () = Stored_Thms.get (Context.the_global_context ());
val get_stored_thm = hd o get_stored_thms;
fun ml_store get (name, ths) =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML_Root.thy Tue Apr 05 22:31:28 2016 +0200
@@ -0,0 +1,41 @@
+(* Title: Pure/ML_Root.thy
+ Author: Makarius
+
+Support for ML project ROOT file, with imitation of ML "use" commands.
+*)
+
+theory ML_Root
+imports Pure
+keywords "use" "use_debug" "use_no_debug" :: thy_load
+ and "use_thy" :: thy_load ("thy")
+begin
+
+setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
+
+ML \<open>
+local
+
+val _ =
+ Outer_Syntax.command @{command_keyword use}
+ "read and evaluate Isabelle/ML or SML file"
+ (Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE);
+
+val _ =
+ Outer_Syntax.command @{command_keyword use_debug}
+ "read and evaluate Isabelle/ML or SML file (with debugger information)"
+ (Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true));
+
+val _ =
+ Outer_Syntax.command @{command_keyword use_no_debug}
+ "read and evaluate Isabelle/ML or SML file (no debugger information)"
+ (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
+
+val _ =
+ Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command"
+ (Parse.path -- @{keyword ";"} >> (fn _ =>
+ Toplevel.keep (fn _ => error "Undefined command 'use_thy'")));
+
+in end
+\<close>
+
+end
--- a/src/Pure/Pure.thy Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Pure.thy Tue Apr 05 22:31:28 2016 +0200
@@ -101,16 +101,16 @@
local
val _ =
- Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
+ Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file"
(Resources.parse_files "ML_file" >> ML_File.ML NONE);
val _ =
- Outer_Syntax.command ("ML_file_debug", @{here})
+ Outer_Syntax.command @{command_keyword ML_file_debug}
"read and evaluate Isabelle/ML file (with debugger information)"
(Resources.parse_files "ML_file_debug" >> ML_File.ML (SOME true));
val _ =
- Outer_Syntax.command ("ML_file_no_debug", @{here})
+ Outer_Syntax.command @{command_keyword ML_file_no_debug}
"read and evaluate Isabelle/ML file (no debugger information)"
(Resources.parse_files "ML_file_no_debug" >> ML_File.ML (SOME false));
@@ -133,8 +133,8 @@
(Parse.ML_source >> (fn source =>
let
val flags: ML_Compiler.flags =
- {SML = true, exchange = true, redirect = false, verbose = true,
- debug = NONE, writeln = writeln, warning = warning};
+ {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
+ verbose = true, debug = NONE, writeln = writeln, warning = warning};
in
Toplevel.theory
(Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
@@ -145,8 +145,8 @@
(Parse.ML_source >> (fn source =>
let
val flags: ML_Compiler.flags =
- {SML = false, exchange = true, redirect = false, verbose = true,
- debug = NONE, writeln = writeln, warning = warning};
+ {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
+ verbose = true, debug = NONE, writeln = writeln, warning = warning};
in
Toplevel.generic_theory
(ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
--- a/src/Pure/ROOT Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ROOT Tue Apr 05 22:31:28 2016 +0200
@@ -1,241 +1,9 @@
chapter Pure
session Pure =
- global_theories Pure
+ global_theories
+ Pure
+ theories
+ ML_Root
files
- "Concurrent/cache.ML"
- "Concurrent/counter.ML"
- "Concurrent/event_timer.ML"
- "Concurrent/future.ML"
- "Concurrent/lazy.ML"
- "Concurrent/mailbox.ML"
- "Concurrent/multithreading.ML"
- "Concurrent/par_exn.ML"
- "Concurrent/par_list.ML"
- "Concurrent/single_assignment.ML"
- "Concurrent/standard_thread.ML"
- "Concurrent/synchronized.ML"
- "Concurrent/task_queue.ML"
- "Concurrent/timeout.ML"
- "Concurrent/unsynchronized.ML"
- "General/alist.ML"
- "General/antiquote.ML"
- "General/balanced_tree.ML"
- "General/basics.ML"
- "General/binding.ML"
- "General/buffer.ML"
- "General/change_table.ML"
- "General/completion.ML"
- "General/exn.ML"
- "General/file.ML"
- "General/graph.ML"
- "General/graph_display.ML"
- "General/heap.ML"
- "General/input.ML"
- "General/integer.ML"
- "General/linear_set.ML"
- "General/long_name.ML"
- "General/name_space.ML"
- "General/ord_list.ML"
- "General/output.ML"
- "General/path.ML"
- "General/position.ML"
- "General/pretty.ML"
- "General/print_mode.ML"
- "General/properties.ML"
- "General/queue.ML"
- "General/random.ML"
- "General/same.ML"
- "General/scan.ML"
- "General/seq.ML"
- "General/sha1.ML"
- "General/socket_io.ML"
- "General/source.ML"
- "General/stack.ML"
- "General/symbol.ML"
- "General/symbol_pos.ML"
- "General/table.ML"
- "General/timing.ML"
- "General/url.ML"
- "Isar/args.ML"
- "Isar/attrib.ML"
- "Isar/auto_bind.ML"
- "Isar/bundle.ML"
- "Isar/calculation.ML"
- "Isar/class.ML"
- "Isar/class_declaration.ML"
- "Isar/code.ML"
- "Isar/context_rules.ML"
- "Isar/element.ML"
- "Isar/experiment.ML"
- "Isar/expression.ML"
- "Isar/generic_target.ML"
- "Isar/interpretation.ML"
- "Isar/isar_cmd.ML"
- "Isar/keyword.ML"
- "Isar/local_defs.ML"
- "Isar/local_theory.ML"
- "Isar/locale.ML"
- "Isar/method.ML"
- "Isar/named_target.ML"
- "Isar/object_logic.ML"
- "Isar/obtain.ML"
- "Isar/outer_syntax.ML"
- "Isar/overloading.ML"
- "Isar/parse.ML"
- "Isar/parse_spec.ML"
- "Isar/proof.ML"
- "Isar/proof_context.ML"
- "Isar/proof_display.ML"
- "Isar/proof_node.ML"
- "Isar/rule_cases.ML"
- "Isar/runtime.ML"
- "Isar/spec_rules.ML"
- "Isar/specification.ML"
- "Isar/subgoal.ML"
- "Isar/token.ML"
- "Isar/toplevel.ML"
- "Isar/typedecl.ML"
- "ML/exn_debugger.ML"
- "ML/exn_properties.ML"
- "ML/ml_antiquotation.ML"
- "ML/ml_antiquotations.ML"
- "ML/ml_compiler.ML"
- "ML/ml_compiler0.ML"
- "ML/ml_compiler1.ML"
- "ML/ml_compiler2.ML"
- "ML/ml_context.ML"
- "ML/ml_debugger.ML"
- "ML/ml_env.ML"
- "ML/ml_file.ML"
- "ML/ml_heap.ML"
- "ML/ml_lex.ML"
- "ML/ml_name_space.ML"
- "ML/ml_options.ML"
- "ML/ml_pervasive_final.ML"
- "ML/ml_pervasive_initial.ML"
- "ML/ml_pp.ML"
- "ML/ml_pretty.ML"
- "ML/ml_profiling.ML"
- "ML/ml_statistics.ML"
- "ML/ml_syntax.ML"
- "ML/ml_system.ML"
- "ML/ml_thms.ML"
- "PIDE/active.ML"
- "PIDE/command.ML"
- "PIDE/command_span.ML"
- "PIDE/document.ML"
- "PIDE/document_id.ML"
- "PIDE/execution.ML"
- "PIDE/markup.ML"
- "PIDE/protocol.ML"
- "PIDE/protocol_message.ML"
- "PIDE/query_operation.ML"
- "PIDE/resources.ML"
- "PIDE/session.ML"
- "PIDE/xml.ML"
- "PIDE/yxml.ML"
- "Proof/extraction.ML"
- "Proof/proof_checker.ML"
- "Proof/proof_rewrite_rules.ML"
- "Proof/proof_syntax.ML"
- "Proof/reconstruct.ML"
"ROOT.ML"
- "Syntax/ast.ML"
- "Syntax/lexicon.ML"
- "Syntax/local_syntax.ML"
- "Syntax/mixfix.ML"
- "Syntax/parser.ML"
- "Syntax/printer.ML"
- "Syntax/simple_syntax.ML"
- "Syntax/syntax.ML"
- "Syntax/syntax_ext.ML"
- "Syntax/syntax_phases.ML"
- "Syntax/syntax_trans.ML"
- "Syntax/term_position.ML"
- "Syntax/type_annotation.ML"
- "System/bash.ML"
- "System/command_line.ML"
- "System/distribution.ML"
- "System/invoke_scala.ML"
- "System/isabelle_process.ML"
- "System/isabelle_system.ML"
- "System/message_channel.ML"
- "System/options.ML"
- "System/system_channel.ML"
- "Thy/document_antiquotations.ML"
- "Thy/html.ML"
- "Thy/latex.ML"
- "Thy/markdown.ML"
- "Thy/present.ML"
- "Thy/term_style.ML"
- "Thy/thy_header.ML"
- "Thy/thy_info.ML"
- "Thy/thy_output.ML"
- "Thy/thy_syntax.ML"
- "Tools/bibtex.ML"
- "Tools/build.ML"
- "Tools/class_deps.ML"
- "Tools/debugger.ML"
- "Tools/find_consts.ML"
- "Tools/find_theorems.ML"
- "Tools/jedit.ML"
- "Tools/named_theorems.ML"
- "Tools/named_thms.ML"
- "Tools/plugin.ML"
- "Tools/print_operation.ML"
- "Tools/rail.ML"
- "Tools/rule_insts.ML"
- "Tools/simplifier_trace.ML"
- "Tools/thm_deps.ML"
- "Tools/thy_deps.ML"
- "assumption.ML"
- "axclass.ML"
- "config.ML"
- "conjunction.ML"
- "consts.ML"
- "context.ML"
- "context_position.ML"
- "conv.ML"
- "defs.ML"
- "drule.ML"
- "envir.ML"
- "facts.ML"
- "global_theory.ML"
- "goal.ML"
- "goal_display.ML"
- "item_net.ML"
- "library.ML"
- "logic.ML"
- "more_pattern.ML"
- "more_thm.ML"
- "more_unify.ML"
- "morphism.ML"
- "name.ML"
- "net.ML"
- "par_tactical.ML"
- "pattern.ML"
- "primitive_defs.ML"
- "proofterm.ML"
- "pure_syn.ML"
- "pure_thy.ML"
- "raw_simplifier.ML"
- "search.ML"
- "sign.ML"
- "simplifier.ML"
- "skip_proof.ML"
- "sorts.ML"
- "tactic.ML"
- "tactical.ML"
- "term.ML"
- "term_ord.ML"
- "term_sharing.ML"
- "term_subst.ML"
- "term_xml.ML"
- "theory.ML"
- "thm.ML"
- "type.ML"
- "type_infer.ML"
- "type_infer_context.ML"
- "unify.ML"
- "variable.ML"
--- a/src/Pure/ROOT.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ROOT.ML Tue Apr 05 22:31:28 2016 +0200
@@ -23,6 +23,7 @@
use "ML/ml_heap.ML";
use "ML/ml_profiling.ML";
+use "ML/ml_print_depth0.ML";
use "ML/ml_pretty.ML";
use "ML/ml_compiler0.ML";
use_no_debug "ML/ml_debugger.ML";
@@ -185,6 +186,7 @@
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
use "ML/ml_options.ML";
+use "ML/ml_print_depth.ML";
use_no_debug "ML/exn_debugger.ML";
use_no_debug "Isar/runtime.ML";
use "PIDE/execution.ML";
@@ -226,7 +228,7 @@
-(** bootstrap phase 3: towards Pure.thy and final ML toplevel setup *)
+(** bootstrap phase 3: towards theory "Pure" and final ML toplevel setup *)
(*basic proof engine*)
use "par_tactical.ML";
@@ -277,7 +279,7 @@
use "Proof/extraction.ML";
(*Isabelle system*)
-use "System/bash.ML";
+use "System/$ISABELLE_WINDOWS_PREFIX/bash.ML";
use "System/isabelle_system.ML";
@@ -337,3 +339,4 @@
use_thy "Pure";
use "ML/ml_pervasive_final.ML";
+use_thy "ML_Root";
--- a/src/Pure/System/bash.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/System/bash.ML Tue Apr 05 22:31:28 2016 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/System/bash.ML
Author: Makarius
-GNU bash processes, with propagation of interrupts.
+GNU bash processes, with propagation of interrupts -- POSIX version.
*)
signature BASH =
@@ -9,99 +9,6 @@
val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
end;
-if ML_System.platform_is_windows then ML
-\<open>
-structure Bash: BASH =
-struct
-
-val process = uninterruptible (fn restore_attributes => fn script =>
- let
- datatype result = Wait | Signal | Result of int;
- val result = Synchronized.var "bash_result" Wait;
-
- val id = serial_string ();
- val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
- val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
- val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
- val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
-
- fun cleanup_files () =
- (try File.rm script_path;
- try File.rm out_path;
- try File.rm err_path;
- try File.rm pid_path);
- val _ = cleanup_files ();
-
- val system_thread =
- Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
- Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
- let
- val _ = File.write script_path script;
- val bash_script =
- "bash " ^ File.bash_path script_path ^
- " > " ^ File.bash_path out_path ^
- " 2> " ^ File.bash_path err_path;
- val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
- val rc =
- Windows.simpleExecute ("",
- quote (ML_System.platform_path bash_process) ^ " " ^
- quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script)
- |> Windows.fromStatus |> SysWord.toInt;
- val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
- in Synchronized.change result (K res) end
- handle exn =>
- (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
-
- fun read_pid 0 = NONE
- | read_pid count =
- (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
- NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
- | some => some);
-
- fun terminate NONE = ()
- | terminate (SOME pid) =
- let
- fun kill s =
- let
- val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
- val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
- in
- OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
- handle OS.SysErr _ => false
- end;
-
- fun multi_kill count s =
- count = 0 orelse
- (kill s; kill "0") andalso
- (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
- val _ =
- multi_kill 10 "INT" andalso
- multi_kill 10 "TERM" andalso
- multi_kill 10 "KILL";
- in () end;
-
- fun cleanup () =
- (Standard_Thread.interrupt_unsynchronized system_thread;
- cleanup_files ());
- in
- let
- val _ =
- restore_attributes (fn () =>
- Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
-
- val out = the_default "" (try File.read out_path);
- val err = the_default "" (try File.read err_path);
- val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
- val pid = read_pid 1;
- val _ = cleanup ();
- in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
- handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
- end);
-
-end;
-\<close>
-else ML
-\<open>
structure Bash: BASH =
struct
@@ -192,4 +99,3 @@
end);
end;
-\<close>;
--- a/src/Pure/System/isabelle_process.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/System/isabelle_process.ML Tue Apr 05 22:31:28 2016 +0200
@@ -209,7 +209,7 @@
(* init options *)
fun init_options () =
- (ML_Pretty.print_depth (Options.default_int "ML_print_depth");
+ (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
Future.ML_statistics := Options.default_bool "ML_statistics";
Multithreading.trace := Options.default_int "threads_trace";
Multithreading.max_threads_update (Options.default_int "threads");
--- a/src/Pure/System/options.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/System/options.ML Tue Apr 05 22:31:28 2016 +0200
@@ -215,11 +215,13 @@
| name =>
let val path = Path.explode name in
(case try File.read path of
- SOME s => (set_default (decode (YXML.parse_body s)); ignore (try File.rm path))
+ SOME s =>
+ (set_default (decode (YXML.parse_body s));
+ if default_bool "ML_system_bootstrap" then () else ignore (try File.rm path))
| NONE => ())
end);
val _ = load_default ();
-val _ = ML_Pretty.print_depth (default_int "ML_print_depth");
+val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth");
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/windows/bash.ML Tue Apr 05 22:31:28 2016 +0200
@@ -0,0 +1,99 @@
+(* Title: Pure/System/windows/bash.ML
+ Author: Makarius
+
+GNU bash processes, with propagation of interrupts -- Windows version.
+*)
+
+signature BASH =
+sig
+ val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
+struct
+
+val process = uninterruptible (fn restore_attributes => fn script =>
+ let
+ datatype result = Wait | Signal | Result of int;
+ val result = Synchronized.var "bash_result" Wait;
+
+ val id = serial_string ();
+ val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+ val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+ val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
+ val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
+
+ fun cleanup_files () =
+ (try File.rm script_path;
+ try File.rm out_path;
+ try File.rm err_path;
+ try File.rm pid_path);
+ val _ = cleanup_files ();
+
+ val system_thread =
+ Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+ Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+ let
+ val _ = File.write script_path script;
+ val bash_script =
+ "bash " ^ File.bash_path script_path ^
+ " > " ^ File.bash_path out_path ^
+ " 2> " ^ File.bash_path err_path;
+ val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
+ val rc =
+ Windows.simpleExecute ("",
+ quote (ML_System.platform_path bash_process) ^ " " ^
+ quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script)
+ |> Windows.fromStatus |> SysWord.toInt;
+ val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
+ in Synchronized.change result (K res) end
+ handle exn =>
+ (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
+
+ fun read_pid 0 = NONE
+ | read_pid count =
+ (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
+ NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
+ | some => some);
+
+ fun terminate NONE = ()
+ | terminate (SOME pid) =
+ let
+ fun kill s =
+ let
+ val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
+ val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
+ in
+ OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
+ handle OS.SysErr _ => false
+ end;
+
+ fun multi_kill count s =
+ count = 0 orelse
+ (kill s; kill "0") andalso
+ (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+ val _ =
+ multi_kill 10 "INT" andalso
+ multi_kill 10 "TERM" andalso
+ multi_kill 10 "KILL";
+ in () end;
+
+ fun cleanup () =
+ (Standard_Thread.interrupt_unsynchronized system_thread;
+ cleanup_files ());
+ in
+ let
+ val _ =
+ restore_attributes (fn () =>
+ Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
+
+ val out = the_default "" (try File.read out_path);
+ val err = the_default "" (try File.read err_path);
+ val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+ val pid = read_pid 1;
+ val _ = cleanup ();
+ in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
+ handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
+ end);
+
+end;
--- a/src/Pure/Thy/sessions.scala Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Thy/sessions.scala Tue Apr 05 22:31:28 2016 +0200
@@ -18,9 +18,6 @@
{
/* info */
- val ROOT = Path.explode("ROOT")
- val ROOTS = Path.explode("ROOTS")
-
def is_pure(name: String): Boolean = name == "Pure"
sealed case class Info(
@@ -141,6 +138,9 @@
/* parser */
+ val ROOT = Path.explode("ROOT")
+ val ROOTS = Path.explode("ROOTS")
+
private val CHAPTER = "chapter"
private val SESSION = "session"
private val IN = "in"
@@ -156,7 +156,7 @@
(CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
- object Parser extends Parse.Parser
+ private object Parser extends Parse.Parser
{
private abstract class Entry
private sealed case class Chapter(name: String) extends Entry
--- a/src/Pure/Thy/thy_info.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Apr 05 22:31:28 2016 +0200
@@ -260,7 +260,7 @@
val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
val (theory, present, weight) =
Resources.load_thy document symbols last_timing update_time dir header text_pos text
- (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
+ (if name = Context.PureN then [Context.the_global_context ()] else parents);
fun commit () = update_thy deps theory;
in
Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
--- a/src/Pure/Thy/thy_info.scala Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Thy/thy_info.scala Tue Apr 05 22:31:28 2016 +0200
@@ -14,6 +14,9 @@
sealed case class Dep(
name: Document.Node.Name,
header: Document.Node.Header)
+ {
+ override def toString: String = name.toString
+ }
}
class Thy_Info(resources: Resources)
@@ -94,6 +97,8 @@
val dep_files = Par_List.map(loaded _, rev_deps)
((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
}
+
+ override def toString: String = deps.toString
}
private def require_thys(session: String, initiators: List[Document.Node.Name],
--- a/src/Pure/Tools/build.scala Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Tools/build.scala Tue Apr 05 22:31:28 2016 +0200
@@ -173,7 +173,11 @@
val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
- val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
+ val loaded_files =
+ if (inlined_files)
+ thy_deps.loaded_files :::
+ (if (Sessions.is_pure(name)) ML_Root.read(info.dir).map(_._2) else Nil)
+ else Nil
val all_files =
(theory_files ::: loaded_files :::
--- a/src/Pure/Tools/debugger.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Tools/debugger.ML Tue Apr 05 22:31:28 2016 +0200
@@ -143,7 +143,7 @@
fun evaluate {SML, verbose} =
ML_Context.eval
- {SML = SML, exchange = false, redirect = false, verbose = verbose,
+ {SML_syntax = SML, SML_env = SML, exchange = false, redirect = false, verbose = verbose,
debug = SOME false, writeln = writeln_message, warning = warning_message}
Position.none;
@@ -155,7 +155,7 @@
fun eval_context thread_name index SML toks =
let
- val context = ML_Context.the_generic_context ();
+ val context = Context.the_generic_context ();
val context1 =
if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
then context
@@ -190,7 +190,7 @@
fun print x =
Pretty.from_polyml
- (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
+ (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), space));
fun print_all () =
#allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
|> sort_by #1 |> map (Pretty.item o single o print o #2)
--- a/src/Pure/build-jars Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/build-jars Tue Apr 05 22:31:28 2016 +0200
@@ -54,6 +54,7 @@
Isar/parse.scala
Isar/token.scala
ML/ml_lex.scala
+ ML/ml_root.scala
ML/ml_syntax.scala
PIDE/batch_session.scala
PIDE/command.scala
--- a/src/Pure/conjunction.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/conjunction.ML Tue Apr 05 22:31:28 2016 +0200
@@ -30,7 +30,7 @@
(** abstract syntax **)
-fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
+fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
val read_prop = certify o Simple_Syntax.read_prop;
val true_prop = certify Logic.true_prop;
@@ -76,7 +76,7 @@
val A_B = read_prop "A &&& B";
val conjunction_def =
- Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def";
+ Thm.unvarify_axiom (Context.the_global_context ()) "Pure.conjunction_def";
fun conjunctionD which =
Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
@@ -137,7 +137,7 @@
local
-val bootstrap_thy = Context.theory_of (Context.the_thread_data ());
+val bootstrap_thy = Context.the_global_context ();
fun conjs n =
let
--- a/src/Pure/context.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/context.ML Tue Apr 05 22:31:28 2016 +0200
@@ -74,9 +74,11 @@
val proof_of: generic -> Proof.context (*total*)
(*thread data*)
val thread_data: unit -> generic option
- val the_thread_data: unit -> generic
val set_thread_data: generic option -> unit
val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
+ val the_generic_context: unit -> generic
+ val the_global_context: unit -> theory
+ val the_local_context: unit -> Proof.context
val >> : (generic -> generic) -> unit
val >>> : (generic -> 'a * generic) -> 'a
end;
@@ -496,19 +498,22 @@
SOME (SOME context) => SOME context
| _ => NONE);
-fun the_thread_data () =
+fun set_thread_data context = Thread.setLocal (tag, context);
+fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
+
+fun the_generic_context () =
(case thread_data () of
SOME context => context
| _ => error "Unknown context");
-fun set_thread_data context = Thread.setLocal (tag, context);
-fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
+val the_global_context = theory_of o the_generic_context;
+val the_local_context = proof_of o the_generic_context;
end;
fun >>> f =
let
- val (res, context') = f (the_thread_data ());
+ val (res, context') = f (the_generic_context ());
val _ = set_thread_data (SOME context');
in res end;
--- a/src/Pure/drule.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/drule.ML Tue Apr 05 22:31:28 2016 +0200
@@ -134,7 +134,7 @@
(*The premises of a theorem, as a cterm list*)
val cprems_of = strip_imp_prems o Thm.cprop_of;
-fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
+fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
val implies = certify Logic.implies;
fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B;
@@ -570,7 +570,7 @@
local
val A = certify (Free ("A", propT));
- val axiom = Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ()));
+ val axiom = Thm.unvarify_axiom (Context.the_global_context ());
val prop_def = axiom "Pure.prop_def";
val term_def = axiom "Pure.term_def";
val sort_constraint_def = axiom "Pure.sort_constraint_def";
@@ -645,7 +645,7 @@
store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
(Thm.equal_intr
(Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
- (Thm.unvarify_global (Context.the_theory (Context.the_thread_data ())) sort_constraintI)))
+ (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
(implies_intr_list [A, C] (Thm.assume A)));
end;
--- a/src/Pure/pure_syn.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/pure_syn.ML Tue Apr 05 22:31:28 2016 +0200
@@ -55,7 +55,7 @@
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
-val bootstrap_thy = ML_Context.the_global_context ();
+val bootstrap_thy = Context.the_global_context ();
val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
--- a/src/Pure/raw_simplifier.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/raw_simplifier.ML Tue Apr 05 22:31:28 2016 +0200
@@ -1392,11 +1392,10 @@
Variable.gen_all ctxt;
val hhf_ss =
- simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
- addsimps Drule.norm_hhf_eqs);
+ simpset_of (empty_simpset (Context.the_local_context ()) addsimps Drule.norm_hhf_eqs);
val hhf_protect_ss =
- simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
+ simpset_of (empty_simpset (Context.the_local_context ())
addsimps Drule.norm_hhf_eqs |> add_eqcong Drule.protect_cong);
in
--- a/src/Tools/Code/code_runtime.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML Tue Apr 05 22:31:28 2016 +0200
@@ -88,7 +88,7 @@
let
val code = (prelude
^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
- ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
+ ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))");
val ctxt' = ctxt
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
|> Context.proof_map (exec ctxt false code);
@@ -539,7 +539,7 @@
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 ());
+ val thy'' = Context.the_global_context ();
val names = Loaded_Values.get thy'';
in (names, thy'') end;
--- a/src/Tools/Spec_Check/gen_construction.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Tools/Spec_Check/gen_construction.ML Tue Apr 05 22:31:28 2016 +0200
@@ -155,7 +155,7 @@
(*produce compilable string*)
fun build_check ctxt name (ty, spec) =
- "Spec_Check.checkGen (ML_Context.the_local_context ()) ("
+ "Spec_Check.checkGen (Context.the_local_context ()) ("
^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
^ name ^ "\", Property.pred (" ^ spec ^ "));";
--- a/src/Tools/Spec_Check/spec_check.ML Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Tools/Spec_Check/spec_check.ML Tue Apr 05 22:31:28 2016 +0200
@@ -192,5 +192,5 @@
end;
-fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s;
+fun check_property s = Spec_Check.check_property (Context.the_local_context ()) s;