wenzelm@10555: #!/usr/bin/env bash
wenzelm@7793: #
wenzelm@7793: # $Id$
wenzelm@9788: # Author: Markus Wenzel, TU Muenchen
wenzelm@7793: #
wenzelm@7793: # DESCRIPTION: prepare theory session document
wenzelm@7793: 
wenzelm@7793: 
wenzelm@10511: PRG="$(basename "$0")"
wenzelm@7793: 
wenzelm@7793: function usage()
wenzelm@7793: {
wenzelm@7793:   echo
wenzelm@7793:   echo "Usage: $PRG [OPTIONS] [DIR]"
wenzelm@7793:   echo
wenzelm@7793:   echo "  Options are:"
wenzelm@8654:   echo "    -c           cleanup -- be aggressive in removing old stuff"
wenzelm@17049:   echo "    -n NAME      specify document name (default 'document')"
wenzelm@17049:   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
wenzelm@17049:   echo "    -t TAGS      specify tagged region markup"
wenzelm@7793:   echo
wenzelm@8211:   echo "  Prepare the theory session document in DIR (default 'document')"
wenzelm@7857:   echo "  producing the specified output format."
wenzelm@7793:   echo
wenzelm@7793:   exit 1
wenzelm@7793: }
wenzelm@7793: 
wenzelm@7793: function fail()
wenzelm@7793: {
wenzelm@7793:   echo "$1" >&2
wenzelm@7793:   exit 2
wenzelm@7793: }
wenzelm@7793: 
wenzelm@7793: 
wenzelm@7793: ## process command line
wenzelm@7793: 
wenzelm@7793: # options
wenzelm@7793: 
wenzelm@8211: CLEAN=""
wenzelm@17049: NAME="document"
wenzelm@7793: OUTFORMAT=dvi
wenzelm@17049: TAGS=""
wenzelm@7793: 
wenzelm@17049: while getopts "cn:o:t:" OPT
wenzelm@7793: do
wenzelm@7793:   case "$OPT" in
wenzelm@8211:     c)
wenzelm@8211:       CLEAN=true
wenzelm@8211:       ;;
wenzelm@17049:     n)
wenzelm@17049:       NAME="$OPTARG"
wenzelm@17049:       ;;
wenzelm@7793:     o)
wenzelm@7793:       OUTFORMAT="$OPTARG"
wenzelm@7793:       ;;
wenzelm@17049:     t)
wenzelm@17049:       TAGS="$OPTARG"
wenzelm@17049:       ;;
wenzelm@7793:     \?)
wenzelm@7793:       usage
wenzelm@7793:       ;;
wenzelm@7793:   esac
wenzelm@7793: done
wenzelm@7793: 
wenzelm@7793: shift $(($OPTIND - 1))
wenzelm@7793: 
wenzelm@7793: 
wenzelm@7793: # args
wenzelm@7793: 
wenzelm@8211: DIR="document"
wenzelm@9788: [ "$#" -ge 1 ] && { DIR="$1"; shift; }
wenzelm@7793: 
wenzelm@9788: [ "$#" -ne 0 ] && usage
wenzelm@7793: 
wenzelm@7793: 
wenzelm@7793: ## main
wenzelm@7793: 
wenzelm@7814: # check format
wenzelm@7814: 
wenzelm@7814: case "$OUTFORMAT" in
wenzelm@7814:   dvi | dvi.gz | ps | ps.gz | pdf)
wenzelm@7814:     ;;
wenzelm@7814:   *)
wenzelm@7814:     fail "Bad output format '$OUTFORMAT'"
wenzelm@7814:     ;;
wenzelm@7814: esac
wenzelm@7814: 
wenzelm@7814: 
wenzelm@17049: # tagged region markup
wenzelm@17049: 
wenzelm@17049: function prep_tags ()
wenzelm@17049: {
wenzelm@17049:   (
wenzelm@17049:     IFS=","
wenzelm@17049:     for TAG in $TAGS
wenzelm@17049:     do
wenzelm@17049:       case "$TAG" in
wenzelm@17049:         /*)
wenzelm@17049:   	  echo "\\isafoldtag{${TAG:1}}"
wenzelm@17049:           ;;
wenzelm@17049:         -*)
wenzelm@17049:   	  echo "\\isadroptag{${TAG:1}}"
wenzelm@17049:           ;;
wenzelm@17049:         +*)
wenzelm@17049:   	  echo "\\isakeeptag{${TAG:1}}"
wenzelm@17049:           ;;
wenzelm@17049:         *)
wenzelm@17049:   	  echo "\\isakeeptag{${TAG}}"
wenzelm@17049:           ;;
wenzelm@17049:       esac
wenzelm@17049:     done
wenzelm@17049:   ) > isabelletags.sty
wenzelm@17049: }
wenzelm@17049: 
wenzelm@17049: 
wenzelm@7814: # prepare document
wenzelm@7793: 
wenzelm@7814: function pre_latex ()
wenzelm@7814: {
wenzelm@7814:   local FMT="$1"
kleing@14367:   [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
wenzelm@28500:   "$ISABELLE_TOOL" latex -o sty && \
wenzelm@28500:   "$ISABELLE_TOOL" latex -o "$FMT" && \
wenzelm@28500:   { [ ! -f root.bib ] || "$ISABELLE_TOOL" latex -o bbl; } && \
wenzelm@28500:   { [ ! -f root.idx ] || "$ISABELLE_TOOL" latex -o idx; } && \
wenzelm@28500:   "$ISABELLE_TOOL" latex -o "$FMT"
wenzelm@7814: }
wenzelm@7814: 
wenzelm@8211: (
wenzelm@8211:   cd "$DIR" || fail "Bad directory '$DIR'"
wenzelm@8211: 
wenzelm@17049:   [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT"
wenzelm@17049: 
wenzelm@17049:   prep_tags
wenzelm@8654: 
wenzelm@8211:   if [ -f IsaMakefile ]; then
wenzelm@28500:     "$ISABELLE_TOOL" make "$OUTFORMAT"
wenzelm@9788:     RC="$?"
wenzelm@8211:   elif [ "$OUTFORMAT" = pdf ]; then
wenzelm@8211:     pre_latex pdf && \
wenzelm@28500:     "$ISABELLE_TOOL" latex -o pdf
wenzelm@9788:     RC="$?"
wenzelm@8211:   else
wenzelm@8211:     pre_latex dvi && \
wenzelm@28500:     "$ISABELLE_TOOL" latex -o "$OUTFORMAT"
wenzelm@9788:     RC="$?"
wenzelm@8211:   fi
wenzelm@8211: 
wenzelm@11581:   if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
wenzelm@17049:     cp -f "root.$OUTFORMAT" "../$NAME.$OUTFORMAT"
wenzelm@11581:   fi
wenzelm@8211: 
wenzelm@8217:   exit "$RC"
wenzelm@8211: )
wenzelm@9788: RC="$?"
wenzelm@7793: 
wenzelm@7793: 
wenzelm@7814: # install
wenzelm@7793: 
wenzelm@17049: [ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
wenzelm@8211: 
wenzelm@8211: #beware!
wenzelm@8211: [ -n "$CLEAN" ] && rm -rf "$DIR"
wenzelm@8211: 
wenzelm@8211: exit "$RC"