lib/Tools/document
author wenzelm
Fri, 19 May 2017 18:10:19 +0200
changeset 65875 12c90c0c4b32
parent 62589 b5783412bfed
child 67173 e746db6db903
permissions -rwxr-xr-x
suppress ANSI control sequences in Scala console;
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')"
52746
eec610972763 discontinued historic document formats;
wenzelm
parents: 51822
diff changeset
    18
  echo "    -o FORMAT    specify output format: pdf (default), dvi"
17049
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"
52746
eec610972763 discontinued historic document formats;
wenzelm
parents: 51822
diff changeset
    40
OUTFORMAT=pdf
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
52746
eec610972763 discontinued historic document formats;
wenzelm
parents: 51822
diff changeset
    80
  pdf | dvi)
7814
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
51822
7aebe43d6a14 avoid empty isabelletags.sty for the sake of arXiv;
wenzelm
parents: 51081
diff changeset
   113
    echo
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   114
  ) > isabelletags.sty
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
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   117
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   118
# prepare document
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   119
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   120
(
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   121
  cd "$DIR" || fail "Bad directory '$DIR'"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   122
52748
8e398d9bedf3 more uniform cleanup;
wenzelm
parents: 52747
diff changeset
   123
  [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT" *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   124
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   125
  prep_tags
8654
38ce936acb99 tuned -c option;
wenzelm
parents: 8269
diff changeset
   126
48657
63ef2f0cf8bb simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents: 48637
diff changeset
   127
  if [ -f build ]; then
63ef2f0cf8bb simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents: 48637
diff changeset
   128
    ./build "$OUTFORMAT" "$NAME"
9788
wenzelm
parents: 8654
diff changeset
   129
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   130
  else
62589
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 52748
diff changeset
   131
    isabelle latex -o sty "$ROOT_NAME.tex" && \
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 52748
diff changeset
   132
    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 52748
diff changeset
   133
    { [ ! -f "$ROOT_NAME.bib" ] || isabelle latex -o bbl "$ROOT_NAME.tex"; } && \
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 52748
diff changeset
   134
    { [ ! -f "$ROOT_NAME.idx" ] || isabelle latex -o idx "$ROOT_NAME.tex"; } && \
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 52748
diff changeset
   135
    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 52748
diff changeset
   136
    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
9788
wenzelm
parents: 8654
diff changeset
   137
    RC="$?"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   138
  fi
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   139
48616
be8002ee43d8 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents: 32390
diff changeset
   140
  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
   141
    cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
11581
d7bb261e3a3b -v option;
wenzelm
parents: 10555
diff changeset
   142
  fi
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   143
8217
dc3b8cdbb816 option -c;
wenzelm
parents: 8212
diff changeset
   144
  exit "$RC"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   145
)
9788
wenzelm
parents: 8654
diff changeset
   146
RC="$?"
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   147
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   148
7814
ef6d84f16592 check format;
wenzelm
parents: 7793
diff changeset
   149
# install
7793
e0676a932348 prepare theory session document;
wenzelm
parents:
diff changeset
   150
17049
ee573216713a added option -n NAME and -t TAGS;
wenzelm
parents: 14981
diff changeset
   151
[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   152
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   153
#beware!
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   154
[ -n "$CLEAN" ] && rm -rf "$DIR"
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   155
714f164f0385 rename -p to -P;
wenzelm
parents: 8171
diff changeset
   156
exit "$RC"