lib/Tools/document
author wenzelm
Tue Aug 16 13:42:15 2005 +0200 (2005-08-16)
changeset 17049 ee573216713a
parent 14981 e73f8140af78
child 26908 25fb7241f32e
permissions -rwxr-xr-x
added option -n NAME and -t TAGS;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@7793
     2
#
wenzelm@7793
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@7793
     5
#
wenzelm@7793
     6
# DESCRIPTION: prepare theory session document
wenzelm@7793
     7
wenzelm@7793
     8
wenzelm@10511
     9
PRG="$(basename "$0")"
wenzelm@7793
    10
wenzelm@7793
    11
function usage()
wenzelm@7793
    12
{
wenzelm@7793
    13
  echo
wenzelm@7793
    14
  echo "Usage: $PRG [OPTIONS] [DIR]"
wenzelm@7793
    15
  echo
wenzelm@7793
    16
  echo "  Options are:"
wenzelm@8654
    17
  echo "    -c           cleanup -- be aggressive in removing old stuff"
wenzelm@17049
    18
  echo "    -n NAME      specify document name (default 'document')"
wenzelm@17049
    19
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
wenzelm@17049
    20
  echo "    -t TAGS      specify tagged region markup"
wenzelm@7793
    21
  echo
wenzelm@8211
    22
  echo "  Prepare the theory session document in DIR (default 'document')"
wenzelm@7857
    23
  echo "  producing the specified output format."
wenzelm@7793
    24
  echo
wenzelm@7793
    25
  exit 1
wenzelm@7793
    26
}
wenzelm@7793
    27
wenzelm@7793
    28
function fail()
wenzelm@7793
    29
{
wenzelm@7793
    30
  echo "$1" >&2
wenzelm@7793
    31
  exit 2
wenzelm@7793
    32
}
wenzelm@7793
    33
wenzelm@7793
    34
wenzelm@7793
    35
## process command line
wenzelm@7793
    36
wenzelm@7793
    37
# options
wenzelm@7793
    38
wenzelm@8211
    39
CLEAN=""
wenzelm@17049
    40
NAME="document"
wenzelm@7793
    41
OUTFORMAT=dvi
wenzelm@17049
    42
TAGS=""
wenzelm@7793
    43
wenzelm@17049
    44
while getopts "cn:o:t:" OPT
wenzelm@7793
    45
do
wenzelm@7793
    46
  case "$OPT" in
wenzelm@8211
    47
    c)
wenzelm@8211
    48
      CLEAN=true
wenzelm@8211
    49
      ;;
wenzelm@17049
    50
    n)
wenzelm@17049
    51
      NAME="$OPTARG"
wenzelm@17049
    52
      ;;
wenzelm@7793
    53
    o)
wenzelm@7793
    54
      OUTFORMAT="$OPTARG"
wenzelm@7793
    55
      ;;
wenzelm@17049
    56
    t)
wenzelm@17049
    57
      TAGS="$OPTARG"
wenzelm@17049
    58
      ;;
wenzelm@7793
    59
    \?)
wenzelm@7793
    60
      usage
wenzelm@7793
    61
      ;;
wenzelm@7793
    62
  esac
wenzelm@7793
    63
done
wenzelm@7793
    64
wenzelm@7793
    65
shift $(($OPTIND - 1))
wenzelm@7793
    66
wenzelm@7793
    67
wenzelm@7793
    68
# args
wenzelm@7793
    69
wenzelm@8211
    70
DIR="document"
wenzelm@9788
    71
[ "$#" -ge 1 ] && { DIR="$1"; shift; }
wenzelm@7793
    72
wenzelm@9788
    73
[ "$#" -ne 0 ] && usage
wenzelm@7793
    74
wenzelm@7793
    75
wenzelm@7793
    76
## main
wenzelm@7793
    77
wenzelm@7814
    78
# check format
wenzelm@7814
    79
wenzelm@7814
    80
case "$OUTFORMAT" in
wenzelm@7814
    81
  dvi | dvi.gz | ps | ps.gz | pdf)
wenzelm@7814
    82
    ;;
wenzelm@7814
    83
  *)
wenzelm@7814
    84
    fail "Bad output format '$OUTFORMAT'"
wenzelm@7814
    85
    ;;
wenzelm@7814
    86
