equal
deleted
inserted
replaced
13 heap: String = "", |
13 heap: String = "", |
14 args: List[String] = Nil, |
14 args: List[String] = Nil, |
15 modes: List[String] = Nil, |
15 modes: List[String] = Nil, |
16 secure: Boolean = false, |
16 secure: Boolean = false, |
17 redirect: Boolean = false, |
17 redirect: Boolean = false, |
18 process_socket: String = ""): Bash.Process = |
18 channel: Option[System_Channel] = None): Bash.Process = |
19 { |
19 { |
20 val load_heaps = |
20 val load_heaps = |
21 { |
21 { |
22 if (heap == "RAW_ML_SYSTEM") Nil |
22 if (heap == "RAW_ML_SYSTEM") Nil |
23 else if (heap.iterator.contains('/')) { |
23 else if (heap.iterator.contains('/')) { |
70 val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()") |
70 val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()") |
71 |
71 |
72 val eval_secure = if (secure) List("Secure.set_secure ()") else Nil |
72 val eval_secure = if (secure) List("Secure.set_secure ()") else Nil |
73 |
73 |
74 val eval_process = |
74 val eval_process = |
75 if (process_socket == "") List("Isabelle_Process.init_options ()") |
75 channel match { |
76 else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket)) |
76 case None => List("Isabelle_Process.init_options ()") |
|
77 case Some(ch) => |
|
78 List("Isabelle_Process.init_protocol " + ML_Syntax.print_string_raw(ch.server_name)) |
|
79 } |
77 |
80 |
78 // bash |
81 // bash |
79 val bash_args = |
82 val bash_args = |
80 Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
83 Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
81 (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process). |
84 (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process). |