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;
     1 /*  Title:      Pure/Admin/remote_dmg.scala
     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 {
    12   def remote_dmg(ssh: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
    13   {
    14     ssh.with_tmp_dir(remote_dir =>
    15       {
    16         val cd = "cd " + File.bash_string(ssh.remote_path(remote_dir)) + "; "
    17 
    18         ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file)
    19         ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
    20         ssh.execute(
    21           cd + "hdiutil create -srcfolder root" +
    22             (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
    23             " dmg.dmg").check
    24         ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file)
    25       })
    26   }
    27 
    28 
    29   /* Isabelle tool wrapper */
    30 
    31   val isabelle_tool =
    32     Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
    33     {
    34       Command_Line.tool0 {
    35         var port = SSH.default_port
    36         var volume_name = ""
    37 
    38         val getopts = Getopts("""
    39 Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
    40 
    41   Options are:
    42     -p PORT      alternative SSH port (default: """ + SSH.default_port + """)
    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 """,
    48           "p:" -> (arg => port = Value.Int.parse(arg)),
    49           "V:" -> (arg => volume_name = arg))
    50 
    51         val more_args = getopts(args)
    52         val (user, host, tar_gz_file, dmg_file) =
    53           more_args match {
    54             case List(SSH.Target(user, host), tar_gz_file, dmg_file) =>
    55               (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file))
    56             case _ => getopts.usage()
    57           }
    58 
    59         val ssh = SSH.init_context(Options.init)
    60         using(ssh.open_session(user = user, host = host, port = port))(
    61           remote_dmg(_, tar_gz_file, dmg_file, volume_name))
    62       }
    63     }, admin = true)
    64 }