# HG changeset patch # User wenzelm # Date 1457463766 -3600 # Node ID 905a5db3932df9133e569ff85d3c34497987cd86 # Parent 4bf00f54e4bc5d07b1a6fc50d12ca48083dce3fd back to external line editor, due to problems of JLine with multithreading of in vs. out; diff -r 4bf00f54e4bc -r 905a5db3932d NEWS --- 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 diff -r 4bf00f54e4bc -r 905a5db3932d etc/settings --- 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) ### 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 diff -r 4bf00f54e4bc -r 905a5db3932d src/Doc/System/Basics.thy --- 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>\HOL\. + \<^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}). diff -r 4bf00f54e4bc -r 905a5db3932d src/Doc/System/Misc.thy --- 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.\} + Run Isabelle process with raw ML console and line editor + (default ISABELLE_LINE_EDITOR).\} Option \<^verbatim>\-l\ specifies the logic session name. By default, its heap image is checked and built on demand, but the option \<^verbatim>\-n\ skips that. Option \<^verbatim>\-r\ @@ -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>\@{url "https://github.com/jline"}\. 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}. \ diff -r 4bf00f54e4bc -r 905a5db3932d src/Pure/Tools/ml_console.scala --- 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 } } }