lib/Tools/document
author wenzelm
Thu Sep 27 12:24:40 2001 +0200 (2001-09-27)
changeset 11581 d7bb261e3a3b
parent 10555 2323ec838401
child 11844 eb072fd9a45a
permissions -rwxr-xr-x
-v option;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@7793
     2
#
wenzelm@7793
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9788
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@7793
     6
#
wenzelm@7793
     7
# DESCRIPTION: prepare theory session document
wenzelm@7793
     8
wenzelm@7793
     9
wenzelm@10511
    10
PRG="$(basename "$0")"
wenzelm@7793
    11
wenzelm@7793
    12
function usage()
wenzelm@7793
    13
{
wenzelm@7793
    14
  echo
wenzelm@7793
    15
  echo "Usage: $PRG [OPTIONS] [DIR]"
wenzelm@7793
    16
  echo
wenzelm@7793
    17
  echo "  Options are:"
wenzelm@8654
    18
  echo "    -c           cleanup -- be aggressive in removing old stuff"
wenzelm@7866
    19
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
wenzelm@7866
    20
  echo "                 ps.gz, pdf"
wenzelm@11581
    21
  echo "    -v           be verbose"
wenzelm@7793
    22
  echo
wenzelm@8211
    23
  echo "  Prepare the theory session document in DIR (default 'document')"
wenzelm@7857
    24
  echo "  producing the specified output format."
wenzelm@7793
    25
  echo
wenzelm@7793
    26
  exit 1
wenzelm@7793
    27
}
wenzelm@7793
    28
wenzelm@7793
    29
function fail()
wenzelm@7793
    30
{
wenzelm@7793
    31
  echo "$1" >&2
wenzelm@7793
    32
  exit 2
wenzelm@7793
    33
}
wenzelm@7793
    34
wenzelm@7793
    35
wenzelm@7793
    36
## process command line
wenzelm@7793
    37
wenzelm@7793
    38
# options
wenzelm@7793
    39
wenzelm@8211
    40
CLEAN=""
wenzelm@7793
    41
OUTFORMAT=dvi
wenzelm@11581
    42
VERBOSE=""
wenzelm@7793
    43
wenzelm@11581
    44
while getopts "co:v" OPT
wenzelm@7793
    45
do
wenzelm@7793
    46
  case "$OPT" in
wenzelm@8211
    47
    c)
wenzelm@8211
    48
      CLEAN=true
wenzelm@8211
    49
      ;;
wenzelm@7793
    50
    o)
wenzelm@7793
    51
      OUTFORMAT="$OPTARG"
wenzelm@7793
    52
      ;;
wenzelm@11581
    53
    v)
wenzelm@11581
    54
      VERBOSE=true
wenzelm@11581
    55
      ;;
wenzelm@7793
    56
    \?)
wenzelm@7793
    57
      usage
wenzelm@7793
    58
      ;;
wenzelm@7793
    59
  esac
wenzelm@7793
    60
done
wenzelm@7793
    61
wenzelm@7793
    62
shift $(($OPTIND - 1))
wenzelm@7793
    63
wenzelm@7793
    64
wenzelm@7793
    65
# args
wenzelm@7793
    66
wenzelm@8211
    67
DIR="document"
wenzelm@9788
    68
[ "$#" -ge 1 ] && { DIR="$1"; shift; }
wenzelm@7793
    69
wenzelm@9788
    70
[ "$#" -ne 0 ] && usage
wenzelm@7793
    71
wenzelm@7793
    72
wenzelm@7793
    73
## main
wenzelm@7793
    74
wenzelm@7814
    75
# check format
wenzelm@7814
    76
wenzelm@7814
    77
case "$OUTFORMAT" in
wenzelm@7814
    78
  dvi | dvi.gz | ps | ps.gz | pdf)
wenzelm@7814
    79
    ;;
wenzelm@7814
    80
  *)
wenzelm@7814
    81
    fail "Bad output format '$OUTFORMAT'"
wenzelm@7814
    82
    ;;
wenzelm@7814
    83
esac
wenzelm@7814
    84
wenzelm@7814
    85
wenzelm@7814
    86
# prepare document
wenzelm@7793
    87
wenzelm@7814
    88
function pre_latex ()
wenzelm@7814
    89
{
wenzelm@7814
    90
  local FMT="$1"
wenzelm@8654
    91
  [ -n "$CLEAN" ] && rm -f *.aux *.out
wenzelm@7814
    92
  if [ -f root.bib ]
wenzelm@7814
    93
  then
wenzelm@9788
    94
    "$ISATOOL" latex -o "$FMT" && \
wenzelm@9788
    95
    "$ISATOOL" latex -o bbl && \
wenzelm@9788
    96
    "$ISATOOL" latex -o "$FMT"
wenzelm@7814
    97
  else
wenzelm@9788
    98
    "$ISATOOL" latex -o "$FMT"
wenzelm@7814
    99
  fi
wenzelm@7814
   100
}
wenzelm@7814
   101
wenzelm@8211
   102
(
wenzelm@8211
   103
  cd "$DIR" || fail "Bad directory '$DIR'"
wenzelm@8211
   104
wenzelm@8654
   105
  [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"
wenzelm@8654
   106
wenzelm@8211
   107
  if [ -f IsaMakefile ]; then
wenzelm@9788
   108
    "$ISATOOL" make "$OUTFORMAT"
wenzelm@9788
   109
    RC="$?"
wenzelm@8211
   110
  elif [ "$OUTFORMAT" = pdf ]; then
wenzelm@8211
   111
    pre_latex pdf && \
wenzelm@9788
   112
    "$ISATOOL" latex -o pdf && \
wenzelm@8211
   113
    { if [ -n "$ISABELLE_THUMBPDF" ]; then
wenzelm@9788
   114
        "$ISATOOL" latex -o png && \
wenzelm@9788
   115
        "$ISATOOL" latex -o pdf
wenzelm@8211
   116
      fi; }
wenzelm@9788
   117
    RC="$?"
wenzelm@8211
   118
  else
wenzelm@8211
   119
    pre_latex dvi && \
wenzelm@9788
   120
    "$ISATOOL" latex -o "$OUTFORMAT"
wenzelm@9788
   121
    RC="$?"
wenzelm@8211
   122
  fi
wenzelm@8211
   123
wenzelm@11581
   124
  if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
wenzelm@11581
   125
    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" && \
wenzelm@11581
   126
    [ -n "$VERBOSE" ] && echo "$(cd ..; echo "Prepared $PWD/document.$OUTFORMAT")" >&2
wenzelm@11581
   127
  fi
wenzelm@8211
   128
wenzelm@8217
   129
  exit "$RC"
wenzelm@8211
   130
)
wenzelm@9788
   131
RC="$?"
wenzelm@7793
   132
wenzelm@7793
   133
wenzelm@7814
   134
# install
wenzelm@7793
   135
wenzelm@8211
   136
[ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"
wenzelm@8211
   137
wenzelm@8211
   138
#beware!
wenzelm@8211
   139
[ -n "$CLEAN" ] && rm -rf "$DIR"
wenzelm@8211
   140
wenzelm@8211
   141
exit "$RC"