esac
wenzelm@7814
    87
wenzelm@7814
    88
wenzelm@17049
    89
# tagged region markup
wenzelm@17049
    90
wenzelm@17049
    91
function prep_tags ()
wenzelm@17049
    92
{
wenzelm@17049
    93
  (
wenzelm@17049
    94
    IFS=","
wenzelm@17049
    95
    for TAG in $TAGS
wenzelm@17049
    96
    do
wenzelm@17049
    97
      case "$TAG" in
wenzelm@17049
    98
        /*)
wenzelm@17049
    99
  	  echo "\\isafoldtag{${TAG:1}}"
wenzelm@17049
   100
          ;;
wenzelm@17049
   101
        -*)
wenzelm@17049
   102
  	  echo "\\isadroptag{${TAG:1}}"
wenzelm@17049
   103
          ;;
wenzelm@17049
   104
        +*)
wenzelm@17049
   105
  	  echo "\\isakeeptag{${TAG:1}}"
wenzelm@17049
   106
          ;;
wenzelm@17049
   107
        *)
wenzelm@17049
   108
  	  echo "\\isakeeptag{${TAG}}"
wenzelm@17049
   109
          ;;
wenzelm@17049
   110
      esac
wenzelm@17049
   111
    done
wenzelm@17049
   112
  ) > isabelletags.sty
wenzelm@17049
   113
}
wenzelm@17049
   114
wenzelm@17049
   115
wenzelm@7814
   116
# prepare document
wenzelm@7793
   117
wenzelm@7814
   118
function pre_latex ()
wenzelm@7814
   119
{
wenzelm@7814
   120
  local FMT="$1"
kleing@14367
   121
  [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
wenzelm@12688
   122
  "$ISATOOL" latex -o sty && \
wenzelm@11948
   123
  "$ISATOOL" latex -o "$FMT" && \
wenzelm@11948
   124
  { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \
wenzelm@14936
   125
  { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \
wenzelm@14936
   126
  "$ISATOOL" latex -o "$FMT"
wenzelm@7814
   127
}
wenzelm@7814
   128
wenzelm@8211
   129
(
wenzelm@8211
   130
  cd "$DIR" || fail "Bad directory '$DIR'"
wenzelm@8211
   131
wenzelm@17049
   132
  [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT"
wenzelm@17049
   133
wenzelm@17049
   134
  prep_tags
wenzelm@8654
   135
wenzelm@8211
   136
  if [ -f IsaMakefile ]; then
wenzelm@9788
   137
    "$ISATOOL" make "$OUTFORMAT"
wenzelm@9788
   138
    RC="$?"
wenzelm@8211
   139
  elif [ "$OUTFORMAT" = pdf ]; then
wenzelm@8211
   140
    pre_latex pdf && \
wenzelm@9788
   141
    "$ISATOOL" latex -o pdf && \
wenzelm@8211
   142
    { if [ -n "$ISABELLE_THUMBPDF" ]; then
wenzelm@9788
   143
        "$ISATOOL" latex -o png && \
wenzelm@9788
   144
        "$ISATOOL" latex -o pdf
wenzelm@8211
   145
      fi; }
wenzelm@9788
   146
    RC="$?"
wenzelm@8211
   147
  else
wenzelm@8211
   148
    pre_latex dvi && \
wenzelm@9788
   149
    "$ISATOOL" latex -o "$OUTFORMAT"
wenzelm@9788
   150
    RC="$?"
wenzelm@8211
   151
  fi
wenzelm@8211
   152
wenzelm@11581
   153
  if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
wenzelm@17049
   154
    cp -f "root.$OUTFORMAT" "../$NAME.$OUTFORMAT"
wenzelm@11581
   155
  fi
wenzelm@8211
   156
wenzelm@8217
   157
  exit "$RC"
wenzelm@8211
   158
)
wenzelm@9788
   159
RC="$?"
wenzelm@7793
   160
wenzelm@7793
   161
wenzelm@7814
   162
# install
wenzelm@7793
   163
wenzelm@17049
   164
[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
wenzelm@8211
   165
wenzelm@8211
   166
#beware!
wenzelm@8211
   167
[ -n "$CLEAN" ] && rm -rf "$DIR"
wenzelm@8211
   168
wenzelm@8211
   169
exit "$RC"