lib/Tools/console
author wenzelm
Thu, 10 Mar 2016 12:11:50 +0100
changeset 62588 cd266473b81b
parent 62562 905a5db3932d
child 62589 b5783412bfed
permissions -rwxr-xr-x
isabelle_process is superseded by "isabelle process" tool; tuned tool usage; misc updates and tuning of "system" manual;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25632
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
     2
#
57439
0e41f26a0250 "isabelle tty" is superseded by "isabelle console";
wenzelm
parents: 52062
diff changeset
     3
# Author: Makarius
25632
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
     4
#
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62562
diff changeset
     5
# DESCRIPTION: raw ML process (interactive mode)
25632
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
     6
62559
83e815849a91 isabelle console is based on Isabelle/Scala;
wenzelm
parents: 62509
diff changeset
     7
isabelle_admin_build jars || exit $?
61135
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 57686
diff changeset
     8
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 57686
diff changeset
     9
case "$ISABELLE_JAVA_PLATFORM" in
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 57686
diff changeset
    10
  x86-*)
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 57686
diff changeset
    11
    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 57686
diff changeset
    12
    ;;
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 57686
diff changeset
    13
  x86_64-*)
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 57686
diff changeset
    14
    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 57686
diff changeset
    15
    ;;
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 57686
diff changeset
    16
esac
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 57686
diff changeset
    17
57580
86b413b8f779 check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;
wenzelm
parents: 57439
diff changeset
    18
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
86b413b8f779 check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;
wenzelm
parents: 57439
diff changeset
    19
57686
5b16e2370ccb proper mkdir;
wenzelm
parents: 57581
diff changeset
    20
mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
57581
74bbe9317aa4 provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents: 57580
diff changeset
    21
62562
905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents: 62559
diff changeset
    22
if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents: 62559
diff changeset
    23
then
905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents: 62559
diff changeset
    24
  exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents: 62559
diff changeset
    25
else
905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents: 62559
diff changeset
    26
  echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents: 62559
diff changeset
    27
  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents: 62559
diff changeset
    28
fi