author | wenzelm |
Thu, 13 Nov 2008 21:33:15 +0100 | |
changeset 28750 | 1ff7fff6a170 |
parent 28650 | a7ba12e0d3b7 |
child 29143 | 72c960b2b83e |
permissions | -rwxr-xr-x |
24185
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
2 |
# |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
3 |
# $Id$ |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
4 |
# Author: David Aspinall and Makarius Wenzel |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
5 |
# |
24206 | 6 |
# DESCRIPTION: prepare a session directory for PG-Eclipse |
24185
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
7 |
|
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
8 |
PRG="$(basename "$0")" |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
9 |
|
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
10 |
function usage() |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
11 |
{ |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
12 |
echo |
28650 | 13 |
echo "Usage: isabelle $PRG NAME" |
24185
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
14 |
echo |
24206 | 15 |
echo " Prepare a session directory for PG-Eclipse." |
24185
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
16 |
exit 1 |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
17 |
} |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
18 |
|
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
19 |
if [ "$#" -eq 1 ]; then |
24206 | 20 |
NAME="$1"; shift |
24185
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
21 |
else |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
22 |
usage |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
23 |
fi |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
24 |
|
28500 | 25 |
"$ISABELLE_TOOL" mkdir -b -q "$NAME" |
26 |
( cd document; "$ISABELLE_TOOL" latex -o sty; ) |