equal
deleted
inserted
replaced
92 def open_session( |
92 def open_session( |
93 options: Options, |
93 options: Options, |
94 host: String, |
94 host: String, |
95 port: Int = 0, |
95 port: Int = 0, |
96 user: String = "", |
96 user: String = "", |
97 actual_host: String = "", |
|
98 multiplex: Boolean = !Platform.is_windows |
97 multiplex: Boolean = !Platform.is_windows |
99 ): Session = { |
98 ): Session = { |
100 val session_host = proper_string(actual_host) getOrElse host |
|
101 val session_port = make_port(port) |
|
102 |
|
103 val (control_master, control_path) = |
99 val (control_master, control_path) = |
104 if (multiplex) { |
100 if (multiplex) { |
105 val file = Isabelle_System.tmp_file("ssh_socket") |
101 val file = Isabelle_System.tmp_file("ssh_socket") |
106 file.delete() |
102 file.delete() |
107 (true, file.getPath) |
103 (true, file.getPath) |
108 } |
104 } |
109 else (false, "") |
105 else (false, "") |
110 |
106 |
111 new Session(options, session_host, session_port, user, control_master, control_path) |
107 new Session(options, host, make_port(port), user, control_master, control_path) |
112 } |
108 } |
113 |
109 |
114 class Session private[SSH]( |
110 class Session private[SSH]( |
115 val options: Options, |
111 val options: Options, |
116 val host: String, |
112 val host: String, |