diff -r c46ff0efa1ce -r 941915a3b811 lib/Tools/latex
--- 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"