lib/Tools/document
author wenzelm
Wed, 01 Feb 2006 22:20:40 +0100
changeset 18888 3b643f81b378
parent 17049 ee573216713a
child 26908 25fb7241f32e
permissions -rwxr-xr-x
updated;
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
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
     5
#
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
     6
# DESCRIPTION: prepare theory session document
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
     7
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
     8
10511
wenzelm
parents: 9788
diff changeset
     9
PRG="$(basename "$0")"
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    10
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    11
function usage()
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    12
{
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    13
  echo
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    14
  echo "Usage: $PRG [OPTIONS] [DIR]"
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    15
  echo
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    16
  echo "  Options are:"
8654
38ce936acb99 tuned -c option;
wenzelm
parents: 8269
diff changeset
    17
  echo "    -c           cleanup -- be aggressive in removing old stuff"
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    18
  echo "    -n NAME      specify document name (default 'document')"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    19
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    20
  echo "    -t TAGS      specify tagged region markup"
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=""
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    40
NAME="document"
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    41
OUTFORMAT=dvi
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    42
TAGS=""
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    43
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    44
while getopts "cn:o:t:" OPT
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    45
do
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    46
  case "$OPT" in
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    47
    c)
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    48
      CLEAN=true
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    49
      ;;
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    50
    n)
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    51
      NAME="$OPTARG"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    52
      ;;
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    53
    o)
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    54
      OUTFORMAT="$OPTARG"
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    55
      ;;
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    56
    t)
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    57
      TAGS="$OPTARG"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    58
      ;;
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    59
    \?)
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    60
      usage
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    61
      ;;
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    62
  esac
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    63
done
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    64
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    65
shift $(($OPTIND - 1))
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
# args
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    69
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    70
DIR="document"
9788
wenzelm
parents: 8654
diff changeset
    71
[ "$#" -ge 1 ] && { DIR="$1"; shift; }
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    72
9788
wenzelm
parents: 8654
diff changeset
    73
[ "$#" -ne 0 ] && usage
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    74
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    75
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    76
## main
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    77
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    78
# check format
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    79
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    80
case "$OUTFORMAT" in
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    81
  dvi | dvi.gz | ps | ps.gz | pdf)
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    82
    ;;
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    83
  *)
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    84
    fail "Bad output format '$OUTFORMAT'"
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    85
    ;;
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    86
esac
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    87
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    88
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    89
# tagged region markup
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    90
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    91
function prep_tags ()
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    92
{
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    93
  (
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    94
    IFS=","
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    95
    for TAG in $TAGS
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    96
    do
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    97
      case "$TAG" in
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    98
        /*)
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    99
  	  echo "\\isafoldtag{${TAG:1}}"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   100
          ;;
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   101
        -*)
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   102
  	  echo "\\isadroptag{${TAG:1}}"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   103
          ;;
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   104
        +*)
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   105
  	  echo "\\isakeeptag{${TAG:1}}"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   106
          ;;
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   107
        *)
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   108
  	  echo "\\isakeeptag{${TAG}}"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   109
          ;;
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   110
      esac
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   111
    done
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   112
  ) > isabelletags.sty
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   113
}
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   114
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   115
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   116
# prepare document
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   117
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   118
function pre_latex ()
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   119
{
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   120
  local FMT="$1"
14367
0b1447d37161 remove more files (index, log files) for -c option
kleing
parents: 14344
diff changeset
   121
  [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
12688
4ad13c2f7196 isatool latex -o sty;
wenzelm
parents: 11948
diff changeset
   122
  "$ISATOOL" latex -o sty && \
11948
9c812b21b2e8 need at least 3 latex runs to get toc right!
wenzelm
parents: 11844
diff changeset
   123
  "$ISATOOL" latex -o "$FMT" && \
9c812b21b2e8 need at least 3 latex runs to get toc right!
wenzelm
parents: 11844
diff changeset
   124
  { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \
14936
wenzelm
parents: 14367
diff changeset
   125
  { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \
wenzelm
parents: 14367
diff changeset
   126
  "$ISATOOL" latex -o "$FMT"
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   127
}
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   128
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   129
(
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   130
  cd "$DIR" || fail "Bad directory '$DIR'"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   131
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   132
  [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   133
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   134
  prep_tags
8654
38ce936acb99 tuned -c option;
wenzelm
parents: 8269
diff changeset
   135
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   136
  if [ -f IsaMakefile ]; then
9788
wenzelm
parents: 8654
diff changeset
   137
    "$ISATOOL" make "$OUTFORMAT"
wenzelm
parents: 8654
diff changeset
   138
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   139
  elif [ "$OUTFORMAT" = pdf ]; then
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   140
    pre_latex pdf && \
9788
wenzelm
parents: 8654
diff changeset
   141
    "$ISATOOL" latex -o pdf && \
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   142
    { if [ -n "$ISABELLE_THUMBPDF" ]; then
9788
wenzelm
parents: 8654
diff changeset
   143
        "$ISATOOL" latex -o png && \
wenzelm
parents: 8654
diff changeset
   144
        "$ISATOOL" latex -o pdf
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   145
      fi; }
9788
wenzelm
parents: 8654
diff changeset
   146
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   147
  else
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   148
    pre_latex dvi && \
9788
wenzelm
parents: 8654
diff changeset
   149
    "$ISATOOL" latex -o "$OUTFORMAT"
wenzelm
parents: 8654
diff changeset
   150
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   151
  fi
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   152
11581
d7bb261e3a3b -v option;
wenzelm
parents: 10555
diff changeset
   153
  if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   154
    cp -f "root.$OUTFORMAT" "../$NAME.$OUTFORMAT"
11581
d7bb261e3a3b -v option;
wenzelm
parents: 10555
diff changeset
   155
  fi
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   156
8217
dc3b8cdbb816 option -c;
wenzelm
parents: 8212
diff changeset
   157
  exit "$RC"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   158
)
9788
wenzelm
parents: 8654
diff changeset
   159
RC="$?"
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   160
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   161
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   162
# install
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   163
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   164
[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   165
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   166
#beware!
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   167
[ -n "$CLEAN" ] && rm -rf "$DIR"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   168
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   169
exit "$RC"