# HG changeset patch # User wenzelm # Date 1457457316 -3600 # Node ID 83e815849a917ffd75f9bec2a858e19bf8f4dd18 # Parent c46418f12ee149e582ecacc3794b7ea18f80e86f isabelle console is based on Isabelle/Scala; diff -r c46418f12ee1 -r 83e815849a91 NEWS --- 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 diff -r c46418f12ee1 -r 83e815849a91 etc/settings --- 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) ### diff -r c46418f12ee1 -r 83e815849a91 lib/Tools/console --- 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 "$@" diff -r c46418f12ee1 -r 83e815849a91 src/Doc/System/Basics.thy --- 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>\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 c46418f12ee1 -r 83e815849a91 src/Doc/System/Misc.thy --- 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).\} + Run Isabelle process with raw ML console and line editor.\} - The \<^verbatim>\-l\ option 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\ abbreviates \<^verbatim>\-l RAW_ML_SYSTEM\, which is relevant to bootstrap + 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\ + abbreviates \<^verbatim>\-l RAW_ML_SYSTEM\, which is relevant to bootstrap Isabelle/Pure interactively. - Options \<^verbatim>\-d\, \<^verbatim>\-o\, \<^verbatim>\-s\ are passed directly to @{tool build} + Options \<^verbatim>\-d\ and \<^verbatim>\-s\ have the same meaning as for @{tool build} (\secref{sec:tool-build}). - Options \<^verbatim>\-m\, \<^verbatim>\-o\ are passed directly to the underlying Isabelle process - (\secref{sec:isabelle-process}). + Options \<^verbatim>\-m\ and \<^verbatim>\-o\ 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>\@{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}. \ diff -r c46418f12ee1 -r 83e815849a91 src/Pure/Tools/build_console.scala --- 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)) - } - } - } -} - diff -r c46418f12ee1 -r 83e815849a91 src/Pure/Tools/ml_console.scala --- /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 + } + } +} diff -r c46418f12ee1 -r 83e815849a91 src/Pure/build-jars --- 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