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