lib/Tools/document
author webertj
Fri, 17 Aug 2012 20:31:12 +0200
changeset 48853 ec82c33c75f8
parent 48657 63ef2f0cf8bb
child 51081 70a4c11cd79e
permissions -rwxr-xr-x
Typo fixed.
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
48616
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
    88
# document variants
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
    89
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
    90
ROOT_NAME="root_$NAME"
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
    91
[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
17049
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
function prep_tags ()
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    94
{
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    95
  (
32322
45cb4a86eca2 change IFS only locally -- thanks to bash arrays;
wenzelm
parents: 29143
diff changeset
    96
    for TAG in "${TAGS[@]}"
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    97
    do
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
    98
      case "$TAG" in
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 "\\isafoldtag{${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 "\\isadroptag{${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:1}}"
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
        *)
32322
45cb4a86eca2 change IFS only locally -- thanks to bash arrays;
wenzelm
parents: 29143
diff changeset
   109
          echo "\\isakeeptag{${TAG}}"
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   110
          ;;
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   111
      esac
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   112
    done
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   113
  ) > isabelletags.sty
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
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   116
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   117
# prepare document
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   118
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   119
function pre_latex ()
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   120
{
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   121
  local FMT="$1"
14367
0b1447d37161 remove more files (index, log files) for -c option
kleing
parents: 14344
diff changeset
   122
  [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
48616
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
   123
  "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
   124
  "$ISABELLE_TOOL" latex -o "$FMT" "$ROOT_NAME.tex" && \
48637
547b075669ae more precise guide for bibtex/makeindex -- dummy files should be sufficient;
wenzelm
parents: 48616
diff changeset
   125
  { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
547b075669ae more precise guide for bibtex/makeindex -- dummy files should be sufficient;
wenzelm
parents: 48616
diff changeset
   126
  { [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 26979
diff changeset
   127
  "$ISABELLE_TOOL" latex -o "$FMT"
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   128
}
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   129
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   130
(
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   131
  cd "$DIR" || fail "Bad directory '$DIR'"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   132
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   133
  [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT"
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   134
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   135
  prep_tags
8654
38ce936acb99 tuned -c option;
wenzelm
parents: 8269
diff changeset
   136
48657
63ef2f0cf8bb simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents: 48637
diff changeset
   137
  if [ -f build ]; then
63ef2f0cf8bb simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents: 48637
diff changeset
   138
    ./build "$OUTFORMAT" "$NAME"
9788
wenzelm
parents: 8654
diff changeset
   139
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   140
  elif [ "$OUTFORMAT" = pdf ]; then
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   141
    pre_latex pdf && \
48616
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
   142
    "$ISABELLE_TOOL" latex -o pdf "$ROOT_NAME.tex"
9788
wenzelm
parents: 8654
diff changeset
   143
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   144
  else
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   145
    pre_latex dvi && \
48616
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
   146
    "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
9788
wenzelm
parents: 8654
diff changeset
   147
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   148
  fi
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   149
48616
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
   150
  if [ "$RC" -eq 0 -a -f "$ROOT_NAME.$OUTFORMAT" ]; then
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
   151
    cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
11581
d7bb261e3a3b -v option;
wenzelm
parents: 10555
diff changeset
   152
  fi
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   153
8217
dc3b8cdbb816 option -c;
wenzelm
parents: 8212
diff changeset
   154
  exit "$RC"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   155
)
9788
wenzelm
parents: 8654
diff changeset
   156
RC="$?"
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   157
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   158
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   159
# install
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   160
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   161
[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   162
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   163
#beware!
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   164
[ -n "$CLEAN" ] && rm -rf "$DIR"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   165
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   166
exit "$RC"