lib/Tools/document
author wenzelm
Sat Oct 09 23:16:31 1999 +0200 (1999-10-09)
changeset 7814 ef6d84f16592
parent 7793 e0676a932348
child 7857 a49a3978fe3a
permissions -rwxr-xr-x
check format;
support bibtex;
wenzelm@7793
     1
#!/bin/bash
wenzelm@7793
     2
#
wenzelm@7793
     3
# $Id$
wenzelm@7793
     4
#
wenzelm@7793
     5
# DESCRIPTION: prepare theory session document
wenzelm@7793
     6
wenzelm@7793
     7
wenzelm@7793
     8
PRG=$(basename $0)
wenzelm@7793
     9
wenzelm@7793
    10
function usage()
wenzelm@7793
    11
{
wenzelm@7793
    12
  echo
wenzelm@7793
    13
  echo "Usage: $PRG [OPTIONS] [DIR]"
wenzelm@7793
    14
  echo
wenzelm@7793
    15
  echo "  Options are:"
wenzelm@7793
    16
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
wenzelm@7793
    17
  echo
wenzelm@7793
    18
  echo
wenzelm@7793
    19
  echo "  Prepare the theory session document in DIR (default .)"
wenzelm@7793
    20
  echo "  producing the speficied output format."
wenzelm@7793
    21
  echo
wenzelm@7793
    22
  exit 1
wenzelm@7793
    23
}
wenzelm@7793
    24
wenzelm@7793
    25
function fail()
wenzelm@7793
    26
{
wenzelm@7793
    27
  echo "$1" >&2
wenzelm@7793
    28
  exit 2
wenzelm@7793
    29
}
wenzelm@7793
    30
wenzelm@7793
    31
wenzelm@7793
    32
## process command line
wenzelm@7793
    33
wenzelm@7793
    34
# options
wenzelm@7793
    35
wenzelm@7793
    36
OUTFORMAT=dvi
wenzelm@7793
    37
wenzelm@7793
    38
while getopts "o:" OPT
wenzelm@7793
    39
do
wenzelm@7793
    40
  case "$OPT" in
wenzelm@7793
    41
    o)
wenzelm@7793
    42
      OUTFORMAT="$OPTARG"
wenzelm@7793
    43
      ;;
wenzelm@7793
    44
    \?)
wenzelm@7793
    45
      usage
wenzelm@7793
    46
      ;;
wenzelm@7793
    47
  esac
wenzelm@7793
    48
done
wenzelm@7793
    49
wenzelm@7793
    50
shift $(($OPTIND - 1))
wenzelm@7793
    51
wenzelm@7793
    52
wenzelm@7793
    53
# args
wenzelm@7793
    54
wenzelm@7793
    55
DIR="."
wenzelm@7793
    56
[ $# -ge 1 ] && { DIR="$1"; shift; }
wenzelm@7793
    57
wenzelm@7793
    58
[ $# -ne 0 ] && usage
wenzelm@7793
    59
wenzelm@7793
    60
wenzelm@7793
    61
## main
wenzelm@7793
    62
wenzelm@7814
    63
# check format
wenzelm@7814
    64
wenzelm@7814
    65
case "$OUTFORMAT" in
wenzelm@7814
    66
  dvi | dvi.gz | ps | ps.gz | pdf)
wenzelm@7814
    67
    ;;
wenzelm@7814
    68
  *)
wenzelm@7814
    69
    fail "Bad output format '$OUTFORMAT'"
wenzelm@7814
    70
    ;;
wenzelm@7814
    71
esac
wenzelm@7814
    72
wenzelm@7814
    73
wenzelm@7814
    74
# prepare document
wenzelm@7793
    75
wenzelm@7793
    76
cd "$DIR" || fail "Bad directory '$DIR'"
wenzelm@7793
    77
wenzelm@7814
    78
function pre_latex ()
wenzelm@7814
    79
{
wenzelm@7814
    80
  local FMT="$1"
wenzelm@7814
    81
  if [ -f root.bib ]
wenzelm@7814
    82
  then
wenzelm@7814
    83
    $ISATOOL latex -o "$FMT" && \
wenzelm@7814
    84
    $ISATOOL latex -o bbl && \
wenzelm@7814
    85
    $ISATOOL latex -o "$FMT"
wenzelm@7814
    86
  else
wenzelm@7814
    87
    $ISATOOL latex -o "$FMT"
wenzelm@7814
    88
  fi
wenzelm@7814
    89
}
wenzelm@7814
    90
wenzelm@7793
    91
if [ -f IsaMakefile ]; then
wenzelm@7793
    92
  $ISATOOL make "$OUTFORMAT"
wenzelm@7793
    93
  RC=$?   #FIXME !??
wenzelm@7793
    94
elif [ "$OUTFORMAT" = pdf ]; then
wenzelm@7814
    95
  pre_latex pdf && \
wenzelm@7814
    96
  $ISATOOL latex -o pdf
wenzelm@7793
    97
  RC=$?
wenzelm@7793
    98
else
wenzelm@7814
    99
  pre_latex dvi && \
wenzelm@7814
   100
  $ISATOOL latex -o "$OUTFORMAT"
wenzelm@7793
   101
  RC=$?
wenzelm@7793
   102
fi
wenzelm@7793
   103
wenzelm@7793
   104
wenzelm@7814
   105
# install
wenzelm@7793
   106
wenzelm@7793
   107
[ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
wenzelm@7793
   108
cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"