equal
deleted
inserted
replaced
4 ML bootstrap environment -- with access to low-level structures! |
4 ML bootstrap environment -- with access to low-level structures! |
5 *) |
5 *) |
6 |
6 |
7 theory ML_Bootstrap |
7 theory ML_Bootstrap |
8 imports Pure |
8 imports Pure |
9 keywords "use" "use_debug" "use_no_debug" :: thy_load |
|
10 begin |
9 begin |
11 |
10 |
12 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
11 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
13 SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close> |
12 SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close> |
14 |
13 setup \<open>Config.put_global ML_Env.SML_environment true\<close> |
15 ML \<open> |
|
16 local |
|
17 |
|
18 val _ = |
|
19 Outer_Syntax.command @{command_keyword use} |
|
20 "read and evaluate Isabelle/ML or SML file" |
|
21 (Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE); |
|
22 |
|
23 val _ = |
|
24 Outer_Syntax.command @{command_keyword use_debug} |
|
25 "read and evaluate Isabelle/ML or SML file (with debugger information)" |
|
26 (Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true)); |
|
27 |
|
28 val _ = |
|
29 Outer_Syntax.command @{command_keyword use_no_debug} |
|
30 "read and evaluate Isabelle/ML or SML file (no debugger information)" |
|
31 (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false)); |
|
32 |
|
33 in end |
|
34 \<close> |
|
35 |
14 |
36 end |
15 end |