20 var dirs: List[Path] = Nil |
20 var dirs: List[Path] = Nil |
21 var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
21 var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
22 var modes: List[String] = Nil |
22 var modes: List[String] = Nil |
23 var no_build = false |
23 var no_build = false |
24 var options = Options.init() |
24 var options = Options.init() |
|
25 var raw_ml_system = false |
25 var system_mode = false |
26 var system_mode = false |
26 |
27 |
27 val getopts = Getopts(""" |
28 val getopts = Getopts(""" |
28 Usage: isabelle console [OPTIONS] |
29 Usage: isabelle console [OPTIONS] |
29 |
30 |
31 -d DIR include session directory |
32 -d DIR include session directory |
32 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
33 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
33 -m MODE add print mode for output |
34 -m MODE add print mode for output |
34 -n no build of session image on startup |
35 -n no build of session image on startup |
35 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
36 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
36 -r logic session is "RAW_ML_SYSTEM" |
37 -r bootstrap from raw Poly/ML |
37 -s system build mode for session image |
38 -s system build mode for session image |
38 |
39 |
39 Build a logic session image and run the raw Isabelle ML process |
40 Build a logic session image and run the raw Isabelle ML process |
40 in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" + |
41 in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" + |
41 quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """. |
42 quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """. |
43 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
44 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
44 "l:" -> (arg => logic = arg), |
45 "l:" -> (arg => logic = arg), |
45 "m:" -> (arg => modes = arg :: modes), |
46 "m:" -> (arg => modes = arg :: modes), |
46 "n" -> (arg => no_build = true), |
47 "n" -> (arg => no_build = true), |
47 "o:" -> (arg => options = options + arg), |
48 "o:" -> (arg => options = options + arg), |
48 "r" -> (_ => logic = "RAW_ML_SYSTEM"), |
49 "r" -> (_ => raw_ml_system = true), |
49 "s" -> (_ => system_mode = true)) |
50 "s" -> (_ => system_mode = true)) |
50 |
51 |
51 val more_args = getopts(args) |
52 val more_args = getopts(args) |
52 if (!more_args.isEmpty) getopts.usage() |
53 if (!more_args.isEmpty) getopts.usage() |
53 |
54 |
54 |
55 |
55 // build |
56 // build |
56 if (!no_build && logic != "RAW_ML_SYSTEM" && |
57 if (!no_build && !raw_ml_system && |
57 !Build.build(options = options, build_heap = true, no_build = true, |
58 !Build.build(options = options, build_heap = true, no_build = true, |
58 dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok) |
59 dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok) |
59 { |
60 { |
60 val progress = new Console_Progress |
61 val progress = new Console_Progress |
61 progress.echo("Build started for Isabelle/" + logic + " ...") |
62 progress.echo("Build started for Isabelle/" + logic + " ...") |
68 } |
69 } |
69 |
70 |
70 // process loop |
71 // process loop |
71 val process = |
72 val process = |
72 ML_Process(options, logic = logic, args = List("-i"), |
73 ML_Process(options, logic = logic, args = List("-i"), |
73 modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"), |
74 modes = if (raw_ml_system) Nil else modes ::: List("ASCII"), |
74 store = Sessions.store(system_mode)) |
75 raw_ml_system = raw_ml_system, store = Sessions.store(system_mode)) |
75 val process_output = Future.thread[Unit]("process_output") { |
76 val process_output = Future.thread[Unit]("process_output") { |
76 try { |
77 try { |
77 var result = new StringBuilder(100) |
78 var result = new StringBuilder(100) |
78 var finished = false |
79 var finished = false |
79 while (!finished) { |
80 while (!finished) { |