lib/Tools/document

1. changed configuration variables for linear programming (Cplex_tools):
LP_SOLVER is either CPLEX or GLPK
CPLEX_PATH is the path to the cplex binary
GLPK_PATH is the path to the glpk binary
The change makes it possible to switch between glpk and cplex at runtime.
2. moved conflicting list theories out of Library.thy into ROOT.ML

#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: prepare theory session document


PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] [DIR]"
  echo
  echo "  Options are:"
  echo "    -c           cleanup -- be aggressive in removing old stuff"
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
  echo "                 ps.gz, pdf"
  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=""
OUTFORMAT=dvi

while getopts "co:" OPT
do
  case "$OPT" in
    c)
      CLEAN=true
      ;;
    o)
      OUTFORMAT="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

DIR="document"
[ "$#" -ge 1 ] && { DIR="$1"; shift; }

[ "$#" -ne 0 ] && usage


## main

# check format

case "$OUTFORMAT" in
  dvi | dvi.gz | ps | ps.gz | pdf)
    ;;
  *)
    fail "Bad output format '$OUTFORMAT'"
    ;;
esac


# prepare document

function pre_latex ()
{
  local FMT="$1"
  [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
  "$ISATOOL" latex -o sty && \
  "$ISATOOL" latex -o "$FMT" && \
  { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \
  { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \
  "$ISATOOL" latex -o "$FMT"
}

(
  cd "$DIR" || fail "Bad directory '$DIR'"

  [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"

  if [ -f IsaMakefile ]; then
    "$ISATOOL" make "$OUTFORMAT"
    RC="$?"
  elif [ "$OUTFORMAT" = pdf ]; then
    pre_latex pdf && \
    "$ISATOOL" latex -o pdf && \
    { if [ -n "$ISABELLE_THUMBPDF" ]; then
        "$ISATOOL" latex -o png && \
        "$ISATOOL" latex -o pdf
      fi; }
    RC="$?"
  else
    pre_latex dvi && \
    "$ISATOOL" latex -o "$OUTFORMAT"
    RC="$?"
  fi

  if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
  fi

  exit "$RC"
)
RC="$?"


# install

[ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"

#beware!
[ -n "$CLEAN" ] && rm -rf "$DIR"

exit "$RC"