author | wenzelm |
Sun, 25 Nov 2018 18:45:10 +0100 | |
changeset 69344 | f87fdd8d2baf |
parent 69277 | 258bef08b31e |
permissions | -rw-r--r-- |
64161 | 1 |
/* Title: Pure/Admin/remote_dmg.scala |
64143 | 2 |
Author: Makarius |
3 |
||
4 |
Build dmg on remote Mac OS X system. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Remote_DMG |
|
11 |
{ |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64233
diff
changeset
|
12 |
def remote_dmg(ssh: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "") |
64143 | 13 |
{ |
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64233
diff
changeset
|
14 |
ssh.with_tmp_dir(remote_dir => |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64233
diff
changeset
|
15 |
{ |
64304 | 16 |
val cd = "cd " + ssh.bash_path(remote_dir) + "; " |
64143 | 17 |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64233
diff
changeset
|
18 |
ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64233
diff
changeset
|
19 |
ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64233
diff
changeset
|
20 |
ssh.execute( |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64233
diff
changeset
|
21 |
cd + "hdiutil create -srcfolder root" + |
64304 | 22 |
(if (volume_name == "") "" else " -volname " + Bash.string(volume_name)) + |
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64233
diff
changeset
|
23 |
" dmg.dmg").check |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64233
diff
changeset
|
24 |
ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64233
diff
changeset
|
25 |
}) |
64143 | 26 |
} |
27 |
||
28 |
||
29 |
/* Isabelle tool wrapper */ |
|
30 |
||
64161 | 31 |
val isabelle_tool = |
32 |
Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args => |
|
33 |
{ |
|
34 |
Command_Line.tool0 { |
|
65594 | 35 |
var port = 0 |
64161 | 36 |
var volume_name = "" |
64143 | 37 |
|
64161 | 38 |
val getopts = Getopts(""" |
64143 | 39 |
Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE |
40 |
||
41 |
Options are: |
|
65594 | 42 |
-p PORT alternative SSH port |
64143 | 43 |
-V NAME specify volume name |
44 |
||
45 |
Turn the contents of a tar.gz file into a dmg file -- produced on a remote |
|
46 |
Mac OS X system. |
|
47 |
""", |
|
64161 | 48 |
"p:" -> (arg => port = Value.Int.parse(arg)), |
49 |
"V:" -> (arg => volume_name = arg)) |
|
64143 | 50 |
|
64161 | 51 |
val more_args = getopts(args) |
52 |
val (user, host, tar_gz_file, dmg_file) = |
|
53 |
more_args match { |
|
64185 | 54 |
case List(SSH.Target(user, host), tar_gz_file, dmg_file) => |
64161 | 55 |
(user, host, Path.explode(tar_gz_file), Path.explode(dmg_file)) |
56 |
case _ => getopts.usage() |
|
57 |
} |
|
64143 | 58 |
|
67844 | 59 |
val options = Options.init() |
67067 | 60 |
using(SSH.open_session(options, host = host, user = user, port = port))( |
64161 | 61 |
remote_dmg(_, tar_gz_file, dmg_file, volume_name)) |
62 |
} |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
67844
diff
changeset
|
63 |
}) |
64143 | 64 |
} |