271 Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file" |
271 Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file" |
272 (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy => |
272 (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy => |
273 let |
273 let |
274 val ([{lines, pos, ...}], thy') = files thy; |
274 val ([{lines, pos, ...}], thy') = files thy; |
275 val source = {delimited = true, text = cat_lines lines, pos = pos}; |
275 val source = {delimited = true, text = cat_lines lines, pos = pos}; |
276 val flags = {SML = true, redirect = true, verbose = true}; |
276 val flags = {SML = true, exchange = false, redirect = true, verbose = true}; |
277 in |
277 in |
278 thy' |> Context.theory_map |
278 thy' |> Context.theory_map |
279 (ML_Context.exec (fn () => ML_Context.eval_source flags source)) |
279 (ML_Context.exec (fn () => ML_Context.eval_source flags source)) |
280 end))); |
280 end))); |
|
281 |
|
282 val _ = |
|
283 Outer_Syntax.command @{command_spec "SML_export"} "evaluate SML within Isabelle/ML environment" |
|
284 (Parse.ML_source >> (fn source => |
|
285 let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in |
|
286 Toplevel.theory |
|
287 (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source))) |
|
288 end)); |
|
289 |
|
290 val _ = |
|
291 Outer_Syntax.command @{command_spec "SML_import"} "evaluate Isabelle/ML within SML environment" |
|
292 (Parse.ML_source >> (fn source => |
|
293 let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in |
|
294 Toplevel.generic_theory |
|
295 (ML_Context.exec (fn () => ML_Context.eval_source flags source) #> |
|
296 Local_Theory.propagate_ml_env) |
|
297 end)); |
281 |
298 |
282 val _ = |
299 val _ = |
283 Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory" |
300 Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory" |
284 (Parse.ML_source >> (fn source => |
301 (Parse.ML_source >> (fn source => |
285 Toplevel.generic_theory |
302 Toplevel.generic_theory |