lib/Tools/document
author paulson
Tue, 10 Feb 2004 12:02:11 +0100
changeset 14378 69c4d5997669
parent 14367 0b1447d37161
child 14936 a13d5118f628
permissions -rwxr-xr-x
generic of_nat and of_int functions, and generalization of iszero and neg
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10511
diff changeset
     1
#!/usr/bin/env 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
10511
wenzelm
parents: 9788
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
11844
eb072fd9a45a removed -v option (handled by isabelle process);
wenzelm
parents: 11581
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"
14367
0b1447d37161 remove more files (index, log files) for -c option
kleing
parents: 14344
diff changeset
    86
  [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
12688
4ad13c2f7196 isatool latex -o sty;
wenzelm
parents: 11948
diff changeset
    87
  "$ISATOOL" latex -o sty && \
11948
9c812b21b2e8 need at least 3 latex runs to get toc right!
wenzelm
parents: 11844
diff changeset
    88
  "$ISATOOL" latex -o "$FMT" && \
9c812b21b2e8 need at least 3 latex runs to get toc right!
wenzelm
parents: 11844
diff changeset
    89
  { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \
14344
0f0a2148a099 run makeindex if necessary
kleing
parents: 12688
diff changeset
    90
  { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \  
0f0a2148a099 run makeindex if necessary
kleing
parents: 12688
diff changeset
    91
    "$ISATOOL" latex -o "$FMT"
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    92
}
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    93
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    94
(
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    95
  cd "$DIR" || fail "Bad directory '$DIR'"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    96
8654
38ce936acb99 tuned -c option;
wenzelm
parents: 8269
diff changeset
    97
  [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"
38ce936acb99 tuned -c option;
wenzelm
parents: 8269
diff changeset
    98
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    99
  if [ -f IsaMakefile ]; then
9788
wenzelm
parents: 8654
diff changeset
   100
    "$ISATOOL" make "$OUTFORMAT"
wenzelm
parents: 8654
diff changeset
   101
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   102
  elif [ "$OUTFORMAT" = pdf ]; then
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   103
    pre_latex pdf && \
9788
wenzelm
parents: 8654
diff changeset
   104
    "$ISATOOL" latex -o pdf && \
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   105
    { if [ -n "$ISABELLE_THUMBPDF" ]; then
9788
wenzelm
parents: 8654
diff changeset
   106
        "$ISATOOL" latex -o png && \
wenzelm
parents: 8654
diff changeset
   107
        "$ISATOOL" latex -o pdf
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   108
      fi; }
9788
wenzelm
parents: 8654
diff changeset
   109
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   110
  else
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   111
    pre_latex dvi && \
9788
wenzelm
parents: 8654
diff changeset
   112
    "$ISATOOL" latex -o "$OUTFORMAT"
wenzelm
parents: 8654
diff changeset
   113
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   114
  fi
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   115
11581
d7bb261e3a3b -v option;
wenzelm
parents: 10555
diff changeset
   116
  if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
11844
eb072fd9a45a removed -v option (handled by isabelle process);
wenzelm
parents: 11581
diff changeset
   117
    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
11581
d7bb261e3a3b -v option;
wenzelm
parents: 10555
diff changeset
   118
  fi
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   119
8217
dc3b8cdbb816 option -c;
wenzelm
parents: 8212
diff changeset
   120
  exit "$RC"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   121
)
9788
wenzelm
parents: 8654
diff changeset
   122
RC="$?"
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   123
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   124
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   125
# install
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   126
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   127
[ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   128
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   129
#beware!
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   130
[ -n "$CLEAN" ] && rm -rf "$DIR"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   131
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   132
exit "$RC"