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