--- a/lib/Tools/document Sun Dec 10 14:50:44 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,158 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: prepare theory session document
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
- echo
- echo " Options are:"
- echo " -c cleanup -- be aggressive in removing old stuff"
- echo " -n NAME specify document name (default 'document')"
- echo " -o FORMAT specify output format: pdf (default), dvi"
- echo " -t TAGS specify tagged region markup"
- echo
- echo " Prepare the theory session document in DIR (default 'document')"
- echo " producing the specified output format."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-CLEAN=""
-NAME="document"
-OUTFORMAT=pdf
-declare -a TAGS=()
-
-while getopts "cn:o:t:" OPT
-do
- case "$OPT" in
- c)
- CLEAN=true
- ;;
- n)
- NAME="$OPTARG"
- ;;
- o)
- OUTFORMAT="$OPTARG"
- ;;
- t)
- splitarray "," "$OPTARG"; TAGS=("${SPLITARRAY[@]}")
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-DIR="document"
-[ "$#" -ge 1 ] && { DIR="$1"; shift; }
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-# check format
-
-case "$OUTFORMAT" in
- pdf | dvi)
- ;;
- *)
- fail "Bad output format '$OUTFORMAT'"
- ;;
-esac
-
-
-# document variants
-
-ROOT_NAME="root_$NAME"
-[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
-
-function prep_tags ()
-{
- (
- for TAG in "${TAGS[@]}"
- do
- case "$TAG" in
- /*)
- echo "\\isafoldtag{${TAG:1}}"
- ;;
- -*)
- echo "\\isadroptag{${TAG:1}}"
- ;;
- +*)
- echo "\\isakeeptag{${TAG:1}}"
- ;;
- *)
- echo "\\isakeeptag{${TAG}}"
- ;;
- esac
- done
- echo
- ) > isabelletags.sty
-}
-
-
-# prepare document
-
-(
- cd "$DIR" || fail "Bad directory '$DIR'"
-
- [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT" *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
-
- prep_tags
-
- if [ -f build ]; then
- ./build "$OUTFORMAT" "$NAME"
- RC="$?"
- else
- isabelle latex -o sty "$ROOT_NAME.tex" && \
- isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
- { [ ! -f "$ROOT_NAME.bib" ] || isabelle latex -o bbl "$ROOT_NAME.tex"; } && \
- { [ ! -f "$ROOT_NAME.idx" ] || isabelle latex -o idx "$ROOT_NAME.tex"; } && \
- isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
- isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
- RC="$?"
- fi
-
- if [ "$RC" -ne 0 ]; then
- isabelle latex_errors -n "$ROOT_NAME"
- elif [ -f "$ROOT_NAME.$OUTFORMAT" ]; then
- cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
- fi
-
- exit "$RC"
-)
-RC="$?"
-
-
-# install
-
-[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
-
-#beware!
-[ -n "$CLEAN" ] && rm -rf "$DIR"
-
-exit "$RC"