--- a/lib/Tools/document Tue Feb 08 20:14:09 2000 +0100
+++ b/lib/Tools/document Tue Feb 08 20:14:58 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/bash -x
#
# $Id$
#
@@ -13,10 +13,11 @@
echo "Usage: $PRG [OPTIONS] [DIR]"
echo
echo " Options are:"
+ echo " -c clean -- remove DIR after succesful run"
echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps,"
echo " ps.gz, pdf"
echo
- echo " Prepare the theory session document in DIR (default '.')"
+ echo " Prepare the theory session document in DIR (default 'document')"
echo " producing the specified output format."
echo
exit 1
@@ -33,11 +34,15 @@
# options
+CLEAN=""
OUTFORMAT=dvi
-while getopts "o:" OPT
+while getopts "co:" OPT
do
case "$OPT" in
+ c)
+ CLEAN=true
+ ;;
o)
OUTFORMAT="$OPTARG"
;;
@@ -52,7 +57,7 @@
# args
-DIR="."
+DIR="document"
[ $# -ge 1 ] && { DIR="$1"; shift; }
[ $# -ne 0 ] && usage
@@ -73,8 +78,6 @@
# prepare document
-cd "$DIR" || fail "Bad directory '$DIR'"
-
function pre_latex ()
{
local FMT="$1"
@@ -89,25 +92,39 @@
fi
}
-if [ -f IsaMakefile ]; then
- $ISATOOL make "$OUTFORMAT"
- RC=$? #FIXME !??
-elif [ "$OUTFORMAT" = pdf ]; then
- pre_latex pdf && \
- $ISATOOL latex -o pdf && \
- { if [ -n "$ISABELLE_THUMBPDF" ]; then
- $ISATOOL latex -o png && \
- $ISATOOL latex -o pdf
- fi; }
- RC=$?
-else
- pre_latex dvi && \
- $ISATOOL latex -o "$OUTFORMAT"
- RC=$?
-fi
+(
+ cd "$DIR" || fail "Bad directory '$DIR'"
+
+ if [ -f IsaMakefile ]; then
+ $ISATOOL make "$OUTFORMAT"
+ RC=$?
+ elif [ "$OUTFORMAT" = pdf ]; then
+ pre_latex pdf && \
+ $ISATOOL latex -o pdf && \
+ { if [ -n "$ISABELLE_THUMBPDF" ]; then
+ $ISATOOL latex -o png && \
+ $ISATOOL latex -o pdf
+ fi; }
+ RC=$?
+ else
+ pre_latex dvi && \
+ $ISATOOL latex -o "$OUTFORMAT"
+ RC=$?
+ fi
+
+ [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
+ cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
+
+ exit $RC
+)
+RC=$?
# install
-[ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
-cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
+[ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"
+
+#beware!
+[ -n "$CLEAN" ] && rm -rf "$DIR"
+
+exit "$RC"
--- a/lib/Tools/mkdir Tue Feb 08 20:14:09 2000 +0100
+++ b/lib/Tools/mkdir Tue Feb 08 20:14:58 2000 +0100
@@ -16,9 +16,9 @@
echo
echo " Options are:"
echo " -I FILE alternative IsaMakefile output"
+ echo " -P include parent logic target"
echo " -b setup build mode (session outputs heap image)"
echo " -d setup document"
- echo " -p include parent logic target"
echo
echo " Prepare session directory, including IsaMakefile, document etc."
echo " with parent LOGIC (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
@@ -38,25 +38,25 @@
# options
ISAMAKEFILE="IsaMakefile"
+PARENT=""
BUILD=""
DOCUMENT=""
-PARENT=""
-while getopts "I:bdp" OPT
+while getopts "I:Pbd" OPT
do
case "$OPT" in
I)
ISAMAKEFILE="$OPTARG"
;;
+ P)
+ PARENT=true
+ ;;
b)
BUILD=true
;;
d)
DOCUMENT=true
;;
- p)
- PARENT=true
- ;;
\?)
usage
;;
@@ -95,7 +95,7 @@
else
IMAGES=""
TEST="$NAME"
- TARGET="\$(LOG)/$NAME.gz"
+ TARGET="\$(LOG)/$LOGIC-$NAME.gz"
USEDIR="\$(USEDIR)"
fi