src/Pure/Isar/isar_syn.ML
changeset 56275 600f432ab556
parent 56240 938c6c7e10eb
child 56304 40274e4f5ebf
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Mar 25 10:37:10 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 25 13:18:10 2014 +0100
     1.3 @@ -268,17 +268,28 @@
     1.4  (* use ML text *)
     1.5  
     1.6  val _ =
     1.7 +  Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file"
     1.8 +    (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
     1.9 +        let
    1.10 +          val ([{lines, pos, ...}], thy') = files thy;
    1.11 +          val source = {delimited = true, text = cat_lines lines, pos = pos};
    1.12 +        in
    1.13 +          thy' |> Context.theory_map
    1.14 +            (ML_Context.exec (fn () => ML_Context.eval_source {SML = true, verbose = true} source))
    1.15 +        end)));
    1.16 +
    1.17 +val _ =
    1.18    Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
    1.19      (Parse.ML_source >> (fn source =>
    1.20        Toplevel.generic_theory
    1.21 -        (ML_Context.exec (fn () => ML_Context.eval_source true source) #>
    1.22 +        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) #>
    1.23            Local_Theory.propagate_ml_env)));
    1.24  
    1.25  val _ =
    1.26    Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
    1.27      (Parse.ML_source >> (fn source =>
    1.28        Toplevel.proof (Proof.map_context (Context.proof_map
    1.29 -        (ML_Context.exec (fn () => ML_Context.eval_source true source))) #>
    1.30 +        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source))) #>
    1.31            Proof.propagate_ml_env)));
    1.32  
    1.33  val _ =