src/Pure/ML/ml_console.scala
author wenzelm
Fri Mar 09 17:03:10 2018 +0100 (17 months ago)
changeset 67802 32d76f08023f
parent 66989 25665e7775b7
child 67803 1cf4126d7bd9
permissions -rw-r--r--
more general TTY loop;
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@62559
    10
object ML_Console
wenzelm@62559
    11
{
wenzelm@62559
    12
  /* command line entry point */
wenzelm@62559
    13
wenzelm@62559
    14
  def main(args: Array[String])
wenzelm@62559
    15
  {
wenzelm@62559
    16
    Command_Line.tool {
wenzelm@62559
    17
      var dirs: List[Path] = Nil
wenzelm@62559
    18
      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
wenzelm@62559
    19
      var modes: List[String] = Nil
wenzelm@62559
    20
      var no_build = false
wenzelm@62559
    21
      var options = Options.init()
wenzelm@62643
    22
      var raw_ml_system = false
wenzelm@62559
    23
      var system_mode = false
wenzelm@62559
    24
wenzelm@62559
    25
      val getopts = Getopts("""
wenzelm@62559
    26
Usage: isabelle console [OPTIONS]
wenzelm@62559
    27
wenzelm@62559
    28
  Options are:
wenzelm@62559
    29
    -d DIR       include session directory
wenzelm@62559
    30
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
wenzelm@62559
    31
    -m MODE      add print mode for output
wenzelm@62559
    32
    -n           no build of session image on startup
wenzelm@62559
    33
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@62643
    34
    -r           bootstrap from raw Poly/ML
wenzelm@62559
    35
    -s           system build mode for session image
wenzelm@62559
    36
wenzelm@62588
    37
  Build a logic session image and run the raw Isabelle ML process
wenzelm@62588
    38
  in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
wenzelm@62588
    39
  quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
wenzelm@62559
    40
""",
wenzelm@62559
    41
        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@62559
    42
        "l:" -> (arg => logic = arg),
wenzelm@62559
    43
        "m:" -> (arg => modes = arg :: modes),
wenzelm@62559
    44
        "n" -> (arg => no_build = true),
wenzelm@62559
    45
        "o:" -> (arg => options = options + arg),
wenzelm@62643
    46
        "r" -> (_ => raw_ml_system = true),
wenzelm@62559
    47
        "s" -> (_ => system_mode = true))
wenzelm@62559
    48
wenzelm@62559
    49
      val more_args = getopts(args)
wenzelm@62559
    50
      if (!more_args.isEmpty) getopts.usage()
wenzelm@62559
    51
wenzelm@62559
    52
wenzelm@62559
    53
      // build
wenzelm@62643
    54
      if (!no_build && !raw_ml_system &&
wenzelm@62641
    55
          !Build.build(options = options, build_heap = true, no_build = true,
wenzelm@62641
    56
            dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
wenzelm@62559
    57
      {
wenzelm@64115
    58
        val progress = new Console_Progress()
wenzelm@62559
    59
        progress.echo("Build started for Isabelle/" + logic + " ...")
wenzelm@62559
    60
        progress.interrupt_handler {
wenzelm@62641
    61
          val res =
wenzelm@62559
    62
            Build.build(options = options, progress = progress, build_heap = true,
wenzelm@62559
    63
              dirs = dirs, system_mode = system_mode, sessions = List(logic))
wenzelm@62641
    64
          if (!res.ok) sys.exit(res.rc)
wenzelm@62559
    65
        }
wenzelm@62559
    66
      }
wenzelm@62559
    67
wenzelm@62559
    68
      // process loop
wenzelm@62559
    69
      val process =
wenzelm@64598
    70
        ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
wenzelm@62643
    71
          modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
wenzelm@65431
    72
          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
wenzelm@65431
    73
          session_base =
wenzelm@65431
    74
            if (raw_ml_system) None
wenzelm@66989
    75
            else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
wenzelm@67802
    76
wenzelm@67802
    77
      val tty_loop = new TTY_Loop(process.stdin, process.stdout, process.interrupt _)
wenzelm@62559
    78
      val process_result = Future.thread[Int]("process_result") {
wenzelm@62559
    79
        val rc = process.join
wenzelm@67802
    80
        tty_loop.cancel
wenzelm@62559
    81
        rc
wenzelm@62559
    82
      }
wenzelm@67802
    83
      tty_loop.join
wenzelm@62562
    84
      process_result.join
wenzelm@62559
    85
    }
wenzelm@62559
    86
  }
wenzelm@62559
    87
}