| author | Christian Urban <urbanc@in.tum.de> |
| Thu, 09 Oct 2008 12:58:50 -0400 | |
| changeset 21 | 2356e5c70d98 |
| parent 15 | 9da9ba2b095b |
| child 26 | 2311f81d7a22 |
| permissions | -rw-r--r-- |
|
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(* |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
Auxiliary antiquotations for the Cookbook. |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
*) |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
local structure O = ThyOutput |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
in |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
fun check_exists f = |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
if File.exists (Path.explode ("~~/src/" ^ f)) then ()
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
else error ("Source file " ^ quote f ^ " does not exist.")
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
val _ = O.add_commands |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
[("ML_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
(check_exists name; Pretty.str name))))]; |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
end |