src/Pure/General/mercurial.scala
changeset 76169 a3c694039fd6
parent 76136 1bb677cceea4
child 76540 83de6e9ae983
equal deleted inserted replaced
76168:aab9bb081f01 76169:a3c694039fd6
   465     progress.echo("Local repository " + local_hg.root.absolute)
   465     progress.echo("Local repository " + local_hg.root.absolute)
   466 
   466 
   467 
   467 
   468     /* remote repository */
   468     /* remote repository */
   469 
   469 
   470     val remote_url =
   470     val remote_url = {
   471       remote match {
   471       if (remote.startsWith("ssh://")) {
   472         case _ if remote.startsWith("ssh://") =>
   472         val ssh_url = remote + "/" + repos_name
   473           val ssh_url = remote + "/" + repos_name
   473 
   474 
   474         if (!remote_exists) {
   475           if (!remote_exists) {
   475           try { local_hg.command("init", ssh_url, repository = false).check }
   476             try { local_hg.command("init", ssh_url, repository = false).check }
   476           catch { case ERROR(msg) => progress.echo_warning(msg) }
   477             catch { case ERROR(msg) => progress.echo_warning(msg) }
   477         }
   478           }
   478 
   479 
   479         ssh_url
   480           ssh_url
   480       }
   481 
   481       else {
   482         case SSH.Target(user, host) =>
   482         val phabricator = Phabricator.API(remote)
   483           val phabricator = Phabricator.API(user, host)
   483 
   484 
   484         var repos =
   485           var repos =
   485           phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
   486             phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
   486             if (remote_exists) {
   487               if (remote_exists) {
   487               error("Remote repository " +
   488                 error("Remote repository " +
   488                 quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
   489                   quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
       
   490               }
       
   491               else phabricator.create_repository(repos_name, short_name = repos_name)
       
   492             }
   489             }
   493 
   490             else phabricator.create_repository(repos_name, short_name = repos_name)
   494           while (repos.importing) {
   491           }
   495             progress.echo("Awaiting remote repository ...")
   492 
   496             Time.seconds(0.5).sleep()
   493         while (repos.importing) {
   497             repos = phabricator.the_repository(repos.phid)
   494           progress.echo("Awaiting remote repository ...")
   498           }
   495           Time.seconds(0.5).sleep()
   499 
   496           repos = phabricator.the_repository(repos.phid)
   500           repos.ssh_url
   497         }
   501 
   498 
   502         case _ => error("Malformed remote specification " + quote(remote))
   499         repos.ssh_url
   503       }
   500       }
       
   501     }
   504 
   502 
   505     progress.echo("Remote repository " + quote(remote_url))
   503     progress.echo("Remote repository " + quote(remote_url))
   506 
   504 
   507 
   505 
   508     /* synchronize local and remote state */
   506     /* synchronize local and remote state */