| author | wenzelm |
| Sun, 21 Aug 2022 13:12:25 +0200 | |
| changeset 75947 | 45f08f13354a |
| parent 75548 | 0af8a0b6216a |
| child 76100 | 758fd2fbde1e |
| permissions | -rw-r--r-- |
| 64123 | 1 |
/* Title: Pure/General/ssh.scala |
2 |
Author: Makarius |
|
3 |
||
| 64124 | 4 |
SSH client based on JSch (see also http://www.jcraft.com/jsch/examples). |
| 64123 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
| 73909 | 10 |
import java.util.{Map => JMap}
|
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
11 |
import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
|
| 64131 | 12 |
|
| 71358 | 13 |
import scala.collection.mutable |
| 71601 | 14 |
import scala.util.matching.Regex |
| 64131 | 15 |
|
| 64222 | 16 |
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
|
| 75548 | 17 |
OpenSSHConfig, UserInfo, ChannelExec, ChannelSftp, SftpATTRS, JSchException} |
| 64123 | 18 |
|
19 |
||
| 75393 | 20 |
object SSH {
|
| 64185 | 21 |
/* target machine: user@host syntax */ |
| 64141 | 22 |
|
| 75393 | 23 |
object Target {
|
| 71601 | 24 |
val User_Host: Regex = "^([^@]+)@(.+)$".r |
| 64141 | 25 |
|
26 |
def parse(s: String): (String, String) = |
|
27 |
s match {
|
|
| 71307 | 28 |
case User_Host(user, host) => (user, host) |
| 64141 | 29 |
case _ => ("", s)
|
30 |
} |
|
31 |
||
32 |
def unapplySeq(s: String): Option[List[String]] = |
|
| 64185 | 33 |
parse(s) match {
|
34 |
case (_, "") => None |
|
35 |
case (user, host) => Some(List(user, host)) |
|
36 |
} |
|
| 64141 | 37 |
} |
38 |
||
| 64142 | 39 |
val default_port = 22 |
|
67745
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
40 |
def make_port(port: Int): Int = if (port > 0) port else default_port |
| 64142 | 41 |
|
| 75500 | 42 |
def port_suffix(port: Int): String = |
43 |
if (port == default_port) "" else ":" + port |
|
| 71549 | 44 |
|
45 |
def user_prefix(user: String): String = |
|
46 |
proper_string(user) match {
|
|
47 |
case None => "" |
|
48 |
case Some(name) => name + "@" |
|
49 |
} |
|
50 |
||
| 64257 | 51 |
def connect_timeout(options: Options): Int = |
52 |
options.seconds("ssh_connect_timeout").ms.toInt
|
|
| 64141 | 53 |
|
| 64325 | 54 |
def alive_interval(options: Options): Int = |
55 |
options.seconds("ssh_alive_interval").ms.toInt
|
|
56 |
||
|
67273
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents:
67067
diff
changeset
|
57 |
def alive_count_max(options: Options): Int = |
|
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents:
67067
diff
changeset
|
58 |
options.int("ssh_alive_count_max")
|
|
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents:
67067
diff
changeset
|
59 |
|
| 64123 | 60 |
|
| 64257 | 61 |
/* init context */ |
62 |
||
| 75393 | 63 |
def init_context(options: Options): Context = {
|
| 64130 | 64 |
val config_dir = Path.explode(options.string("ssh_config_dir"))
|
| 64123 | 65 |
if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
|
66 |
||
67 |
val jsch = new JSch |
|
68 |
||
| 64130 | 69 |
val config_file = Path.explode(options.string("ssh_config_file"))
|
| 64123 | 70 |
if (config_file.is_file) |
71 |
jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file))) |
|
72 |
||
73 |
val known_hosts = config_dir + Path.explode("known_hosts")
|
|
74 |
if (!known_hosts.is_file) known_hosts.file.createNewFile |
|
75 |
jsch.setKnownHosts(File.platform_path(known_hosts)) |
|
76 |
||
| 64130 | 77 |
val identity_files = |
| 71601 | 78 |
space_explode(':', options.string("ssh_identity_files")).map(Path.explode)
|
| 71780 | 79 |
for (identity_file <- identity_files if identity_file.is_file) {
|
80 |
try { jsch.addIdentity(File.platform_path(identity_file)) }
|
|
81 |
catch {
|
|
82 |
case exn: JSchException => |
|
83 |
error("Error in ssh identity file " + identity_file + ": " + exn.getMessage)
|
|
84 |
} |
|
85 |
} |
|
| 64123 | 86 |
|
| 64257 | 87 |
new Context(options, jsch) |
| 64123 | 88 |
} |
89 |
||
|
71564
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
wenzelm
parents:
71562
diff
changeset
|
90 |
def open_session(options: Options, |
|
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
wenzelm
parents:
71562
diff
changeset
|
91 |
host: String, user: String = "", port: Int = 0, actual_host: String = "", |
| 67771 | 92 |
proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, |
93 |
permissive: Boolean = false): Session = |
|
|
71564
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
wenzelm
parents:
71562
diff
changeset
|
94 |
init_context(options).open_session( |
|
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
wenzelm
parents:
71562
diff
changeset
|
95 |
host = host, user = user, port = port, actual_host = actual_host, |
| 67771 | 96 |
proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, |
97 |
permissive = permissive) |
|
| 67067 | 98 |
|
| 75393 | 99 |
class Context private[SSH](val options: Options, val jsch: JSch) {
|
| 64257 | 100 |
def update_options(new_options: Options): Context = new Context(new_options, jsch) |
101 |
||
| 75393 | 102 |
private def connect_session( |
103 |
host: String, |
|
104 |
user: String = "", |
|
105 |
port: Int = 0, |
|
| 75547 | 106 |
permissive: Boolean = false, |
| 71549 | 107 |
nominal_host: String = "", |
108 |
nominal_user: String = "", |
|
|
75545
218dd201e24d
clarified types -- proper default_port via make_port;
wenzelm
parents:
75544
diff
changeset
|
109 |
nominal_port: Option[Int] = None, |
| 75393 | 110 |
on_close: () => Unit = () => () |
111 |
): Session = {
|
|
| 75547 | 112 |
val connect_port = make_port(port) |
113 |
val session = jsch.getSession(proper_string(user).orNull, host, connect_port) |
|
| 64257 | 114 |
|
115 |
session.setUserInfo(No_User_Info) |
|
| 64325 | 116 |
session.setServerAliveInterval(alive_interval(options)) |
|
67273
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents:
67067
diff
changeset
|
117 |
session.setServerAliveCountMax(alive_count_max(options)) |
| 64257 | 118 |
session.setConfig("MaxAuthTries", "3")
|
| 75547 | 119 |
if (permissive) session.setConfig("StrictHostKeyChecking", "no")
|
| 71549 | 120 |
if (nominal_host != "") session.setHostKeyAlias(nominal_host) |
| 64257 | 121 |
|
122 |
if (options.bool("ssh_compression")) {
|
|
123 |
session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
|
|
124 |
session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
|
|
125 |
session.setConfig("compression_level", "9")
|
|
126 |
} |
|
|
67745
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
127 |
session.connect(connect_timeout(options)) |
| 71549 | 128 |
new Session(options, session, on_close, |
129 |
proper_string(nominal_host) getOrElse host, |
|
|
75544
179a3b028b0a
proper nominal_port, notably for port forwarding;
wenzelm
parents:
75517
diff
changeset
|
130 |
proper_string(nominal_user) getOrElse user, |
| 75547 | 131 |
nominal_port getOrElse connect_port) |
|
67745
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
132 |
} |
| 64257 | 133 |
|
|
71564
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
wenzelm
parents:
71562
diff
changeset
|
134 |
def open_session( |
| 75393 | 135 |
host: String, |
136 |
user: String = "", |
|
137 |
port: Int = 0, |
|
138 |
actual_host: String = "", |
|
139 |
proxy_host: String = "", |
|
140 |
proxy_user: String = "", |
|
141 |
proxy_port: Int = 0, |
|
142 |
permissive: Boolean = false |
|
143 |
): Session = {
|
|
|
71564
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
wenzelm
parents:
71562
diff
changeset
|
144 |
val connect_host = proper_string(actual_host) getOrElse host |
| 75547 | 145 |
val connect_port = make_port(port) |
146 |
if (proxy_host == "") connect_session(host = connect_host, user = user, port = connect_port) |
|
|
67745
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
147 |
else {
|
|
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
148 |
val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user) |
|
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
149 |
|
|
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
150 |
val fw = |
| 75547 | 151 |
try { proxy.port_forwarding(remote_host = connect_host, remote_port = connect_port) }
|
| 73367 | 152 |
catch { case exn: Throwable => proxy.close(); throw exn }
|
|
67745
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
153 |
|
|
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
154 |
try {
|
| 75547 | 155 |
connect_session( |
156 |
host = fw.local_host, |
|
157 |
port = fw.local_port, |
|
158 |
permissive = permissive, |
|
|
75545
218dd201e24d
clarified types -- proper default_port via make_port;
wenzelm
parents:
75544
diff
changeset
|
159 |
nominal_host = host, |
| 75547 | 160 |
nominal_port = Some(connect_port), |
| 75546 | 161 |
nominal_user = user, user = user, |
| 75394 | 162 |
on_close = { () => fw.close(); proxy.close() })
|
|
67745
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
163 |
} |
| 73367 | 164 |
catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
|
|
67745
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
165 |
} |
| 64257 | 166 |
} |
167 |
} |
|
| 64130 | 168 |
|
| 64123 | 169 |
|
170 |
/* logging */ |
|
171 |
||
| 75393 | 172 |
def logging(verbose: Boolean = true, debug: Boolean = false): Unit = {
|
| 64123 | 173 |
JSch.setLogger(if (verbose) new Logger(debug) else null) |
174 |
} |
|
175 |
||
| 75393 | 176 |
private class Logger(debug: Boolean) extends JSch_Logger {
|
| 64123 | 177 |
def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug |
178 |
||
| 75393 | 179 |
def log(level: Int, msg: String): Unit = {
|
| 64123 | 180 |
level match {
|
181 |
case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) |
|
182 |
case JSch_Logger.WARN => Output.warning(msg) |
|
183 |
case _ => Output.writeln(msg) |
|
184 |
} |
|
185 |
} |
|
186 |
} |
|
187 |
||
188 |
||
| 64128 | 189 |
/* user info */ |
190 |
||
| 75393 | 191 |
object No_User_Info extends UserInfo {
|
| 64128 | 192 |
def getPassphrase: String = null |
193 |
def getPassword: String = null |
|
194 |
def promptPassword(msg: String): Boolean = false |
|
195 |
def promptPassphrase(msg: String): Boolean = false |
|
196 |
def promptYesNo(msg: String): Boolean = false |
|
197 |
def showMessage(msg: String): Unit = Output.writeln(msg) |
|
198 |
} |
|
199 |
||
200 |
||
| 65009 | 201 |
/* port forwarding */ |
202 |
||
| 75393 | 203 |
object Port_Forwarding {
|
204 |
def open( |
|
205 |
ssh: Session, |
|
206 |
ssh_close: Boolean, |
|
207 |
local_host: String, |
|
208 |
local_port: Int, |
|
209 |
remote_host: String, |
|
210 |
remote_port: Int |
|
211 |
): Port_Forwarding = {
|
|
| 65010 | 212 |
val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port) |
|
65636
df804cdba5f9
ssh_close for proper termination after use of database;
wenzelm
parents:
65594
diff
changeset
|
213 |
new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port) |
| 65010 | 214 |
} |
215 |
} |
|
216 |
||
217 |
class Port_Forwarding private[SSH]( |
|
218 |
ssh: SSH.Session, |
|
|
65636
df804cdba5f9
ssh_close for proper termination after use of database;
wenzelm
parents:
65594
diff
changeset
|
219 |
ssh_close: Boolean, |
| 65010 | 220 |
val local_host: String, |
221 |
val local_port: Int, |
|
222 |
val remote_host: String, |
|
| 75393 | 223 |
val remote_port: Int |
224 |
) extends AutoCloseable {
|
|
| 65010 | 225 |
override def toString: String = |
226 |
local_host + ":" + local_port + ":" + remote_host + ":" + remote_port |
|
227 |
||
| 75393 | 228 |
def close(): Unit = {
|
|
65636
df804cdba5f9
ssh_close for proper termination after use of database;
wenzelm
parents:
65594
diff
changeset
|
229 |
ssh.session.delPortForwardingL(local_host, local_port) |
|
df804cdba5f9
ssh_close for proper termination after use of database;
wenzelm
parents:
65594
diff
changeset
|
230 |
if (ssh_close) ssh.close() |
|
df804cdba5f9
ssh_close for proper termination after use of database;
wenzelm
parents:
65594
diff
changeset
|
231 |
} |
| 65009 | 232 |
} |
233 |
||
234 |
||
| 64191 | 235 |
/* Sftp channel */ |
236 |
||
237 |
type Attrs = SftpATTRS |
|
238 |
||
| 75393 | 239 |
sealed case class Dir_Entry(name: String, is_dir: Boolean) {
|
|
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
67771
diff
changeset
|
240 |
def is_file: Boolean = !is_dir |
| 64191 | 241 |
} |
242 |
||
243 |
||
| 64132 | 244 |
/* exec channel */ |
245 |
||
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
246 |
private val exec_wait_delay = Time.seconds(0.3) |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
247 |
|
| 75393 | 248 |
class Exec private[SSH](session: Session, channel: ChannelExec) extends AutoCloseable {
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
249 |
override def toString: String = "exec " + session.toString |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
250 |
|
| 75548 | 251 |
def close(): Unit = channel.disconnect() |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
252 |
|
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
253 |
val exit_status: Future[Int] = |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
254 |
Future.thread("ssh_wait") {
|
|
73702
7202e12cb324
tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents:
73634
diff
changeset
|
255 |
while (!channel.isClosed) exec_wait_delay.sleep() |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
256 |
channel.getExitStatus |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
257 |
} |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
258 |
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
259 |
val stdin: OutputStream = channel.getOutputStream |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
260 |
val stdout: InputStream = channel.getInputStream |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
261 |
val stderr: InputStream = channel.getErrStream |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
262 |
|
| 64166 | 263 |
// connect after preparing streams |
264 |
channel.connect(connect_timeout(session.options)) |
|
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
265 |
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
266 |
def result( |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
267 |
progress_stdout: String => Unit = (_: String) => (), |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
268 |
progress_stderr: String => Unit = (_: String) => (), |
| 75393 | 269 |
strict: Boolean = true |
270 |
): Process_Result = {
|
|
| 73367 | 271 |
stdin.close() |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
272 |
|
| 75393 | 273 |
def read_lines(stream: InputStream, progress: String => Unit): List[String] = {
|
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
274 |
val result = new mutable.ListBuffer[String] |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
275 |
val line_buffer = new ByteArrayOutputStream(100) |
| 75393 | 276 |
def line_flush(): Unit = {
|
| 64326 | 277 |
val line = Library.trim_line(line_buffer.toString(UTF8.charset_name)) |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
278 |
progress(line) |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
279 |
result += line |
| 75548 | 280 |
line_buffer.reset() |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
281 |
} |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
282 |
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
283 |
var c = 0 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
284 |
var finished = false |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
285 |
while (!finished) {
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
286 |
while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c)
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
287 |
if (c == 10) line_flush() |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
288 |
else if (channel.isClosed) {
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
289 |
if (line_buffer.size > 0) line_flush() |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
290 |
finished = true |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
291 |
} |
|
73702
7202e12cb324
tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents:
73634
diff
changeset
|
292 |
else exec_wait_delay.sleep() |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
293 |
} |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
294 |
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
295 |
result.toList |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
296 |
} |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
297 |
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
298 |
val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) }
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
299 |
val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) }
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
300 |
|
| 75393 | 301 |
def terminate(): Unit = {
|
| 73367 | 302 |
close() |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
303 |
out_lines.join |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
304 |
err_lines.join |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
305 |
exit_status.join |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
306 |
} |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
307 |
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
308 |
val rc = |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
309 |
try { exit_status.join }
|
| 74306 | 310 |
catch { case Exn.Interrupt() => terminate(); Process_Result.RC.interrupt }
|
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
311 |
|
| 73367 | 312 |
close() |
| 74306 | 313 |
if (strict && rc == Process_Result.RC.interrupt) throw Exn.Interrupt() |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
314 |
|
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
315 |
Process_Result(rc, out_lines.join, err_lines.join) |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
316 |
} |
| 64131 | 317 |
} |
318 |
||
319 |
||
| 64123 | 320 |
/* session */ |
321 |
||
|
67745
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
322 |
class Session private[SSH]( |
|
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
323 |
val options: Options, |
|
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
324 |
val session: JSch_Session, |
| 71549 | 325 |
on_close: () => Unit, |
326 |
val nominal_host: String, |
|
|
75544
179a3b028b0a
proper nominal_port, notably for port forwarding;
wenzelm
parents:
75517
diff
changeset
|
327 |
val nominal_user: String, |
|
179a3b028b0a
proper nominal_port, notably for port forwarding;
wenzelm
parents:
75517
diff
changeset
|
328 |
val nominal_port: Int |
| 75393 | 329 |
) extends System {
|
|
67745
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents:
67273
diff
changeset
|
330 |
def update_options(new_options: Options): Session = |
|
75544
179a3b028b0a
proper nominal_port, notably for port forwarding;
wenzelm
parents:
75517
diff
changeset
|
331 |
new Session(new_options, session, on_close, nominal_host, nominal_user, nominal_port) |
| 64166 | 332 |
|
| 64347 | 333 |
def host: String = if (session.getHost == null) "" else session.getHost |
| 71549 | 334 |
|
335 |
override def hg_url: String = |
|
336 |
"ssh://" + user_prefix(nominal_user) + nominal_host + "/" |
|
| 66570 | 337 |
|
| 75500 | 338 |
override def rsync_prefix: String = |
339 |
user_prefix(nominal_user) + nominal_host + ":" |
|
340 |
||
| 64123 | 341 |
override def toString: String = |
|
75544
179a3b028b0a
proper nominal_port, notably for port forwarding;
wenzelm
parents:
75517
diff
changeset
|
342 |
user_prefix(session.getUserName) + host + port_suffix(session.getPort) + |
| 71549 | 343 |
(if (session.isConnected) "" else " (disconnected)") |
| 64123 | 344 |
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
345 |
|
| 65009 | 346 |
/* port forwarding */ |
347 |
||
|
65636
df804cdba5f9
ssh_close for proper termination after use of database;
wenzelm
parents:
65594
diff
changeset
|
348 |
def port_forwarding( |
|
df804cdba5f9
ssh_close for proper termination after use of database;
wenzelm
parents:
65594
diff
changeset
|
349 |
remote_port: Int, remote_host: String = "localhost", |
|
df804cdba5f9
ssh_close for proper termination after use of database;
wenzelm
parents:
65594
diff
changeset
|
350 |
local_port: Int = 0, local_host: String = "localhost", |
|
df804cdba5f9
ssh_close for proper termination after use of database;
wenzelm
parents:
65594
diff
changeset
|
351 |
ssh_close: Boolean = false): Port_Forwarding = |
|
df804cdba5f9
ssh_close for proper termination after use of database;
wenzelm
parents:
65594
diff
changeset
|
352 |
Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port) |
| 65009 | 353 |
|
354 |
||
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
355 |
/* sftp channel */ |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
356 |
|
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
357 |
val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
|
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
358 |
sftp.connect(connect_timeout(options)) |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
359 |
|
| 75548 | 360 |
override def close(): Unit = { sftp.disconnect(); session.disconnect(); on_close() }
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
361 |
|
| 75393 | 362 |
val settings: JMap[String, String] = {
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
363 |
val home = sftp.getHome |
| 73897 | 364 |
JMap.of("HOME", home, "USER_HOME", home)
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
365 |
} |
| 66570 | 366 |
override def expand_path(path: Path): Path = path.expand_env(settings) |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
367 |
def remote_path(path: Path): String = expand_path(path).implode |
| 67066 | 368 |
override def bash_path(path: Path): String = Bash.string(remote_path(path)) |
| 64123 | 369 |
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
370 |
def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path)) |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
371 |
def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2)) |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
372 |
def rm(path: Path): Unit = sftp.rm(remote_path(path)) |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
373 |
def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path)) |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
374 |
def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path)) |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
375 |
|
| 69302 | 376 |
private def test_entry(path: Path, as_dir: Boolean): Boolean = |
377 |
try {
|
|
378 |
val is_dir = sftp.stat(remote_path(path)).isDir |
|
379 |
if (as_dir) is_dir else !is_dir |
|
380 |
} |
|
381 |
catch { case _: SftpException => false }
|
|
|
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
67771
diff
changeset
|
382 |
|
| 69302 | 383 |
override def is_dir(path: Path): Boolean = test_entry(path, true) |
384 |
override def is_file(path: Path): Boolean = test_entry(path, false) |
|
|
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
67771
diff
changeset
|
385 |
|
| 69301 | 386 |
def is_link(path: Path): Boolean = |
387 |
try { sftp.lstat(remote_path(path)).isLink }
|
|
388 |
catch { case _: SftpException => false }
|
|
389 |
||
| 75393 | 390 |
override def make_directory(path: Path): Path = {
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
391 |
if (!is_dir(path)) {
|
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
392 |
execute( |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
393 |
"perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
|
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
394 |
if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path)))
|
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
395 |
} |
| 72376 | 396 |
path |
397 |
} |
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
398 |
|
| 75393 | 399 |
def read_dir(path: Path): List[Dir_Entry] = {
|
|
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
67771
diff
changeset
|
400 |
if (!is_dir(path)) error("No such directory: " + path.toString)
|
|
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
67771
diff
changeset
|
401 |
|
|
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
67771
diff
changeset
|
402 |
val dir_name = remote_path(path) |
|
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
67771
diff
changeset
|
403 |
val dir = sftp.ls(dir_name) |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
404 |
(for {
|
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
405 |
i <- (0 until dir.size).iterator |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
406 |
a = dir.get(i).asInstanceOf[AnyRef] |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
407 |
name = Untyped.get[String](a, "filename") |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
408 |
attrs = Untyped.get[Attrs](a, "attrs") |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
409 |
if name != "." && name != ".." |
| 69302 | 410 |
} |
411 |
yield {
|
|
412 |
Dir_Entry(name, |
|
413 |
if (attrs.isLink) {
|
|
414 |
try { sftp.stat(dir_name + "/" + name).isDir }
|
|
415 |
catch { case _: SftpException => false }
|
|
416 |
} |
|
417 |
else attrs.isDir) |
|
|
69427
ff2f39a221d4
clarified operations: uniform sorting of results;
wenzelm
parents:
69393
diff
changeset
|
418 |
}).toList.sortBy(_.name) |
| 64191 | 419 |
} |
|
64135
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents:
64134
diff
changeset
|
420 |
|
| 69301 | 421 |
def find_files( |
422 |
start: Path, |
|
423 |
pred: Path => Boolean = _ => true, |
|
424 |
include_dirs: Boolean = false, |
|
| 75393 | 425 |
follow_links: Boolean = false |
426 |
): List[Path] = {
|
|
| 69301 | 427 |
val result = new mutable.ListBuffer[Path] |
| 73340 | 428 |
def check(path: Path): Unit = { if (pred(path)) result += path }
|
| 69301 | 429 |
|
| 75393 | 430 |
def find(dir: Path): Unit = {
|
| 69303 | 431 |
if (include_dirs) check(dir) |
| 69301 | 432 |
if (follow_links || !is_link(dir)) {
|
433 |
for (entry <- read_dir(dir)) {
|
|
| 69302 | 434 |
val path = dir + Path.basic(entry.name) |
435 |
if (entry.is_file) check(path) else find(path) |
|
| 69301 | 436 |
} |
437 |
} |
|
438 |
} |
|
439 |
if (is_file(start)) check(start) else find(start) |
|
440 |
||
441 |
result.toList |
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
442 |
} |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
443 |
|
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
444 |
def open_input(path: Path): InputStream = sftp.get(remote_path(path)) |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
445 |
def open_output(path: Path): OutputStream = sftp.put(remote_path(path)) |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
446 |
|
| 73634 | 447 |
override def read_file(path: Path, local_path: Path): Unit = |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
448 |
sftp.get(remote_path(path), File.platform_path(local_path)) |
| 75513 | 449 |
override def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_)) |
450 |
override def read(path: Path): String = using(open_input(path))(File.read_stream) |
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
451 |
|
| 73634 | 452 |
override def write_file(path: Path, local_path: Path): Unit = |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
453 |
sftp.put(File.platform_path(local_path), remote_path(path)) |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
454 |
def write_bytes(path: Path, bytes: Bytes): Unit = |
| 71601 | 455 |
using(open_output(path))(bytes.write_stream) |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
456 |
def write(path: Path, text: String): Unit = |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
457 |
using(open_output(path))(stream => Bytes(text).write_stream(stream)) |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
458 |
|
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
459 |
|
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
460 |
/* exec channel */ |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
461 |
|
| 75393 | 462 |
def exec(command: String): Exec = {
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
463 |
val channel = session.openChannel("exec").asInstanceOf[ChannelExec]
|
|
64190
c62b99e3ec07
provide USER_HOME, such that symbolic Path.explode("~") can be used remotely;
wenzelm
parents:
64185
diff
changeset
|
464 |
channel.setCommand("export USER_HOME=\"$HOME\"\n" + command)
|
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
465 |
new Exec(this, channel) |
| 64129 | 466 |
} |
| 64123 | 467 |
|
| 66570 | 468 |
override def execute(command: String, |
| 64191 | 469 |
progress_stdout: String => Unit = (_: String) => (), |
470 |
progress_stderr: String => Unit = (_: String) => (), |
|
| 73634 | 471 |
settings: Boolean = true, |
| 64191 | 472 |
strict: Boolean = true): Process_Result = |
473 |
exec(command).result(progress_stdout, progress_stderr, strict) |
|
| 64137 | 474 |
|
| 72340 | 475 |
override def isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(this)) |
| 72338 | 476 |
|
| 64137 | 477 |
|
478 |
/* tmp dirs */ |
|
479 |
||
|
64306
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
wenzelm
parents:
64304
diff
changeset
|
480 |
def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) |
|
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
wenzelm
parents:
64304
diff
changeset
|
481 |
|
| 64137 | 482 |
def rm_tree(remote_dir: String): Unit = |
| 64304 | 483 |
execute("rm -r -f " + Bash.string(remote_dir)).check
|
| 64137 | 484 |
|
485 |
def tmp_dir(): String = |
|
486 |
execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
|
|
487 |
||
| 75393 | 488 |
override def with_tmp_dir[A](body: Path => A): A = {
|
| 64137 | 489 |
val remote_dir = tmp_dir() |
| 64233 | 490 |
try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
|
| 64137 | 491 |
} |
| 64123 | 492 |
} |
| 66570 | 493 |
|
494 |
||
495 |
/* system operations */ |
|
496 |
||
| 75393 | 497 |
trait System extends AutoCloseable {
|
| 73634 | 498 |
def close(): Unit = () |
499 |
||
| 66570 | 500 |
def hg_url: String = "" |
501 |
||
| 75500 | 502 |
def rsync_prefix: String = "" |
| 75517 | 503 |
def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode |
| 75500 | 504 |
|
| 66570 | 505 |
def expand_path(path: Path): Path = path.expand |
| 67066 | 506 |
def bash_path(path: Path): String = File.bash_path(path) |
|
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
67771
diff
changeset
|
507 |
def is_dir(path: Path): Boolean = path.is_dir |
| 66570 | 508 |
def is_file(path: Path): Boolean = path.is_file |
| 72376 | 509 |
def make_directory(path: Path): Path = Isabelle_System.make_directory(path) |
| 73634 | 510 |
def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
|
511 |
def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) |
|
512 |
def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1) |
|
| 75513 | 513 |
def read_bytes(path: Path): Bytes = Bytes.read(path) |
514 |
def read(path: Path): String = File.read(path) |
|
| 66570 | 515 |
|
516 |
def execute(command: String, |
|
517 |
progress_stdout: String => Unit = (_: String) => (), |
|
518 |
progress_stderr: String => Unit = (_: String) => (), |
|
| 73634 | 519 |
settings: Boolean = true, |
| 66570 | 520 |
strict: Boolean = true): Process_Result = |
| 73634 | 521 |
Isabelle_System.bash(command, |
522 |
progress_stdout = progress_stdout, |
|
523 |
progress_stderr = progress_stderr, |
|
524 |
env = if (settings) Isabelle_System.settings() else null, |
|
525 |
strict = strict) |
|
| 72338 | 526 |
|
| 72340 | 527 |
def isabelle_platform: Isabelle_Platform = Isabelle_Platform() |
| 66570 | 528 |
} |
529 |
||
530 |
object Local extends System |
|
| 64123 | 531 |
} |