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