author | wenzelm |
Wed, 21 Sep 2016 20:33:44 +0200 | |
changeset 63932 | 6040db6b929d |
parent 62840 | d9744f41a4ec |
child 66906 | 03a96b8c7c06 |
permissions | -rwxr-xr-x |
25632 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
57439
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
52062
diff
changeset
|
3 |
# Author: Makarius |
25632 | 4 |
# |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62562
diff
changeset
|
5 |
# DESCRIPTION: raw ML process (interactive mode) |
25632 | 6 |
|
62559 | 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-*) |
62840
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62589
diff
changeset
|
11 |
ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS32" |
61135
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-*) |
62840
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62589
diff
changeset
|
14 |
ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS64" |
61135
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 |
|
62840
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62589
diff
changeset
|
18 |
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)" |
57580
86b413b8f779
check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
57439
diff
changeset
|
19 |
|
57686 | 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 |
62589
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents:
62588
diff
changeset
|
24 |
exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
62562
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\"" |
62589
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents:
62588
diff
changeset
|
27 |
exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
62562
905a5db3932d
back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents:
62559
diff
changeset
|
28 |
fi |