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