lib/Tools/document
author paulson
Tue, 02 Feb 2010 09:48:20 +0000
changeset 35503 7bba12c3b7b6
parent 32390 468eff174a77
child 48616 be8002ee43d8
permissions -rwxr-xr-x
Correction of a tiny error
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
#
9788
wenzelm
parents: 8654
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
7793
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
10511
wenzelm
parents: 9788
diff changeset
     8
PRG="$(basename "$0")"
7793
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
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 28500
diff changeset
    13
  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    14
  echo
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    15
  echo "  Options are:"
8654
38ce936acb99 tuned -c option;
wenzelm
parents: 8269
diff changeset
    16
  echo "    -c           cleanup -- be aggressive in removing old stuff"
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    17
  echo "    -n NAME      specify document name (default 'document')"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    18
  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
    19
  echo "    -t TAGS      specify tagged region markup"
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    20
  echo
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    21
  echo "  Prepare the theory session document in DIR (default 'document')"
7857
a49a3978fe3a tuned usage;
wenzelm
parents: 7814
diff changeset
    22
  echo "  producing the specified output format."
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    23
  echo
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    24
  exit 1
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    25
}
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    26
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    27
function fail()
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    28
{
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    29
  echo "$1" >&2
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    30
  exit 2
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
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    34
## process command line
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    35
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    36
# options
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    37
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    38
CLEAN=""
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    39
NAME="document"
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    40
OUTFORMAT=dvi
32322
45cb4a86eca2 change IFS only locally -- thanks to bash arrays;
wenzelm
parents: 29143
diff changeset
    41
declare -a TAGS=()
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    42
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    43
while getopts "cn:o:t:" OPT
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    44
do
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    45
  case "$OPT" in
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    46
    c)
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    47
      CLEAN=true
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    48
      ;;
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    49
    n)
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    50
      NAME="$OPTARG"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    51
      ;;
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    52
    o)
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    53
      OUTFORMAT="$OPTARG"
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    54
      ;;
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    55
    t)
32390
468eff174a77 function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents: 32322
diff changeset
    56
      splitarray "," "$OPTARG"; TAGS=("${SPLITARRAY[@]}")
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    57
      ;;
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    58
    \?)
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    59
      usage
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    60
      ;;
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    61
  esac
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    62
done
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    63
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    64
shift $(($OPTIND - 1))
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    65
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    66
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    67
# args
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    68
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
    69
DIR="document"
9788
wenzelm
parents: 8654
diff changeset
    70
[ "$#" -ge 1 ] && { DIR="$1"; shift; }
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    71
9788
wenzelm
parents: 8654
diff changeset
    72
[ "$#" -ne 0 ] && usage
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    73
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    74
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    75
## main
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
    76
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    77
# check format
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    78
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    79
case "$OUTFORMAT" in
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    80
  dvi | dvi.gz | ps | ps.gz | pdf)
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    81
    ;;
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    82
  *)
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    83
    fail "Bad output format '$OUTFORMAT'"
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    84
    ;;
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    85
esac
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    86
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
    87
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    88
# tagged region markup
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    89
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    90
function prep_tags ()
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    91
{
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    92
  (
32322
45cb4a86eca2 change IFS only locally -- thanks to bash arrays;
wenzelm
parents: 29143
diff changeset
    93
    for TAG in "${TAGS[@]}"
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    94
    do
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    95
      case "$TAG" in
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    96
        /*)
32322
45cb4a86eca2 change IFS only locally -- thanks to bash arrays;
wenzelm
parents: 29143
diff changeset
    97
          echo "\\isafoldtag{${TAG:1}}"
17049
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
        -*)
32322
45cb4a86eca2 change IFS only locally -- thanks to bash arrays;
wenzelm
parents: 29143
diff changeset
   100
          echo "\\isadroptag{${TAG:1}}"
17049
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
        +*)
32322
45cb4a86eca2 change IFS only locally -- thanks to bash arrays;
wenzelm
parents: 29143
diff changeset
   103
          echo "\\isakeeptag{${TAG:1}}"
17049
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
        *)
32322
45cb4a86eca2 change IFS only locally -- thanks to bash arrays;
wenzelm
parents: 29143
diff changeset
   106
          echo "\\isakeeptag{${TAG}}"
17049
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
      esac
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   109
    done
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   110
  ) > isabelletags.sty
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   111
}
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   112
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   113
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   114
# prepare document
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   115
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   116
function pre_latex ()
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   117
{
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   118
  local FMT="$1"
14367
0b1447d37161 remove more files (index, log files) for -c option
kleing
parents: 14344
diff changeset
   119
  [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26979
diff changeset
   120
  "$ISABELLE_TOOL" latex -o sty && \
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26979
diff changeset
   121
  "$ISABELLE_TOOL" latex -o "$FMT" && \
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26979
diff changeset
   122
  { [ ! -f root.bib ] || "$ISABELLE_TOOL" latex -o bbl; } && \
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26979
diff changeset
   123
  { [ ! -f root.idx ] || "$ISABELLE_TOOL" latex -o idx; } && \
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26979
diff changeset
   124
  "$ISABELLE_TOOL" latex -o "$FMT"
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   125
}
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   126
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   127
(
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   128
  cd "$DIR" || fail "Bad directory '$DIR'"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   129
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   130
  [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   131
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   132
  prep_tags
8654
38ce936acb99 tuned -c option;
wenzelm
parents: 8269
diff changeset
   133
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   134
  if [ -f IsaMakefile ]; then
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26979
diff changeset
   135
    "$ISABELLE_TOOL" make "$OUTFORMAT"
9788
wenzelm
parents: 8654
diff changeset
   136
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   137
  elif [ "$OUTFORMAT" = pdf ]; then
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   138
    pre_latex pdf && \
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26979
diff changeset
   139
    "$ISABELLE_TOOL" latex -o pdf
9788
wenzelm
parents: 8654
diff changeset
   140
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   141
  else
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   142
    pre_latex dvi && \
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26979
diff changeset
   143
    "$ISABELLE_TOOL" latex -o "$OUTFORMAT"
9788
wenzelm
parents: 8654
diff changeset
   144
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   145
  fi
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   146
11581
d7bb261e3a3b -v option;
wenzelm
parents: 10555
diff changeset
   147
  if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   148
    cp -f "root.$OUTFORMAT" "../$NAME.$OUTFORMAT"
11581
d7bb261e3a3b -v option;
wenzelm
parents: 10555
diff changeset
   149
  fi
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   150
8217
dc3b8cdbb816 option -c;
wenzelm
parents: 8212
diff changeset
   151
  exit "$RC"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   152
)
9788
wenzelm
parents: 8654
diff changeset
   153
RC="$?"
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   154
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   155
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   156
# install
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   157
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   158
[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   159
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   160
#beware!
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   161
[ -n "$CLEAN" ] && rm -rf "$DIR"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   162
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   163
exit "$RC"