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