lib/Tools/document

use open/close_target rather than Local_Theory.restore to get polymorphic definitions;

#!/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_TOOL" latex -o sty "$ROOT_NAME.tex" && \
    "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
    { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
    { [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
    "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
    "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
    RC="$?"
  fi

  if [ "$RC" -eq 0 -a -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"