src/Pure/Isar/isar_syn.ML
changeset 56618 874bdedb2313
parent 56467 8d7d6f17c6a7
child 56629 ca302c495bca
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 17 14:52:23 2014 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 19 17:23:05 2014 +0200
     1.3 @@ -273,13 +273,30 @@
     1.4          let
     1.5            val ([{lines, pos, ...}], thy') = files thy;
     1.6            val source = {delimited = true, text = cat_lines lines, pos = pos};
     1.7 -          val flags = {SML = true, redirect = true, verbose = true};
     1.8 +          val flags = {SML = true, exchange = false, redirect = true, verbose = true};
     1.9          in
    1.10            thy' |> Context.theory_map
    1.11              (ML_Context.exec (fn () => ML_Context.eval_source flags source))
    1.12          end)));
    1.13  
    1.14  val _ =
    1.15 +  Outer_Syntax.command @{command_spec "SML_export"} "evaluate SML within Isabelle/ML environment"
    1.16 +    (Parse.ML_source >> (fn source =>
    1.17 +      let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in
    1.18 +        Toplevel.theory
    1.19 +          (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
    1.20 +      end));
    1.21 +
    1.22 +val _ =
    1.23 +  Outer_Syntax.command @{command_spec "SML_import"} "evaluate Isabelle/ML within SML environment"
    1.24 +    (Parse.ML_source >> (fn source =>
    1.25 +      let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in
    1.26 +        Toplevel.generic_theory
    1.27 +          (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
    1.28 +            Local_Theory.propagate_ml_env)
    1.29 +      end));
    1.30 +
    1.31 +val _ =
    1.32    Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
    1.33      (Parse.ML_source >> (fn source =>
    1.34        Toplevel.generic_theory