--- a/lib/Tools/console Tue Mar 08 19:29:56 2016 +0100
+++ b/lib/Tools/console Tue Mar 08 20:02:46 2016 +0100
@@ -19,4 +19,10 @@
mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
+if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
+then
+ exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
+else
+ echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
+ exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
+fi