--- a/lib/Tools/latex Wed May 19 11:54:58 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: run LaTeX (and related tools)
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
- echo
- echo " Options are:"
- echo " -o FORMAT specify output format: pdf (default), bbl, idx"
- echo
- echo " Run LaTeX (and related tools) on FILE (default root.tex),"
- echo " producing the specified output format."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-OUTFORMAT=pdf
-
-while getopts "o:" OPT
-do
- case "$OPT" in
- o)
- OUTFORMAT="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-FILE="root.tex"
-[ "$#" -ge 1 ] && { FILE="$1"; shift; }
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-# root file
-
-DIR="$(dirname "$FILE")"
-FILEBASE="$(basename "$FILE" .tex)"
-[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
-
-function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
-
-
-# operations
-
-case "$OUTFORMAT" in
- pdf)
- check_root
- $ISABELLE_PDFLATEX "$FILEBASE.tex"
- RC="$?"
- ;;
- bbl)
- check_root
- $ISABELLE_BIBTEX </dev/null "$FILEBASE"
- RC="$?"
- ;;
- idx)
- check_root
- $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"
- RC="$?"
- ;;
- *)
- fail "Bad output format '$OUTFORMAT'"
- ;;
-esac
-
-exit "$RC"