#!/usr/bin/env bash

#

# Author: Makarius

#

# build - build Isabelle/ML

#

# Requires proper Isabelle settings environment.

## diagnostics

function usage()

{

  echo

  echo "Usage: $PRG TARGET OUTPUT"

  echo

  exit 1

}

function fail()

{

  echo "$1" >&2

  exit 2

}

[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"

## process command line

# args

if [ "$#" -eq 2 ]; then

  TARGET="$1"; shift

  OUTPUT="$1"; shift

else

  usage

fi

## main

# get compatibility file

ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)

[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"

COMPAT=""

[ -f "ML-Systems/${ML_SYSTEM_BASE}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM_BASE}.ML"

[ -f "ML-Systems/${ML_SYSTEM}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM}.ML"

[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"

# run isabelle

. "$ISABELLE_HOME/lib/scripts/timestart.bash"

if [ "$TARGET" = RAW ]; then

  if [ -z "$OUTPUT" ]; then

    "$ISABELLE_PROCESS" \

      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \

      -q RAW_ML_SYSTEM

  else

    "$ISABELLE_PROCESS" \

      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \

      -e "structure Isar = struct fun main () = () end;" \

      -e "ml_prompts \"ML> \" \"ML# \";" \

      -q -w RAW_ML_SYSTEM "$OUTPUT"

  fi

else

  if [ -z "$OUTPUT" ]; then

    "$ISABELLE_PROCESS" \

      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \

      -q RAW_ML_SYSTEM

  else

    "$ISABELLE_PROCESS" \

      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \

      -e "ml_prompts \"ML> \" \"ML# \";" \

      -f -q -w RAW_ML_SYSTEM "$OUTPUT"

  fi

fi

RC="$?"

. "$ISABELLE_HOME/lib/scripts/timestop.bash"

if [ "$RC" -eq 0 ]; then

  echo "Finished $TARGET ($TIMES_REPORT)" >&2

fi

exit "$RC"