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