src/Pure/Tools/ml_console.scala
author wenzelm
Tue Mar 08 18:15:16 2016 +0100 (2016-03-08)
changeset 62559 83e815849a91
child 62561 4bf00f54e4bc
permissions -rw-r--r--
isabelle console is based on Isabelle/Scala;
wenzelm@62559
     1
/*  Title:      Pure/Tools/ml_console.scala
wenzelm@62559
     2
    Author:     Makarius
wenzelm@62559
     3
wenzelm@62559
     4
Run Isabelle process with raw ML console and line editor.
wenzelm@62559
     5
*/
wenzelm@62559
     6
wenzelm@62559
     7
package isabelle
wenzelm@62559
     8
wenzelm@62559
     9
wenzelm@62559
    10
import scala.annotation.tailrec
wenzelm@62559
    11
wenzelm@62559
    12
import jline.console.ConsoleReader
wenzelm@62559
    13
import jline.console.history.FileHistory
wenzelm@62559
    14
wenzelm@62559
    15
wenzelm@62559
    16
object ML_Console
wenzelm@62559
    17
{
wenzelm@62559
    18
  /* command line entry point */
wenzelm@62559
    19
wenzelm@62559
    20
  def main(args: Array[String])
wenzelm@62559
    21
  {
wenzelm@62559
    22
    Command_Line.tool {
wenzelm@62559
    23
      var dirs: List[Path] = Nil
wenzelm@62559
    24
      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
wenzelm@62559
    25
      var modes: List[String] = Nil
wenzelm@62559
    26
      var no_build = false
wenzelm@62559
    27
      var options = Options.init()
wenzelm@62559
    28
      var system_mode = false
wenzelm@62559
    29
wenzelm@62559
    30
      val getopts = Getopts("""
wenzelm@62559
    31
Usage: isabelle console [OPTIONS]
wenzelm@62559
    32
wenzelm@62559
    33
  Options are:
wenzelm@62559
    34
    -d DIR       include session directory
wenzelm@62559
    35
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
wenzelm@62559
    36
    -m MODE      add print mode for output
wenzelm@62559
    37
    -n           no build of session image on startup
wenzelm@62559
    38
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@62559
    39
    -r           logic session is RAW_ML_SYSTEM
wenzelm@62559
    40
    -s           system build mode for session image
wenzelm@62559
    41
wenzelm@62559
    42
  Run Isabelle process with raw ML console and line editor.
wenzelm@62559
    43
""",
wenzelm@62559
    44
        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@62559
    45
        "l:" -> (arg => logic = arg),
wenzelm@62559
    46
        "m:" -> (arg => modes = arg :: modes),
wenzelm@62559
    47
        "n" -> (arg => no_build = true),
wenzelm@62559
    48
        "o:" -> (arg => options = options + arg),
wenzelm@62559
    49
        "r" -> (_ => logic = "RAW_ML_SYSTEM"),
wenzelm@62559
    50
        "s" -> (_ => system_mode = true))
wenzelm@62559
    51
wenzelm@62559
    52
      val more_args = getopts(args)
wenzelm@62559
    53
      if (!more_args.isEmpty) getopts.usage()
wenzelm@62559
    54
wenzelm@62559
    55
wenzelm@62559
    56
      // build
wenzelm@62559
    57
      if (!no_build && logic != "RAW_ML_SYSTEM" &&
wenzelm@62559
    58
          Build.build(options = options, build_heap = true, no_build = true,
wenzelm@62559
    59
            dirs = dirs, system_mode = system_mode, sessions = List(logic)) != 0)
wenzelm@62559
    60
      {
wenzelm@62559
    61
        val progress = new Console_Progress
wenzelm@62559
    62
        progress.echo("Build started for Isabelle/" + logic + " ...")
wenzelm@62559
    63
        progress.interrupt_handler {
wenzelm@62559
    64
          val rc =
wenzelm@62559
    65
            Build.build(options = options, progress = progress, build_heap = true,
wenzelm@62559
    66
              dirs = dirs, system_mode = system_mode, sessions = List(logic))
wenzelm@62559
    67
          if (rc != 0) sys.exit(rc)
wenzelm@62559
    68
        }
wenzelm@62559
    69
      }
wenzelm@62559
    70
wenzelm@62559
    71
      // reader with history
wenzelm@62559
    72
      val history = new FileHistory(Path.explode("$ISABELLE_HOME_USER/console_history").file)
wenzelm@62559
    73
      val reader = new ConsoleReader
wenzelm@62559
    74
      reader.setHistory(history)
wenzelm@62559
    75
wenzelm@62559
    76
      // process loop
wenzelm@62559
    77
      val process =
wenzelm@62559
    78
        ML_Process(options, heap = logic,
wenzelm@62559
    79
          modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"))
wenzelm@62559
    80
      val process_output = Future.thread[Unit]("process_output") {
wenzelm@62559
    81
        var result = new StringBuilder(100)
wenzelm@62559
    82
        var finished = false
wenzelm@62559
    83
        while (!finished) {
wenzelm@62559
    84
          var c = -1
wenzelm@62559
    85
          var done = false
wenzelm@62559
    86
          while (!done && (result.length == 0 || process.stdout.ready)) {
wenzelm@62559
    87
            c = process.stdout.read
wenzelm@62559
    88
            if (c >= 0) result.append(c.asInstanceOf[Char])
wenzelm@62559
    89
            else done = true
wenzelm@62559
    90
          }
wenzelm@62559
    91
          if (result.length > 0) {
wenzelm@62559
    92
            System.out.print(result.toString)
wenzelm@62559
    93
            System.out.flush()
wenzelm@62559
    94
            result.length = 0
wenzelm@62559
    95
          }
wenzelm@62559
    96
          else {
wenzelm@62559
    97
            process.stdout.close()
wenzelm@62559
    98
            finished = true
wenzelm@62559
    99
          }
wenzelm@62559
   100
        }
wenzelm@62559
   101
      }
wenzelm@62559
   102
      val process_input = Future.thread[Unit]("process_input") {
wenzelm@62559
   103
        POSIX_Interrupt.handler { process.interrupt } {
wenzelm@62559
   104
          var finished = false
wenzelm@62559
   105
          while (!finished) {
wenzelm@62559
   106
            reader.readLine() match {
wenzelm@62559
   107
              case null =>
wenzelm@62559
   108
                process.stdin.close()
wenzelm@62559
   109
                finished = true
wenzelm@62559
   110
              case line =>
wenzelm@62559
   111
                process.stdin.write(line)
wenzelm@62559
   112
                process.stdin.write("\n")
wenzelm@62559
   113
                process.stdin.flush()
wenzelm@62559
   114
            }
wenzelm@62559
   115
          }
wenzelm@62559
   116
        }
wenzelm@62559
   117
      }
wenzelm@62559
   118
      val process_result = Future.thread[Int]("process_result") {
wenzelm@62559
   119
        val rc = process.join
wenzelm@62559
   120
        process_input.cancel
wenzelm@62559
   121
        rc
wenzelm@62559
   122
      }
wenzelm@62559
   123
wenzelm@62559
   124
      process_output.join
wenzelm@62559
   125
      process_input.join
wenzelm@62559
   126
wenzelm@62559
   127
      val rc = process_result.join
wenzelm@62559
   128
      history.flush()
wenzelm@62559
   129
      rc
wenzelm@62559
   130
    }
wenzelm@62559
   131
  }
wenzelm@62559
   132
}