src/Pure/Pure.thy

--- a/src/Pure/Pure.thy	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/Pure.thy	Thu Apr 07 16:53:43 2016 +0200
@@ -100,41 +100,43 @@
 ML \<open>
 local
 
+val semi = Scan.option @{keyword ";"};
+
 val _ =
   Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file"
-    (Resources.parse_files "ML_file" >> ML_File.ML NONE);
+    (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE);
 
 val _ =
   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));
+    (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true));
 
 val _ =
   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));
+    (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false));
 
 val _ =
   Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
-    (Resources.parse_files "SML_file" >> ML_File.SML NONE);
+    (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE);
 
 val _ =
   Outer_Syntax.command @{command_keyword SML_file_debug}
     "read and evaluate Standard ML file (with debugger information)"
-    (Resources.parse_files "SML_file_debug" >> ML_File.SML (SOME true));
+    (Resources.parse_files "SML_file_debug" --| semi >> 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.parse_files "SML_file_no_debug" >> ML_File.SML (SOME false));
+    (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false));
 
 val _ =
   Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
-            verbose = true, debug = NONE, writeln = writeln, warning = warning};
+          {SML = 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 +147,8 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
-            verbose = true, debug = NONE, writeln = writeln, warning = warning};
+          {SML = 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) #>