diff -r 4bf00f54e4bc -r 905a5db3932d lib/Tools/console
--- 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