diff -r 0e9ad8ad41d7 -r e0676a932348 lib/Tools/document
--- /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"