isabelle: lib/Tools/console@187277b77d50 (annotated)

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-*)
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 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
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

author	wenzelm
	Sun, 12 Mar 2017 18:50:02 +0100
changeset 65202	187277b77d50
parent 62840	d9744f41a4ec
child 66906	03a96b8c7c06
permissions	-rwxr-xr-x