Admin/lib/Tools/build_doc
author wenzelm
Sat, 05 Apr 2014 23:56:21 +0200
changeset 56432 96b54a96b117
parent 56429 bc61161a5bd0
child 61135 8f7d802b7a71
permissions -rwxr-xr-x
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     2
#
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     3
# Author: Makarius
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     4
#
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: build Isabelle documentation
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     6
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     7
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     8
## diagnostics
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     9
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    10
PRG="$(basename "$0")"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    11
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    12
function usage()
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    13
{
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    14
  echo
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    15
  echo "Usage: isabelle $PRG [OPTIONS] [DOCS ...]"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    16
  echo
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    17
  echo "  Options are:"
56432
wenzelm
parents: 56429
diff changeset
    18
  echo "    -a           select all documentation sessions"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    19
  echo "    -j INT       maximum number of parallel jobs (default 1)"
53208
bec95e287d26 prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
wenzelm
parents: 52740
diff changeset
    20
  echo "    -s           system build mode"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    21
  echo
56432
wenzelm
parents: 56429
diff changeset
    22
  echo "  Build Isabelle documentation from documentation sessions with"
wenzelm
parents: 56429
diff changeset
    23
  echo "  suitable document_variants entry."
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    24
  echo
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    25
  exit 1
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    26
}
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    27
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    28
function fail()
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    29
{
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    30
  echo "$1" >&2
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    31
  exit 2
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    32
}
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    33
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    34
function check_number()
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    35
{
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    36
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    37
}
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    38
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    39
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    40
## process command line
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    41
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    42
ALL_DOCS="false"
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    43
MAX_JOBS="1"
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    44
SYSTEM_MODE="false"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    45
53208
bec95e287d26 prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
wenzelm
parents: 52740
diff changeset
    46
while getopts "aj:s" OPT
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    47
do
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    48
  case "$OPT" in
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    49
    a)
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    50
      ALL_DOCS="true"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    51
      ;;
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    52
    j)
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    53
      check_number "$OPTARG"
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    54
      MAX_JOBS="$OPTARG"
53208
bec95e287d26 prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
wenzelm
parents: 52740
diff changeset
    55
      ;;
bec95e287d26 prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
wenzelm
parents: 52740
diff changeset
    56
    s)
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    57
      SYSTEM_MODE="true"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    58
      ;;
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    59
    \?)
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    60
      usage
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    61
      ;;
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    62
  esac
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    63
done
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    64
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    65
shift $(($OPTIND - 1))
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    66
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    67
[ "$ALL_DOCS" = false -a "$#" -eq 0 ] && usage
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    68
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    69
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    70
## main
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    71
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    72
isabelle_admin_build jars || exit $?
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    73
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    74
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    75
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    76
"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc \
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    77
  "$ALL_DOCS" "$MAX_JOBS" "$SYSTEM_MODE" "$@"
49005
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    78