src/Pure/Admin/remote_dmg.scala
author wenzelm
Mon, 13 Nov 2017 14:39:03 +0100
changeset 67067 02729ced9b1e
parent 65594 659305708959
child 67844 7f82445e8f0e
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
     1
/*  Title:      Pure/Admin/remote_dmg.scala
64143
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
     3
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
     4
Build dmg on remote Mac OS X system.
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
     5
*/
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
     6
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
     7
package isabelle
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
     8
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
     9
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    10
object Remote_DMG
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    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
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    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
96bc94c87a81 clarified modules;
wenzelm
parents: 64257
diff changeset
    16
        val cd = "cd " + ssh.bash_path(remote_dir) + "; "
64143
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    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
96bc94c87a81 clarified modules;
wenzelm
parents: 64257
diff changeset
    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
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    26
  }
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    27
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    28
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    29
  /* Isabelle tool wrapper */
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    30
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    31
  val isabelle_tool =
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    32
    Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    33
    {
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    34
      Command_Line.tool0 {
65594
659305708959 clarified treatment of default port;
wenzelm
parents: 64304
diff changeset
    35
        var port = 0
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    36
        var volume_name = ""
64143
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    37
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    38
        val getopts = Getopts("""
64143
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    39
Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    40
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    41
  Options are:
65594
659305708959 clarified treatment of default port;
wenzelm
parents: 64304
diff changeset
    42
    -p PORT      alternative SSH port
64143
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    43
    -V NAME      specify volume name
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    44
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    45
  Turn the contents of a tar.gz file into a dmg file -- produced on a remote
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    46
  Mac OS X system.
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    47
""",
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    48
          "p:" -> (arg => port = Value.Int.parse(arg)),
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    49
          "V:" -> (arg => volume_name = arg))
64143
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    50
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    51
        val more_args = getopts(args)
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    52
        val (user, host, tar_gz_file, dmg_file) =
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    53
          more_args match {
64185
wenzelm
parents: 64161
diff changeset
    54
            case List(SSH.Target(user, host), tar_gz_file, dmg_file) =>
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    55
              (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file))
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    56
            case _ => getopts.usage()
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    57
          }
64143
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    58
67067
02729ced9b1e tuned signature;
wenzelm
parents: 65594
diff changeset
    59
        val options = Options.init
02729ced9b1e tuned signature;
wenzelm
parents: 65594
diff changeset
    60
        using(SSH.open_session(options, host = host, user = user, port = port))(
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    61
          remote_dmg(_, tar_gz_file, dmg_file, volume_name))
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    62
      }
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64143
diff changeset
    63
    }, admin = true)
64143
578e71c2c976 added isabelle remote_dmg tool;
wenzelm
parents:
diff changeset
    64
}