lib/Tools/latex

prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;

#!/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), dvi, bbl, idx, sty, syms"
  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

function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
function copy_styles ()
{
  for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
  do
    TARGET="$DIR"/$(basename "$STYLEFILE")
    perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
  done
}

function extract_syms ()
{
  perl -n \
    -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
    "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
  perl -n \
    -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
    "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
}

case "$OUTFORMAT" in
  pdf)
    check_root && \
    run_pdflatex
    RC="$?"
    ;;
  dvi)
    check_root && \
    run_latex
    RC="$?"
    ;;
  bbl)
    check_root && \
    run_bibtex
    RC="$?"
    ;;
  idx)
    check_root && \
    run_makeindex
    RC="$?"
    ;;
  sty)
    copy_styles
    RC="$?"
    ;;
  syms)
    extract_syms
    RC="$?"
    ;;
  *)
    fail "Bad output format '$OUTFORMAT'"
    ;;
esac

exit "$RC"