diff -r 4e5ba4b23731 -r 13b5c3ff1954 lib/Tools/document
--- 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"