src/Pure/Admin/remote_dmg.scala
author wenzelm
Tue Oct 18 10:05:38 2016 +0200 (2016-10-18)
changeset 64294 303976a45afe
parent 64257 9d51ac055cec
child 64304 96bc94c87a81
permissions -rw-r--r--
shared_home is default for classic isatest home setup;
distinct ISABELLE_IDENTIFIER for all tasks;
wenzelm@64161
     1
/*  Title:      Pure/Admin/remote_dmg.scala
wenzelm@64143
     2
    Author:     Makarius
wenzelm@64143
     3
wenzelm@64143
     4
Build dmg on remote Mac OS X system.
wenzelm@64143
     5
*/
wenzelm@64143
     6
wenzelm@64143
     7
package isabelle
wenzelm@64143
     8
wenzelm@64143
     9
wenzelm@64143
    10
object Remote_DMG
wenzelm@64143
    11
{
wenzelm@64256
    12
  def remote_dmg(ssh: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
wenzelm@64143
    13
  {
wenzelm@64256
    14
    ssh.with_tmp_dir(remote_dir =>
wenzelm@64256
    15
      {
wenzelm@64256
    16
        val cd = "cd " + File.bash_string(ssh.remote_path(remote_dir)) + "; "
wenzelm@64143
    17
wenzelm@64256
    18
        ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file)
wenzelm@64256
    19
        ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
wenzelm@64256
    20
        ssh.execute(
wenzelm@64256
    21
          cd + "hdiutil create -srcfolder root" +
wenzelm@64256
    22
            (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
wenzelm@64256
    23
            " dmg.dmg").check
wenzelm@64256
    24
        ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file)
wenzelm@64256
    25
      })
wenzelm@64143
    26
  }
wenzelm@64143
    27
wenzelm@64143
    28
wenzelm@64143
    29
  /* Isabelle tool wrapper */
wenzelm@64143
    30
wenzelm@64161
    31
  val isabelle_tool =
wenzelm@64161
    32
    Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
wenzelm@64161
    33
    {
wenzelm@64161
    34
      Command_Line.tool0 {
wenzelm@64161
    35
        var port = SSH.default_port
wenzelm@64161
    36
        var volume_name = ""
wenzelm@64143
    37
wenzelm@64161
    38
        val getopts = Getopts("""
wenzelm@64143
    39
Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
wenzelm@64143
    40
wenzelm@64143
    41
  Options are:
wenzelm@64143
    42
    -p PORT      alternative SSH port (default: """ + SSH.default_port + """)
wenzelm@64143
    43
    -V NAME      specify volume name
wenzelm@64143
    44
wenzelm@64143
    45
  Turn the contents of a tar.gz file into a dmg file -- produced on a remote
wenzelm@64143
    46
  Mac OS X system.
wenzelm@64143
    47
""",
wenzelm@64161
    48
          "p:" -> (arg => port = Value.Int.parse(arg)),
wenzelm@64161
    49
          "V:" -> (arg => volume_name = arg))
wenzelm@64143
    50
wenzelm@64161
    51
        val more_args = getopts(args)
wenzelm@64161
    52
        val (user, host, tar_gz_file, dmg_file) =
wenzelm@64161
    53
          more_args match {
wenzelm@64185
    54
            case List(SSH.Target(user, host), tar_gz_file, dmg_file) =>
wenzelm@64161
    55
              (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file))
wenzelm@64161
    56
            case _ => getopts.usage()
wenzelm@64161
    57
          }
wenzelm@64143
    58
wenzelm@64257
    59
        val ssh = SSH.init_context(Options.init)
wenzelm@64161
    60
        using(ssh.open_session(user = user, host = host, port = port))(
wenzelm@64161
    61
          remote_dmg(_, tar_gz_file, dmg_file, volume_name))
wenzelm@64161
    62
      }
wenzelm@64161
    63
    }, admin = true)
wenzelm@64143
    64
}