back to external line editor, due to problems of JLine with multithreading of in vs. out;
authorwenzelm
Tue Mar 08 20:02:46 2016 +0100 (2016-03-08 ago)
changeset 62562905a5db3932d
parent 62561 4bf00f54e4bc
child 62563 2e352f63d15f
back to external line editor, due to problems of JLine with multithreading of in vs. out;
NEWS
etc/settings
lib/Tools/console
src/Doc/System/Basics.thy
src/Doc/System/Misc.thy
src/Pure/Tools/ml_console.scala
     1.1 --- a/NEWS	Tue Mar 08 19:29:56 2016 +0100
     1.2 +++ b/NEWS	Tue Mar 08 20:02:46 2016 +0100
     1.3 @@ -239,10 +239,8 @@
     1.4  expressions (option -e) or files (option -f). Errors lead to premature
     1.5  exit of the ML process with return code 1.
     1.6  
     1.7 -* Command-line tool "isabelle console" is now based on Isabelle/Scala
     1.8 -and uses the built-in JLine editor instead of ISABELLE_LINE_EDITOR
     1.9 -(default "rlwrap"). The new option "-r" helps to bootstrap Isabelle/Pure
    1.10 -interactively.
    1.11 +* Command-line tool "isabelle console -r" helps to bootstrap
    1.12 +Isabelle/Pure interactively.
    1.13  
    1.14  * The somewhat pointless command-line tool "isabelle yxml" has been
    1.15  discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
     2.1 --- a/etc/settings	Tue Mar 08 19:29:56 2016 +0100
     2.2 +++ b/etc/settings	Tue Mar 08 20:02:46 2016 +0100
     2.3 @@ -27,6 +27,13 @@
     2.4  
     2.5  
     2.6  ###
     2.7 +### Interactive sessions (cf. isabelle console)
     2.8 +###
     2.9 +
    2.10 +ISABELLE_LINE_EDITOR="rlwrap"
    2.11 +
    2.12 +
    2.13 +###
    2.14  ### Batch sessions (cf. isabelle build)
    2.15  ###
    2.16  
     3.1 --- a/lib/Tools/console	Tue Mar 08 19:29:56 2016 +0100
     3.2 +++ b/lib/Tools/console	Tue Mar 08 20:02:46 2016 +0100
     3.3 @@ -19,4 +19,10 @@
     3.4  
     3.5  mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
     3.6  
     3.7 -"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
     3.8 +if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
     3.9 +then
    3.10 +  exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
    3.11 +else
    3.12 +  echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
    3.13 +  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
    3.14 +fi
     4.1 --- a/src/Doc/System/Basics.thy	Tue Mar 08 19:29:56 2016 +0100
     4.2 +++ b/src/Doc/System/Basics.thy	Tue Mar 08 20:02:46 2016 +0100
     4.3 @@ -209,6 +209,9 @@
     4.4    \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
     4.5    is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
     4.6  
     4.7 +  \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
     4.8 +  @{tool_ref console} interface.
     4.9 +
    4.10    \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
    4.11    @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
    4.12    document preparation (see also \secref{sec:tool-latex}).
     5.1 --- a/src/Doc/System/Misc.thy	Tue Mar 08 19:29:56 2016 +0100
     5.2 +++ b/src/Doc/System/Misc.thy	Tue Mar 08 20:02:46 2016 +0100
     5.3 @@ -65,14 +65,15 @@
     5.4  
     5.5    Options are:
     5.6      -d DIR       include session directory
     5.7 -    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
     5.8 +    -l NAME      logic session name (default ISABELLE_LOGIC)
     5.9      -m MODE      add print mode for output
    5.10      -n           no build of session image on startup
    5.11      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    5.12      -r           logic session is RAW_ML_SYSTEM
    5.13      -s           system build mode for session image
    5.14  
    5.15 -  Run Isabelle process with raw ML console and line editor.\<close>}
    5.16 +  Run Isabelle process with raw ML console and line editor
    5.17 +  (default ISABELLE_LINE_EDITOR).\<close>}
    5.18  
    5.19    Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
    5.20    checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
    5.21 @@ -86,11 +87,15 @@
    5.22    isabelle_process} (\secref{sec:isabelle-process}).
    5.23  
    5.24    \<^medskip>
    5.25 -  Interaction works via the built-in line editor of Scala, which is based on
    5.26 -  JLine\<^footnote>\<open>@{url "https://github.com/jline"}\<close>. The user is connected to the raw
    5.27 -  ML toplevel loop: this is neither Isabelle/Isar nor Isabelle/ML within the
    5.28 -  usual formal context. The most relevant ML commands at this stage are @{ML
    5.29 -  use}, @{ML use_thy}, @{ML use_thys}.
    5.30 +  The Isabelle/ML process is run through the line editor that is specified via
    5.31 +  the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
    5.32 +  @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
    5.33 +  standard input/output.
    5.34 +
    5.35 +  The user is connected to the raw ML toplevel loop: this is neither
    5.36 +  Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
    5.37 +  relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
    5.38 +  use_thys}.
    5.39  \<close>
    5.40  
    5.41  
     6.1 --- a/src/Pure/Tools/ml_console.scala	Tue Mar 08 19:29:56 2016 +0100
     6.2 +++ b/src/Pure/Tools/ml_console.scala	Tue Mar 08 20:02:46 2016 +0100
     6.3 @@ -7,12 +7,7 @@
     6.4  package isabelle
     6.5  
     6.6  
     6.7 -import java.io.IOException
     6.8 -
     6.9 -import scala.annotation.tailrec
    6.10 -
    6.11 -import jline.console.ConsoleReader
    6.12 -import jline.console.history.FileHistory
    6.13 +import java.io.{IOException, BufferedReader, InputStreamReader}
    6.14  
    6.15  
    6.16  object ML_Console
    6.17 @@ -41,7 +36,8 @@
    6.18      -r           logic session is RAW_ML_SYSTEM
    6.19      -s           system build mode for session image
    6.20  
    6.21 -  Run Isabelle process with raw ML console and line editor.
    6.22 +  Run Isabelle process with raw ML console and line editor
    6.23 +  (ISABELLE_LINE_EDITOR=""" + quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
    6.24  """,
    6.25          "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    6.26          "l:" -> (arg => logic = arg),
    6.27 @@ -70,11 +66,6 @@
    6.28          }
    6.29        }
    6.30  
    6.31 -      // reader with history
    6.32 -      val history = new FileHistory(Path.explode("$ISABELLE_HOME_USER/console_history").file)
    6.33 -      val reader = new ConsoleReader
    6.34 -      reader.setHistory(history)
    6.35 -
    6.36        // process loop
    6.37        val process =
    6.38          ML_Process(options, heap = logic,
    6.39 @@ -105,6 +96,7 @@
    6.40          catch { case e: IOException => case Exn.Interrupt() => }
    6.41        }
    6.42        val process_input = Future.thread[Unit]("process_input") {
    6.43 +        val reader = new BufferedReader(new InputStreamReader(System.in))
    6.44          POSIX_Interrupt.handler { process.interrupt } {
    6.45            try {
    6.46              var finished = false
    6.47 @@ -131,10 +123,7 @@
    6.48  
    6.49        process_output.join
    6.50        process_input.join
    6.51 -
    6.52 -      val rc = process_result.join
    6.53 -      history.flush()
    6.54 -      rc
    6.55 +      process_result.join
    6.56      }
    6.57    }
    6.58  }