author | wenzelm |
Tue, 05 Apr 2016 18:16:11 +0200 | |
changeset 62871 | 4a6cbe1239fe |
parent 62868 | 61a691db1c4d |
child 62873 | 2f9c8a18f832 |
permissions | -rw-r--r-- |
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML/ML_Root.thy |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
3 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
4 |
Support for ML project ROOT file, with imitation of ML "use" commands. |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
5 |
*) |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
6 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
7 |
theory ML_Root |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
8 |
imports "../Pure" |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
9 |
keywords "use" "use_debug" "use_no_debug" :: thy_load |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
10 |
and "use_thy" :: thy_load |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
11 |
begin |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
12 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
13 |
ML \<open> |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
14 |
local |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
15 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
16 |
val _ = |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
17 |
Outer_Syntax.command @{command_keyword use} |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
18 |
"read and evaluate Isabelle/ML or SML file" |
62871 | 19 |
(Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE); |
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
20 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
21 |
val _ = |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
22 |
Outer_Syntax.command @{command_keyword use_debug} |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
23 |
"read and evaluate Isabelle/ML or SML file (with debugger information)" |
62871 | 24 |
(Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true)); |
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
25 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
26 |
val _ = |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
27 |
Outer_Syntax.command @{command_keyword use_no_debug} |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
28 |
"read and evaluate Isabelle/ML or SML file (no debugger information)" |
62871 | 29 |
(Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false)); |
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
30 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
31 |
val _ = |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
32 |
Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command" |
62871 | 33 |
(Parse.path -- @{keyword ";"} >> (fn _ => |
34 |
Toplevel.keep (fn _ => error "Undefined command 'use_thy'"))); |
|
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
35 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
36 |
in end |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
37 |
\<close> |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
38 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
39 |
end |