#!/usr/bin/env bash

 #

 # Author: Makarius

 #

 # DESCRIPTION: build and manage Isabelle sessions

 ## diagnostics

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

 function usage()

 {

   echo

   echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"

   echo

   echo "  Options are:"

   echo "    -a           all sessions"

   echo "    -b           build target images"

   echo "    -d DIR       additional session directory with ROOT file"

   echo "    -j INT       maximum number of jobs (default 1)"

   echo "    -l           list sessions only"

   echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"

   echo "    -v           verbose"

   echo

   echo "  Build and manage Isabelle sessions, depending on implicit"

   echo "  ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""

   echo

   echo "  ML_PLATFORM=\"$ML_PLATFORM\""

   echo "  ML_HOME=\"$ML_HOME\""

   echo "  ML_SYSTEM=\"$ML_SYSTEM\""

   echo "  ML_OPTIONS=\"$ML_OPTIONS\""

   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

 ALL_SESSIONS=false

 BUILD_IMAGES=false

 MAX_JOBS=1

 LIST_ONLY=false

 VERBOSE=false

 declare -a MORE_DIRS=()

 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"

 while getopts "abd:j:lo:v" OPT

 do

   case "$OPT" in

     a)

       ALL_SESSIONS="true"

       ;;

     b)

       BUILD_IMAGES="true"

       ;;

     d)

       MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"

       ;;

     j)

       check_number "$OPTARG"

       MAX_JOBS="$OPTARG"

       ;;

     l)

       LIST_ONLY="true"

       ;;

     o)

       BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"

       ;;

     v)

       VERBOSE="true"

       ;;

     \?)

       usage

       ;;

   esac

 done

 shift $(($OPTIND - 1))

 ## main

 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }

 exec "$ISABELLE_TOOL" java isabelle.Build \

   "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$VERBOSE" \

   "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"