author | wenzelm |
Tue, 05 Apr 2016 15:58:58 +0200 | |
changeset 62868 | 61a691db1c4d |
child 62871 | 4a6cbe1239fe |
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" |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
19 |
(Resources.parse_files "use" >> ML_File.use NONE); |
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)" |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
24 |
(Resources.parse_files "use_debug" >> ML_File.use (SOME true)); |
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)" |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
29 |
(Resources.parse_files "use_no_debug" >> ML_File.use (SOME false)); |
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" |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
33 |
(Scan.succeed (Toplevel.keep (fn _ => error "Undefined command 'use_thy'"))); |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
34 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
35 |
in end |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
36 |
\<close> |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
37 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
38 |
end |