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