#!/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' "$@"