back to external line editor, due to problems of JLine with multithreading of in vs. out;

--- a/NEWS	Tue Mar 08 19:29:56 2016 +0100
+++ b/NEWS	Tue Mar 08 20:02:46 2016 +0100
@@ -239,10 +239,8 @@
 expressions (option -e) or files (option -f). Errors lead to premature
 exit of the ML process with return code 1.
 
-* Command-line tool "isabelle console" is now based on Isabelle/Scala
-and uses the built-in JLine editor instead of ISABELLE_LINE_EDITOR
-(default "rlwrap"). The new option "-r" helps to bootstrap Isabelle/Pure
-interactively.
+* Command-line tool "isabelle console -r" helps to bootstrap
+Isabelle/Pure interactively.
 
 * The somewhat pointless command-line tool "isabelle yxml" has been
 discontinued. INCOMPATIBILITY, use operations from the modules "XML" and

--- a/etc/settings	Tue Mar 08 19:29:56 2016 +0100
+++ b/etc/settings	Tue Mar 08 20:02:46 2016 +0100
@@ -27,6 +27,13 @@
 
 
 ###
+### Interactive sessions (cf. isabelle console)
+###
+
+ISABELLE_LINE_EDITOR="rlwrap"
+
+
+###
 ### Batch sessions (cf. isabelle build)
 ###
 

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

--- a/src/Doc/System/Basics.thy	Tue Mar 08 19:29:56 2016 +0100
+++ b/src/Doc/System/Basics.thy	Tue Mar 08 20:02:46 2016 +0100
@@ -209,6 +209,9 @@
   \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
   is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
 
+  \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
+  @{tool_ref console} interface.
+
   \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
   @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
   document preparation (see also \secref{sec:tool-latex}).

--- a/src/Doc/System/Misc.thy	Tue Mar 08 19:29:56 2016 +0100
+++ b/src/Doc/System/Misc.thy	Tue Mar 08 20:02:46 2016 +0100
@@ -65,14 +65,15 @@
 
   Options are:
     -d DIR       include session directory
-    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
+    -l NAME      logic session name (default ISABELLE_LOGIC)
     -m MODE      add print mode for output
     -n           no build of session image on startup
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -r           logic session is RAW_ML_SYSTEM
     -s           system build mode for session image
 
-  Run Isabelle process with raw ML console and line editor.\<close>}
+  Run Isabelle process with raw ML console and line editor
+  (default ISABELLE_LINE_EDITOR).\<close>}
 
   Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
   checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
@@ -86,11 +87,15 @@
   isabelle_process} (\secref{sec:isabelle-process}).
 
   \<^medskip>
-  Interaction works via the built-in line editor of Scala, which is based on
-  JLine\<^footnote>\<open>@{url "https://github.com/jline"}\<close>. The user is connected to the raw
-  ML toplevel loop: this is neither Isabelle/Isar nor Isabelle/ML within the
-  usual formal context. The most relevant ML commands at this stage are @{ML
-  use}, @{ML use_thy}, @{ML use_thys}.
+  The Isabelle/ML process is run through the line editor that is specified via
+  the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
+  @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
+  standard input/output.
+
+  The user is connected to the raw ML toplevel loop: this is neither
+  Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
+  relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
+  use_thys}.
 \<close>
 
 

--- a/src/Pure/Tools/ml_console.scala	Tue Mar 08 19:29:56 2016 +0100
+++ b/src/Pure/Tools/ml_console.scala	Tue Mar 08 20:02:46 2016 +0100
@@ -7,12 +7,7 @@
 package isabelle
 
 
-import java.io.IOException
-
-import scala.annotation.tailrec
-
-import jline.console.ConsoleReader
-import jline.console.history.FileHistory
+import java.io.{IOException, BufferedReader, InputStreamReader}
 
 
 object ML_Console
@@ -41,7 +36,8 @@
     -r           logic session is RAW_ML_SYSTEM
     -s           system build mode for session image
 
-  Run Isabelle process with raw ML console and line editor.
+  Run Isabelle process with raw ML console and line editor
+  (ISABELLE_LINE_EDITOR=""" + quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
 """,
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "l:" -> (arg => logic = arg),
@@ -70,11 +66,6 @@
         }
       }
 
-      // reader with history
-      val history = new FileHistory(Path.explode("$ISABELLE_HOME_USER/console_history").file)
-      val reader = new ConsoleReader
-      reader.setHistory(history)
-
       // process loop
       val process =
         ML_Process(options, heap = logic,
@@ -105,6 +96,7 @@
         catch { case e: IOException => case Exn.Interrupt() => }
       }
       val process_input = Future.thread[Unit]("process_input") {
+        val reader = new BufferedReader(new InputStreamReader(System.in))
         POSIX_Interrupt.handler { process.interrupt } {
           try {
             var finished = false
@@ -131,10 +123,7 @@
 
       process_output.join
       process_input.join
-
-      val rc = process_result.join
-      history.flush()
-      rc
+      process_result.join
     }
   }
 }