lib/Tools/console
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 66906 03a96b8c7c06
permissions -rwxr-xr-x
more robust sorted_entries;
wenzelm@25632
     1
#!/usr/bin/env bash
wenzelm@25632
     2
#
wenzelm@57439
     3
# Author: Makarius
wenzelm@25632
     4
#
wenzelm@62588
     5
# DESCRIPTION: raw ML process (interactive mode)
wenzelm@25632
     6
wenzelm@62559
     7
isabelle_admin_build jars || exit $?
wenzelm@61135
     8
wenzelm@66906
     9
eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
wenzelm@57580
    10
wenzelm@57686
    11
mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
wenzelm@57581
    12
wenzelm@62562
    13
if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
wenzelm@62562
    14
then
wenzelm@62589
    15
  exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
wenzelm@62562
    16
else
wenzelm@62562
    17
  echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
wenzelm@62589
    18
  exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
wenzelm@62562
    19
fi