isabelle: lib/Tools/console@78913f29fc21 (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
74038 b4f57bfe82e7 more robust "isabelle build_scala" as separate tool; wenzelm parents: 74017 diff changeset	7	isabelle scala_build \|\| exit $?
61135 8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component); wenzelm parents: 57686 diff changeset	8
66906 03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only; wenzelm parents: 62840 diff changeset	9	eval "declare -a 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	10
57686 5b16e2370ccb proper mkdir; wenzelm parents: 57581 diff changeset	11	mkdir -p "$ISABELLE_TMP_PREFIX" \|\| exit $?
57581 74bbe9317aa4 provide explicit options file -- avoid multiple Scala/JVM invocation; wenzelm parents: 57580 diff changeset	12
62562 905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out; wenzelm parents: 62559 diff changeset	13	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	14	then
62589 b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment; wenzelm parents: 62588 diff changeset	15	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	16	else
71373 201486ced92d clarified output channel; wenzelm parents: 66906 diff changeset	17	echo >&2 "### No line editor: \"$ISABELLE_LINE_EDITOR\""
62589 b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment; wenzelm parents: 62588 diff changeset	18	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	19	fi

author	wenzelm
	Tue, 14 Mar 2023 17:34:38 +0100
changeset 77654	78913f29fc21
parent 74038	b4f57bfe82e7
permissions	-rwxr-xr-x