src/Pure/ML/ml_console.scala
author wenzelm
Thu Nov 02 11:26:58 2017 +0100 (21 months ago)
changeset 66989 25665e7775b7
parent 66976 806bc39550a5
child 67802 32d76f08023f
permissions -rw-r--r--
tuned;
wenzelm@65477
     1
/*  Title:      Pure/ML/ml_console.scala
wenzelm@62559
     2
    Author:     Makarius
wenzelm@62559
     3
wenzelm@62588
     4
The raw ML process in interactive mode.
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@62643
    25
      var raw_ml_system = false
wenzelm@62559
    26
      var system_mode = false
wenzelm@62559
    27
wenzelm@62559
    28
      val getopts = Getopts("""
wenzelm@62559
    29
Usage: isabelle console [OPTIONS]
wenzelm@62559
    30
wenzelm@62559
    31
  Options are:
wenzelm@62559
    32
    -d DIR       include session directory
wenzelm@62559
    33
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
wenzelm@62559
    34
    -m MODE      add print mode for output
wenzelm@62559
    35
    -n           no build of session image on startup
wenzelm@62559
    36
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@62643
    37
    -r           bootstrap from raw Poly/ML
wenzelm@62559
    38
    -s           system build mode for session image
wenzelm@62559
    39
wenzelm@62588
    40
  Build a logic session image and run the raw Isabelle ML process
wenzelm@62588
    41
  in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
wenzelm@62588
    42
  quote(Isabelle_System.getenv("ISABELLE_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@62643
    49
        "r" -> (_ => raw_ml_system = true),
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@62643
    57
      if (!no_build && !raw_ml_system &&
wenzelm@62641
    58
          !Build.build(options = options, build_heap = true, no_build = true,
wenzelm@62641
    59
            dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
wenzelm@62559
    60
      {
wenzelm@64115
    61
        val progress = new Console_Progress()
wenzelm@62559
    62
        progress.echo("Build started for Isabelle/" + logic + " ...")
wenzelm@62559
    63
        progress.interrupt_handler {
wenzelm@62641
    64
          val res =
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@62641
    67
          if (!res.ok) sys.exit(res.rc)
wenzelm@62559
    68
        }
wenzelm@62559
    69
      }
wenzelm@62559
    70
wenzelm@62559
    71
      // process loop
wenzelm@62559
    72
      val process =
wenzelm@64598
    73
        ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
wenzelm@62643
    74
          modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
wenzelm@65431
    75
          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
wenzelm@65431
    76
          session_base =
wenzelm@65431
    77
            if (raw_ml_system) None
wenzelm@66989
    78
            else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
wenzelm@62559
    79
      val process_output = Future.thread[Unit]("process_output") {
wenzelm@62561
    80
        try {
wenzelm@62561
    81
          var result = new StringBuilder(100)
wenzelm@62561
    82
          var finished = false
wenzelm@62561
    83
          while (!finished) {
wenzelm@62561
    84
            var c = -1
wenzelm@62561
    85
            var done = false
wenzelm@62561
    86
            while (!done && (result.length == 0 || process.stdout.ready)) {
wenzelm@62561
    87
              c = process.stdout.read
wenzelm@62561
    88
              if (c >= 0) result.append(c.asInstanceOf[Char])
wenzelm@62561
    89
              else done = true
wenzelm@62561
    90
            }
wenzelm@62561
    91
            if (result.length > 0) {
wenzelm@62561
    92
              System.out.print(result.toString)
wenzelm@62561
    93
              System.out.flush()
wenzelm@62561
    94
              result.length = 0
wenzelm@62561
    95
            }
wenzelm@62561
    96
            else {
wenzelm@62561
    97
              process.stdout.close()
wenzelm@62561
    98
              finished = true
wenzelm@62561
    99
            }
wenzelm@62559
   100
          }
wenzelm@62559
   101
        }
wenzelm@62561
   102
        catch { case e: IOException => case Exn.Interrupt() => }
wenzelm@62559
   103
      }
wenzelm@62559
   104
      val process_input = Future.thread[Unit]("process_input") {
wenzelm@62562
   105
        val reader = new BufferedReader(new InputStreamReader(System.in))
wenzelm@62559
   106
        POSIX_Interrupt.handler { process.interrupt } {
wenzelm@62561
   107
          try {
wenzelm@62561
   108
            var finished = false
wenzelm@62561
   109
            while (!finished) {
wenzelm@62561
   110
              reader.readLine() match {
wenzelm@62561
   111
                case null =>
wenzelm@62561
   112
                  process.stdin.close()
wenzelm@62561
   113
                  finished = true
wenzelm@62561
   114
                case line =>
wenzelm@62561
   115
                  process.stdin.write(line)
wenzelm@62561
   116
                  process.stdin.write("\n")
wenzelm@62561
   117
                  process.stdin.flush()
wenzelm@62561
   118
              }
wenzelm@62559
   119
            }
wenzelm@62559
   120
          }
wenzelm@62561
   121
          catch { case e: IOException => case Exn.Interrupt() => }
wenzelm@62559
   122
        }
wenzelm@62559
   123
      }
wenzelm@62559
   124
      val process_result = Future.thread[Int]("process_result") {
wenzelm@62559
   125
        val rc = process.join
wenzelm@62559
   126
        process_input.cancel
wenzelm@62559
   127
        rc
wenzelm@62559
   128
      }
wenzelm@62559
   129
wenzelm@62559
   130
      process_output.join
wenzelm@62559
   131
      process_input.join
wenzelm@62562
   132
      process_result.join
wenzelm@62559
   133
    }
wenzelm@62559
   134
  }
wenzelm@62559
   135
}