1 (* Title: Pure/ML/ml_file.ML |
|
2 Author: Makarius |
|
3 |
|
4 The 'ML_file' command. |
|
5 *) |
|
6 |
|
7 structure ML_File: sig end = |
|
8 struct |
|
9 |
|
10 fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy => |
|
11 let |
|
12 val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy); |
|
13 val provide = Resources.provide (src_path, digest); |
|
14 val source = Input.source true (cat_lines lines) (pos, pos); |
|
15 val flags: ML_Compiler.flags = |
|
16 {SML = false, exchange = false, redirect = true, verbose = true, |
|
17 debug = debug, writeln = writeln, warning = warning}; |
|
18 in |
|
19 gthy |
|
20 |> ML_Context.exec (fn () => ML_Context.eval_source flags source) |
|
21 |> Local_Theory.propagate_ml_env |
|
22 |> Context.mapping provide (Local_Theory.background_theory provide) |
|
23 end); |
|
24 |
|
25 val _ = |
|
26 Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file" |
|
27 (Resources.parse_files "ML_file" >> ML_file_cmd NONE); |
|
28 |
|
29 val _ = |
|
30 Outer_Syntax.command ("ML_file_debug", @{here}) |
|
31 "read and evaluate Isabelle/ML file (with debugger information)" |
|
32 (Resources.parse_files "ML_file_debug" >> ML_file_cmd (SOME true)); |
|
33 |
|
34 val _ = |
|
35 Outer_Syntax.command ("ML_file_no_debug", @{here}) |
|
36 "read and evaluate Isabelle/ML file (no debugger information)" |
|
37 (Resources.parse_files "ML_file_no_debug" >> ML_file_cmd (SOME false)); |
|
38 |
|
39 end; |
|