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