equal
deleted
inserted
replaced
|
1 (* Title: Pure/ML_Root.thy |
|
2 Author: Makarius |
|
3 |
|
4 Support for ML project ROOT file, with imitation of ML "use" commands. |
|
5 *) |
|
6 |
|
7 theory ML_Root |
|
8 imports Pure |
|
9 keywords "use" "use_debug" "use_no_debug" :: thy_load |
|
10 and "use_thy" :: thy_load |
|
11 begin |
|
12 |
|
13 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
|
14 |
|
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 val _ = |
|
34 Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command" |
|
35 (Parse.path -- @{keyword ";"} >> (fn _ => |
|
36 Toplevel.keep (fn _ => error "Undefined command 'use_thy'"))); |
|
37 |
|
38 in end |
|
39 \<close> |
|
40 |
|
41 end |