--- a/NEWS Tue Mar 08 17:55:11 2016 +0100
+++ b/NEWS Tue Mar 08 18:15:16 2016 +0100
@@ -239,8 +239,10 @@
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 -r" helps to bootstrap
-Isabelle/Pure interactively.
+* 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.
* 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 17:55:11 2016 +0100
+++ b/etc/settings Tue Mar 08 18:15:16 2016 +0100
@@ -27,13 +27,6 @@
###
-### Interactive sessions (cf. isabelle console)
-###
-
-ISABELLE_LINE_EDITOR="rlwrap"
-
-
-###
### Batch sessions (cf. isabelle build)
###
--- a/lib/Tools/console Tue Mar 08 17:55:11 2016 +0100
+++ b/lib/Tools/console Tue Mar 08 18:15:16 2016 +0100
@@ -4,7 +4,7 @@
#
# DESCRIPTION: run Isabelle process with raw ML console and line editor
-## settings
+isabelle_admin_build jars || exit $?
case "$ISABELLE_JAVA_PLATFORM" in
x86-*)
@@ -15,112 +15,8 @@
;;
esac
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS]"
- echo
- echo " Options are:"
- echo " -d DIR include session directory"
- echo " -l NAME logic session name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
- echo " -m MODE add print mode for output"
- echo " -n no build of session image on startup"
- echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
- echo " -r logic session is RAW_ML_SYSTEM"
- echo " -s system build mode for session image"
- echo
- echo " Run Isabelle process with raw ML console and line editor"
- echo " (ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")."
- echo
- exit 1
-}
-
-
-## process command line
-
-# options
-
-declare -a ISABELLE_OPTIONS=()
-
-declare -a INCLUDE_DIRS=()
-LOGIC="$ISABELLE_LOGIC"
-NO_BUILD="false"
-declare -a SYSTEM_OPTIONS=()
-SYSTEM_MODE="false"
-
-while getopts "d:l:m:no:rs" OPT
-do
- case "$OPT" in
- d)
- INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
- ;;
- l)
- LOGIC="$OPTARG"
- ;;
- m)
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
- ;;
- n)
- NO_BUILD="true"
- ;;
- o)
- SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
- ;;
- r)
- LOGIC="RAW_ML_SYSTEM"
- ;;
- s)
- SYSTEM_MODE="true"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
-
-
-## main
-
-isabelle_admin_build jars || exit $?
-
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
-OPTIONS_FILE="$ISABELLE_TMP_PREFIX/options$$"
-if [ "$LOGIC" = "RAW_ML_SYSTEM" ]; then
- "$ISABELLE_TOOL" options -x "$OPTIONS_FILE"
-else
- "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
- "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" "$OPTIONS_FILE" \
- "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
- rm -f "$OPTIONS_FILE"
- exit "$?"
- }
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="ASCII"
-fi
-
-ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-O"
-ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTIONS_FILE"
-
-if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
-then
- exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
-else
- echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
- exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
-fi
+"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
--- a/src/Doc/System/Basics.thy Tue Mar 08 17:55:11 2016 +0100
+++ b/src/Doc/System/Basics.thy Tue Mar 08 18:15:16 2016 +0100
@@ -209,9 +209,6 @@
\<^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 17:55:11 2016 +0100
+++ b/src/Doc/System/Misc.thy Tue Mar 08 18:15:16 2016 +0100
@@ -72,29 +72,25 @@
-r logic session is RAW_ML_SYSTEM
-s system build mode for session image
- Run Isabelle process with raw ML console and line editor
- (default ISABELLE_LINE_EDITOR).\<close>}
+ Run Isabelle process with raw ML console and line editor.\<close>}
- The \<^verbatim>\<open>-l\<close> option 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> abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
+ 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>
+ abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
Isabelle/Pure interactively.
- Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed directly to @{tool build}
+ Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
(\secref{sec:tool-build}).
- Options \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> are passed directly to the underlying Isabelle process
- (\secref{sec:isabelle-process}).
+ Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for the raw @{executable
+ isabelle_process} (\secref{sec:isabelle-process}).
- The Isabelle 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.
-
- Interaction works via the raw ML toplevel loop: this is neither
- Isabelle/Isar nor Isabelle/ML within the usual formal context. Some useful
- ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML use_thys}.
+ \<^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}.
\<close>
--- a/src/Pure/Tools/build_console.scala Tue Mar 08 17:55:11 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-/* Title: Pure/Tools/build_console.scala
- Author: Makarius
-
-Check and build Isabelle session for console tool.
-*/
-
-package isabelle
-
-
-object Build_Console
-{
- /* build_console */
-
- def build_console(
- options: Options,
- progress: Progress = Ignore_Progress,
- dirs: List[Path] = Nil,
- no_build: Boolean = false,
- system_mode: Boolean = false,
- session: String): Int =
- {
- if (no_build ||
- Build.build(options = options, build_heap = true, no_build = true,
- dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0) 0
- else {
- progress.echo("Build started for Isabelle/" + session + " ...")
- Build.build(options = options, progress = progress, build_heap = true,
- dirs = dirs, system_mode = system_mode, sessions = List(session))
- }
- }
-
-
- /* command line entry point */
-
- def main(args: Array[String])
- {
- Command_Line.tool {
- args.toList match {
- case
- session ::
- Properties.Value.Boolean(no_build) ::
- Properties.Value.Boolean(system_mode) ::
- options_file ::
- Command_Line.Chunks(dirs, system_options) =>
- val options = (Options.init() /: system_options)(_ + _)
- File.write(Path.explode(options_file), YXML.string_of_body(options.encode))
-
- val progress = new Console_Progress()
- progress.interrupt_handler {
- build_console(options, progress,
- dirs.map(Path.explode(_)), no_build, system_mode, session)
- }
- case _ => error("Bad arguments:\n" + cat_lines(args))
- }
- }
- }
-}
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/ml_console.scala Tue Mar 08 18:15:16 2016 +0100
@@ -0,0 +1,132 @@
+/* Title: Pure/Tools/ml_console.scala
+ Author: Makarius
+
+Run Isabelle process with raw ML console and line editor.
+*/
+
+package isabelle
+
+
+import scala.annotation.tailrec
+
+import jline.console.ConsoleReader
+import jline.console.history.FileHistory
+
+
+object ML_Console
+{
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool {
+ var dirs: List[Path] = Nil
+ var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+ var modes: List[String] = Nil
+ var no_build = false
+ var options = Options.init()
+ var system_mode = false
+
+ val getopts = Getopts("""
+Usage: isabelle console [OPTIONS]
+
+ Options are:
+ -d DIR include session directory
+ -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(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.
+""",
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "l:" -> (arg => logic = arg),
+ "m:" -> (arg => modes = arg :: modes),
+ "n" -> (arg => no_build = true),
+ "o:" -> (arg => options = options + arg),
+ "r" -> (_ => logic = "RAW_ML_SYSTEM"),
+ "s" -> (_ => system_mode = true))
+
+ val more_args = getopts(args)
+ if (!more_args.isEmpty) getopts.usage()
+
+
+ // build
+ if (!no_build && logic != "RAW_ML_SYSTEM" &&
+ Build.build(options = options, build_heap = true, no_build = true,
+ dirs = dirs, system_mode = system_mode, sessions = List(logic)) != 0)
+ {
+ val progress = new Console_Progress
+ progress.echo("Build started for Isabelle/" + logic + " ...")
+ progress.interrupt_handler {
+ val rc =
+ Build.build(options = options, progress = progress, build_heap = true,
+ dirs = dirs, system_mode = system_mode, sessions = List(logic))
+ if (rc != 0) sys.exit(rc)
+ }
+ }
+
+ // 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,
+ modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"))
+ val process_output = Future.thread[Unit]("process_output") {
+ var result = new StringBuilder(100)
+ var finished = false
+ while (!finished) {
+ var c = -1
+ var done = false
+ while (!done && (result.length == 0 || process.stdout.ready)) {
+ c = process.stdout.read
+ if (c >= 0) result.append(c.asInstanceOf[Char])
+ else done = true
+ }
+ if (result.length > 0) {
+ System.out.print(result.toString)
+ System.out.flush()
+ result.length = 0
+ }
+ else {
+ process.stdout.close()
+ finished = true
+ }
+ }
+ }
+ val process_input = Future.thread[Unit]("process_input") {
+ POSIX_Interrupt.handler { process.interrupt } {
+ var finished = false
+ while (!finished) {
+ reader.readLine() match {
+ case null =>
+ process.stdin.close()
+ finished = true
+ case line =>
+ process.stdin.write(line)
+ process.stdin.write("\n")
+ process.stdin.flush()
+ }
+ }
+ }
+ }
+ val process_result = Future.thread[Int]("process_result") {
+ val rc = process.join
+ process_input.cancel
+ rc
+ }
+
+ process_output.join
+ process_input.join
+
+ val rc = process_result.join
+ history.flush()
+ rc
+ }
+ }
+}
--- a/src/Pure/build-jars Tue Mar 08 17:55:11 2016 +0100
+++ b/src/Pure/build-jars Tue Mar 08 18:15:16 2016 +0100
@@ -96,13 +96,13 @@
Thy/thy_syntax.scala
Tools/bibtex.scala
Tools/build.scala
- Tools/build_console.scala
Tools/build_doc.scala
Tools/check_keywords.scala
Tools/check_sources.scala
Tools/debugger.scala
Tools/doc.scala
Tools/main.scala
+ Tools/ml_console.scala
Tools/ml_statistics.scala
Tools/news.scala
Tools/print_operation.scala