lib/Tools/document
author wenzelm
Tue Feb 08 20:14:58 2000 +0100 (2000-02-08)
changeset 8211 714f164f0385
parent 8171 f89329974d2d
child 8212 419157483fc9
permissions -rwxr-xr-x
rename -p to -P;
fixed target name: LOGIC-NAME;
wenzelm@8211
     1
#!/bin/bash -x
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@8211
    16
  echo "    -c           clean -- remove DIR after succesful run"
wenzelm@7866
    17
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
wenzelm@7866
    18
  echo "                 ps.gz, pdf"
wenzelm@7793
    19
  echo
wenzelm@8211
    20
  echo "  Prepare the theory session document in DIR (default 'document')"
wenzelm@7857
    21
  echo "  producing the specified output format."
wenzelm@7793
    22
  echo
wenzelm@7793
    23
  exit 1
wenzelm@7793
    24
}
wenzelm@7793
    25
wenzelm@7793
    26
function fail()
wenzelm@7793
    27
{
wenzelm@7793
    28
  echo "$1" >&2
wenzelm@7793
    29
  exit 2
wenzelm@7793
    30
}
wenzelm@7793
    31
wenzelm@7793
    32
wenzelm@7793
    33
## process command line
wenzelm@7793
    34
wenzelm@7793
    35
# options
wenzelm@7793
    36
wenzelm@8211
    37
CLEAN=""
wenzelm@7793
    38
OUTFORMAT=dvi
wenzelm@7793
    39
wenzelm@8211
    40
while getopts "co:" OPT
wenzelm@7793
    41
do
wenzelm@7793
    42
  case "$OPT" in
wenzelm@8211
    43
    c)
wenzelm@8211
    44
      CLEAN=true
wenzelm@8211
    45
      ;;
wenzelm@7793
    46
    o)
wenzelm@7793
    47
      OUTFORMAT="$OPTARG"
wenzelm@7793
    48
      ;;
wenzelm@7793
    49
    \?)
wenzelm@7793
    50
      usage
wenzelm@7793
    51
      ;;
wenzelm@7793
    52
  esac
wenzelm@7793
    53
done
wenzelm@7793
    54
wenzelm@7793
    55
shift $(($OPTIND - 1))
wenzelm@7793
    56
wenzelm@7793
    57
wenzelm@7793
    58
# args
wenzelm@7793
    59
wenzelm@8211
    60
DIR="document"
wenzelm@7793
    61
[ $# -ge 1 ] && { DIR="$1"; shift; }
wenzelm@7793
    62
wenzelm@7793
    63
[ $# -ne 0 ] && usage
wenzelm@7793
    64
wenzelm@7793
    65
wenzelm@7793
    66
## main
wenzelm@7793
    67
wenzelm@7814
    68
# check format
wenzelm@7814
    69
wenzelm@7814
    70
case "$OUTFORMAT" in
wenzelm@7814
    71
  dvi | dvi.gz | ps | ps.gz | pdf)
wenzelm@7814
    72
    ;;
wenzelm@7814
    73
  *)
wenzelm@7814
    74
    fail "Bad output format '$OUTFORMAT'"
wenzelm@7814
    75
    ;;
wenzelm@7814
    76
esac
wenzelm@7814
    77
wenzelm@7814
    78
wenzelm@7814
    79
# prepare document
wenzelm@7793
    80
wenzelm@7814
    81
function pre_latex ()
wenzelm@7814
    82
{
wenzelm@7814
    83
  local FMT="$1"
wenzelm@8171
    84
  rm -f *.aux
wenzelm@7814
    85
  if [ -f root.bib ]
wenzelm@7814
    86
  then
wenzelm@7814
    87
    $ISATOOL latex -o "$FMT" && \
wenzelm@7814
    88
    $ISATOOL latex -o bbl && \
wenzelm@7814
    89
    $ISATOOL latex -o "$FMT"
wenzelm@7814
    90
  else
wenzelm@7814
    91
    $ISATOOL latex -o "$FMT"
wenzelm@7814
    92
  fi
wenzelm@7814
    93
}
wenzelm@7814
    94
wenzelm@8211
    95
(
wenzelm@8211
    96
  cd "$DIR" || fail "Bad directory '$DIR'"
wenzelm@8211
    97
wenzelm@8211
    98
  if [ -f IsaMakefile ]; then
wenzelm@8211
    99
    $ISATOOL make "$OUTFORMAT"
wenzelm@8211
   100
    RC=$?
wenzelm@8211
   101
  elif [ "$OUTFORMAT" = pdf ]; then
wenzelm@8211
   102
    pre_latex pdf && \
wenzelm@8211
   103
    $ISATOOL latex -o pdf && \
wenzelm@8211
   104
    { if [ -n "$ISABELLE_THUMBPDF" ]; then
wenzelm@8211
   105
        $ISATOOL latex -o png && \
wenzelm@8211
   106
        $ISATOOL latex -o pdf
wenzelm@8211
   107
      fi; }
wenzelm@8211
   108
    RC=$?
wenzelm@8211
   109
  else
wenzelm@8211
   110
    pre_latex dvi && \
wenzelm@8211
   111
    $ISATOOL latex -o "$OUTFORMAT"
wenzelm@8211
   112
    RC=$?
wenzelm@8211
   113
  fi
wenzelm@8211
   114
wenzelm@8211
   115
  [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
wenzelm@8211
   116
    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
wenzelm@8211
   117
wenzelm@8211
   118
  exit $RC
wenzelm@8211
   119
)
wenzelm@8211
   120
RC=$?
wenzelm@7793
   121
wenzelm@7793
   122
wenzelm@7814
   123
# install
wenzelm@7793
   124
wenzelm@8211
   125
[ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"
wenzelm@8211
   126
wenzelm@8211
   127
#beware!
wenzelm@8211
   128
[ -n "$CLEAN" ] && rm -rf "$DIR"
wenzelm@8211
   129
wenzelm@8211
   130
exit "$RC"