equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 theory ML_Root |
7 theory ML_Root |
8 imports Pure |
8 imports Pure |
9 keywords "use" "use_debug" "use_no_debug" :: thy_load |
9 keywords "use" "use_debug" "use_no_debug" :: thy_load |
10 and "use_thy" :: thy_load ("thy") |
|
11 begin |
10 begin |
12 |
11 |
13 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
12 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
14 |
13 |
15 ML \<open> |
14 ML \<open> |
28 val _ = |
27 val _ = |
29 Outer_Syntax.command @{command_keyword use_no_debug} |
28 Outer_Syntax.command @{command_keyword use_no_debug} |
30 "read and evaluate Isabelle/ML or SML file (no debugger information)" |
29 "read and evaluate Isabelle/ML or SML file (no debugger information)" |
31 (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false)); |
30 (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false)); |
32 |
31 |
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 |
32 in end |
39 \<close> |
33 \<close> |
40 |
34 |
41 end |
35 end |