src/Pure/Pure.thy
changeset 62902 3c0f53eae166
parent 62898 fdc290b68ecd
child 62913 13252110a6fe
     1.1 --- a/src/Pure/Pure.thy	Thu Apr 07 15:32:47 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Thu Apr 07 16:53:43 2016 +0200
     1.3 @@ -100,41 +100,43 @@
     1.4  ML \<open>
     1.5  local
     1.6  
     1.7 +val semi = Scan.option @{keyword ";"};
     1.8 +
     1.9  val _ =
    1.10    Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file"
    1.11 -    (Resources.parse_files "ML_file" >> ML_File.ML NONE);
    1.12 +    (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE);
    1.13  
    1.14  val _ =
    1.15    Outer_Syntax.command @{command_keyword ML_file_debug}
    1.16      "read and evaluate Isabelle/ML file (with debugger information)"
    1.17 -    (Resources.parse_files "ML_file_debug" >> ML_File.ML (SOME true));
    1.18 +    (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true));
    1.19  
    1.20  val _ =
    1.21    Outer_Syntax.command @{command_keyword ML_file_no_debug}
    1.22      "read and evaluate Isabelle/ML file (no debugger information)"
    1.23 -    (Resources.parse_files "ML_file_no_debug" >> ML_File.ML (SOME false));
    1.24 +    (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false));
    1.25  
    1.26  val _ =
    1.27    Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
    1.28 -    (Resources.parse_files "SML_file" >> ML_File.SML NONE);
    1.29 +    (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE);
    1.30  
    1.31  val _ =
    1.32    Outer_Syntax.command @{command_keyword SML_file_debug}
    1.33      "read and evaluate Standard ML file (with debugger information)"
    1.34 -    (Resources.parse_files "SML_file_debug" >> ML_File.SML (SOME true));
    1.35 +    (Resources.parse_files "SML_file_debug" --| semi >> ML_File.SML (SOME true));
    1.36  
    1.37  val _ =
    1.38    Outer_Syntax.command @{command_keyword SML_file_no_debug}
    1.39      "read and evaluate Standard ML file (no debugger information)"
    1.40 -    (Resources.parse_files "SML_file_no_debug" >> ML_File.SML (SOME false));
    1.41 +    (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false));
    1.42  
    1.43  val _ =
    1.44    Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
    1.45      (Parse.ML_source >> (fn source =>
    1.46        let
    1.47          val flags: ML_Compiler.flags =
    1.48 -          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
    1.49 -            verbose = true, debug = NONE, writeln = writeln, warning = warning};
    1.50 +          {SML = true, exchange = true, redirect = false, verbose = true,
    1.51 +            debug = NONE, writeln = writeln, warning = warning};
    1.52        in
    1.53          Toplevel.theory
    1.54            (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
    1.55 @@ -145,8 +147,8 @@
    1.56      (Parse.ML_source >> (fn source =>
    1.57        let
    1.58          val flags: ML_Compiler.flags =
    1.59 -          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
    1.60 -            verbose = true, debug = NONE, writeln = writeln, warning = warning};
    1.61 +          {SML = false, exchange = true, redirect = false, verbose = true,
    1.62 +            debug = NONE, writeln = writeln, warning = warning};
    1.63        in
    1.64          Toplevel.generic_theory
    1.65            (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>