src/Pure/Pure.thy

--- 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"