1#!/usr/bin/env bash 2# 3# Author: Makarius 4# 5# DESCRIPTION: raw ML process (interactive mode) 6 7isabelle_admin_build jars || exit $? 8 9eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)" 10 11mkdir -p "$ISABELLE_TMP_PREFIX" || exit $? 12 13if type -p "$ISABELLE_LINE_EDITOR" > /dev/null 14then 15 exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" 16else 17 echo >&2 "### No line editor: \"$ISABELLE_LINE_EDITOR\"" 18 exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" 19fi 20