--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/document Fri Oct 08 15:03:11 1999 +0200
@@ -0,0 +1,82 @@
+#!/bin/bash
+#
+# $Id$
+#
+# DESCRIPTION: prepare theory session document
+
+
+PRG=$(basename $0)
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS] [DIR]"
+ echo
+ echo " Options are:"
+ echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
+ echo
+ echo
+ echo " Prepare the theory session document in DIR (default .)"
+ echo " producing the speficied output format."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+# options
+
+OUTFORMAT=dvi
+
+while getopts "o:" OPT
+do
+ case "$OPT" in
+ o)
+ OUTFORMAT="$OPTARG"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+DIR="."
+[ $# -ge 1 ] && { DIR="$1"; shift; }
+
+[ $# -ne 0 ] && usage
+
+
+## main
+
+#prepare document
+
+cd "$DIR" || fail "Bad directory '$DIR'"
+
+if [ -f IsaMakefile ]; then
+ $ISATOOL make "$OUTFORMAT"
+ RC=$? #FIXME !??
+elif [ "$OUTFORMAT" = pdf ]; then
+ $ISATOOL latex -o pdf && $ISATOOL latex -o pdf
+ RC=$?
+else
+ $ISATOOL latex -o dvi && $ISATOOL latex -o "$OUTFORMAT"
+ RC=$?
+fi
+
+
+#install
+
+[ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
+cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"