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      var system_mode = false
25
26      val getopts = Getopts("""
27Usage: isabelle console [OPTIONS]
28
29  Options are:
30    -d DIR       include session directory
31    -i NAME      include session in name-space of theories
32    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
33    -m MODE      add print mode for output
34    -n           no build of session image on startup
35    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
36    -r           bootstrap from raw Poly/ML
37    -s           system build mode for session image
38
39  Build a logic session image and run the raw Isabelle ML process
40  in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
41  quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
42""",
43        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
44        "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
45        "l:" -> (arg => logic = arg),
46        "m:" -> (arg => modes = arg :: modes),
47        "n" -> (arg => no_build = true),
48        "o:" -> (arg => options = options + arg),
49        "r" -> (_ => raw_ml_system = true),
50        "s" -> (_ => system_mode = true))
51
52      val more_args = getopts(args)
53      if (!more_args.isEmpty) getopts.usage()
54
55
56      // build logic
57      if (!no_build && !raw_ml_system) {
58        val progress = new Console_Progress()
59        val rc =
60          progress.interrupt_handler {
61            Build.build_logic(options, logic, build_heap = true, progress = progress,
62              dirs = dirs, system_mode = system_mode)
63          }
64        if (rc != 0) sys.exit(rc)
65      }
66
67      // process loop
68      val process =
69        ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
70          modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
71          raw_ml_system = raw_ml_system,
72          store = Some(Sessions.store(options, system_mode)),
73          session_base =
74            if (raw_ml_system) None
75            else Some(Sessions.base_info(
76              options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
77
78      val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _))
79      val process_result = Future.thread[Int]("process_result") {
80        val rc = process.join
81        tty_loop.cancel  // FIXME does not quite work, cannot interrupt blocking read on System.in
82        rc
83      }
84      tty_loop.join
85      process_result.join
86    }
87  }
88}
89