1/*  Title:      Pure/ML/ml_console.scala
2    Author:     Makarius
3
4The raw ML process in interactive mode.
5*/
6
7package isabelle
8
9
10object ML_Console
11{
12  /* command line entry point */
13
14  def main(args: Array[String])
15  {
16    Command_Line.tool {
17      var dirs: List[Path] = Nil
18      var include_sessions: List[String] = Nil
19      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
20      var modes: List[String] = Nil
21      var no_build = false
22      var options = Options.init()
23      var raw_ml_system = false
24
25      val getopts = Getopts("""
26Usage: isabelle console [OPTIONS]
27
28  Options are:
29    -d DIR       include session directory
30    -i NAME      include session in name-space of theories
31    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
32    -m MODE      add print mode for output
33    -n           no build of session image on startup
34    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
35    -r           bootstrap from raw Poly/ML
36
37  Build a logic session image and run the raw Isabelle ML process
38  in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
39  quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
40""",
41        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
42        "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
43        "l:" -> (arg => logic = arg),
44        "m:" -> (arg => modes = arg :: modes),
45        "n" -> (arg => no_build = true),
46        "o:" -> (arg => options = options + arg),
47        "r" -> (_ => raw_ml_system = true))
48
49      val more_args = getopts(args)
50      if (more_args.nonEmpty) getopts.usage()
51
52
53      // build logic
54      if (!no_build && !raw_ml_system) {
55        val progress = new Console_Progress()
56        val rc =
57          progress.interrupt_handler {
58            Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs)
59          }
60        if (rc != 0) sys.exit(rc)
61      }
62
63      // process loop
64      val process =
65        ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
66          modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
67          raw_ml_system = raw_ml_system,
68          store = Some(Sessions.store(options)),
69          session_base =
70            if (raw_ml_system) None
71            else Some(Sessions.base_info(
72              options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
73
74      val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _))
75      val process_result = Future.thread[Int]("process_result") {
76        val rc = process.join
77        tty_loop.cancel  // FIXME does not quite work, cannot interrupt blocking read on System.in
78        rc
79      }
80      tty_loop.join
81      process_result.join
82    }
83  }
84}
85