src/Pure/ML/ml_file.ML

--- a/src/Pure/ML/ml_file.ML	Mon Aug 17 16:27:12 2015 +0200
+++ b/src/Pure/ML/ml_file.ML	Mon Aug 17 19:34:15 2015 +0200
@@ -7,21 +7,33 @@
 structure ML_File: sig end =
 struct
 
+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);
+
 val _ =
-  Outer_Syntax.command ("ML_file", @{here}) "ML text from file"
-    (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
-        let
-          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: ML_Compiler.flags =
-            {SML = false, exchange = false, redirect = true, verbose = true,
-              debug = NONE, 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)));
+  Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
+    (Resources.parse_files "ML_file" >> ML_file_cmd 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));
+
+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));
 
 end;