Admin/lib/Tools/build_doc

added field to record

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: build Isabelle documentation


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
  echo
  echo "  Options are:"
  echo "    -a           select all doc sessions"
  echo "    -j INT       maximum number of parallel jobs (default 1)"
  echo "    -p           build only pdf documents"
  echo
  echo "  Build Isabelle documentation from (doc) sessions."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}

function check_number()
{
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
}


## process command line

# options

ALL_DOCS="false"
JOBS=""
PDF_ONLY=""

while getopts "aj:p" OPT
do
  case "$OPT" in
    a)
      ALL_DOCS="true"
      ;;
    j)
      check_number "$OPTARG"
      JOBS="-j $OPTARG"
      ;;
    p)
      PDF_ONLY="true"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# arguments

if [ "$ALL_DOCS" = true ]; then
  declare -a BUILD_ARGS=(-g doc)
else
  declare -a BUILD_ARGS=()
  [ "$#" -eq 0 ] && usage
fi

BUILD_ARGS["${#BUILD_ARGS[@]}"]="--"

while [ "$#" -ne 0 ]; do
  BUILD_ARGS["${#BUILD_ARGS[@]}"]="$1"
  shift
done


## main

OUTPUT="$ISABELLE_TMP_PREFIX$$"
mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\""

"$ISABELLE_TOOL" build -R -b $JOBS "${BUILD_ARGS[@]}"
RC=$?

if [ "$PDF_ONLY" = true ]; then
  FORMATS="pdf"
else
  FORMATS="dvi pdf"
fi

for FORMAT in $FORMATS
do
  if [ "$RC" = 0 ]; then
    echo "Document format: $FORMAT"
    "$ISABELLE_TOOL" build -o browser_info=false -o "document=$FORMAT" \
      -o "document_output=$OUTPUT" -c $JOBS "${BUILD_ARGS[@]}"
    RC=$?
  fi
done

if [ "$RC" = 0 ]; then
  for FILE in $(find "$OUTPUT" -name "*.eps" -o -name "*.ps")
  do
    cp -f "$FILE" "$ISABELLE_HOME/doc"
  done
  if [ "$PDF_ONLY" = true ]; then
    cp -f "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
  else
    cp -f "$OUTPUT"/*.dvi "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
  fi
fi

rm -rf "$OUTPUT"

exit $RC