diff -r 3000965b1fdf -r 7726fbf5f81f etc/settings
--- a/etc/settings	Fri Dec 14 21:15:32 2007 +0100
+++ b/etc/settings	Fri Dec 14 21:15:33 2007 +0100
@@ -76,7 +76,16 @@
 
 
 ###
-### Compilation options (cf. isatool usedir)
+### Interactive sessions (cf. isatool tty)
+###
+
+ISABELLE_LINE_EDITOR=""
+[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
+[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
+
+
+###
+### Batch sessions (cf. isatool usedir)
 ###
 
 ISABELLE_USEDIR_OPTIONS="-p 1 -v true -V outline=/proof,/ML"