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