--- a/src/Doc/Isar_Ref/Spec.thy Mon Apr 04 23:13:41 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Apr 04 23:58:48 2016 +0200
@@ -1026,7 +1026,7 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "SML_file"} & : & \<open>theory \<rightarrow> theory\<close> \\
+ @{command_def "SML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "ML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "ML"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "ML_prf"} & : & \<open>proof \<rightarrow> proof\<close> \\
@@ -1052,11 +1052,11 @@
\<close>}
\<^descr> \<^theory_text>\<open>SML_file name\<close> reads and evaluates the given Standard ML file. Top-level
- SML bindings are stored within the theory context; the initial environment
- is restricted to the Standard ML implementation of Poly/ML, without the many
- add-ons of Isabelle/ML. Multiple \<^theory_text>\<open>SML_file\<close> commands may be used to build
- larger Standard ML projects, independently of the regular Isabelle/ML
- environment.
+ SML bindings are stored within the (global or local) theory context; the
+ initial environment is restricted to the Standard ML implementation of
+ Poly/ML, without the many add-ons of Isabelle/ML. Multiple \<^theory_text>\<open>SML_file\<close>
+ commands may be used to build larger Standard ML projects, independently of
+ the regular Isabelle/ML environment.
\<^descr> \<^theory_text>\<open>ML_file name\<close> reads and evaluates the given ML file. The current theory
context is passed down to the ML toplevel and may be modified, using @{ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_file.ML Mon Apr 04 23:58:48 2016 +0200
@@ -0,0 +1,45 @@
+(* Title: Pure/ML/ml_file.ML
+ Author: Makarius
+
+Commands to load ML files.
+*)
+
+signature ML_FILE =
+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
+end;
+
+structure ML_File: ML_FILE =
+struct
+
+fun command SML debug files = Toplevel.generic_theory (fn gthy =>
+ let
+ 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 flags =
+ {SML = SML src_path, exchange = false, redirect = true, verbose = true,
+ debug = debug, writeln = writeln, warning = warning};
+ in
+ gthy
+ |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
+ |> Local_Theory.propagate_ml_env
+ |> Context.mapping provide (Local_Theory.background_theory provide)
+ end);
+
+val ML = command (K false);
+val SML = command (K true);
+
+val any =
+ command (fn path =>
+ (case try (#2 o Path.split_ext) path of
+ SOME "ML" => false
+ | SOME "sml" => true
+ | SOME "sig" => true
+ | _ =>
+ error ("Bad file name " ^ Path.print path ^
+ "\nExpected .ML for Isabelle/ML or .sml/.sig for Standard ML")));
+
+end;
--- a/src/Pure/Pure.thy Mon Apr 04 23:13:41 2016 +0200
+++ b/src/Pure/Pure.thy Mon Apr 04 23:58:48 2016 +0200
@@ -100,60 +100,33 @@
ML \<open>
local
-fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy =>
- let
- 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 flags: ML_Compiler.flags =
- {SML = 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)
- |> Local_Theory.propagate_ml_env
- |> Context.mapping provide (Local_Theory.background_theory provide)
- end);
-
-fun SML_file_cmd debug files = Toplevel.theory (fn thy =>
- let
- 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};
- in
- thy' |> Context.theory_map
- (ML_Context.exec (fn () => ML_Context.eval_source flags source))
- end);
-
val _ =
Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
- (Resources.parse_files "ML_file" >> ML_file_cmd NONE);
+ (Resources.parse_files "ML_file" >> ML_File.ML NONE);
val _ =
Outer_Syntax.command ("ML_file_debug", @{here})
"read and evaluate Isabelle/ML file (with debugger information)"
- (Resources.parse_files "ML_file_debug" >> ML_file_cmd (SOME true));
+ (Resources.parse_files "ML_file_debug" >> ML_File.ML (SOME true));
val _ =
Outer_Syntax.command ("ML_file_no_debug", @{here})
"read and evaluate Isabelle/ML file (no debugger information)"
- (Resources.parse_files "ML_file_no_debug" >> ML_file_cmd (SOME false));
+ (Resources.parse_files "ML_file_no_debug" >> ML_File.ML (SOME false));
val _ =
Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
- (Resources.provide_parse_files "SML_file" >> SML_file_cmd NONE);
+ (Resources.parse_files "SML_file" >> ML_File.SML NONE);
val _ =
Outer_Syntax.command @{command_keyword SML_file_debug}
"read and evaluate Standard ML file (with debugger information)"
- (Resources.provide_parse_files "SML_file_debug" >> SML_file_cmd (SOME true));
+ (Resources.parse_files "SML_file_debug" >> ML_File.SML (SOME true));
val _ =
Outer_Syntax.command @{command_keyword SML_file_no_debug}
"read and evaluate Standard ML file (no debugger information)"
- (Resources.provide_parse_files "SML_file_no_debug" >> SML_file_cmd (SOME false));
+ (Resources.parse_files "SML_file_no_debug" >> ML_File.SML (SOME false));
val _ =
Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
--- a/src/Pure/ROOT Mon Apr 04 23:13:41 2016 +0200
+++ b/src/Pure/ROOT Mon Apr 04 23:58:48 2016 +0200
@@ -107,6 +107,7 @@
"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"
--- a/src/Pure/ROOT.ML Mon Apr 04 23:13:41 2016 +0200
+++ b/src/Pure/ROOT.ML Mon Apr 04 23:58:48 2016 +0200
@@ -316,6 +316,7 @@
use "ML/ml_pp.ML";
use "ML/ml_antiquotations.ML";
use "ML/ml_thms.ML";
+use "ML/ml_file.ML";
use "Tools/build.ML";
use "Tools/named_thms.ML";