--- a/src/Pure/Admin/build_history.scala Sat Jun 17 18:49:19 2017 +0200
+++ b/src/Pure/Admin/build_history.scala Sat Jun 17 20:24:22 2017 +0200
@@ -429,6 +429,7 @@
self_update: Boolean = false,
push_isabelle_home: Boolean = false,
progress: Progress = No_Progress,
+ rev: String = "",
options: String = "",
args: String = ""): List[(String, Bytes)] =
{
@@ -440,33 +441,31 @@
val isabelle_hg =
Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = Some(ssh))
- val rev =
- if (self_update) {
- val rev =
- if (push_isabelle_home) {
- val isabelle_home_hg = Mercurial.repository(Path.explode("~~"))
- val rev = isabelle_home_hg.id()
- isabelle_home_hg.push(isabelle_hg.root_url, rev = rev, force = true)
- rev
- }
- else {
- isabelle_hg.pull()
- isabelle_hg.id()
- }
- isabelle_hg.update(rev = rev, clean = true)
- ssh.execute(
- ssh.bash_path(isabelle_repos_self + Path.explode("bin/isabelle"))
- + " components -a").check
- ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
- rev
- }
- else "tip"
+ if (self_update) {
+ val self_rev =
+ if (push_isabelle_home) {
+ val isabelle_home_hg = Mercurial.repository(Path.explode("~~"))
+ val self_rev = isabelle_home_hg.id()
+ isabelle_home_hg.push(isabelle_hg.root_url, rev = self_rev, force = true)
+ self_rev
+ }
+ else {
+ isabelle_hg.pull()
+ isabelle_hg.id()
+ }
+ isabelle_hg.update(rev = self_rev, clean = true)
+ ssh.execute(
+ ssh.bash_path(isabelle_repos_self + Path.explode("bin/isabelle"))
+ + " components -a").check
+ ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
+ }
+ if (Mercurial.is_repository(isabelle_repos_other, ssh = Some(ssh))) {
+ ssh.rm_tree(isabelle_repos_other)
+ }
val other_hg =
- Mercurial.setup_repository(
- ssh.bash_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
- other_hg.pull(isabelle_hg.root.implode)
- other_hg.update(rev = rev, clean = true)
+ Mercurial.clone_repository(
+ ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev, ssh = Some(ssh))
/* Admin/build_history */
@@ -478,8 +477,9 @@
ssh.execute(
Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
ssh.bash_path(isabelle_admin + Path.explode("build_history")) +
- " -o " + ssh.bash_path(output_file) + " " + options + " " +
- ssh.bash_path(isabelle_repos_other) + " " + args,
+ " -o " + ssh.bash_path(output_file) +
+ (if (rev == "") "" else " -r " + Bash.string(rev)) + " " +
+ options + " " + ssh.bash_path(isabelle_repos_other) + " " + args,
progress_stdout = progress.echo(_),
progress_stderr = progress.echo(_),
strict = false).check
--- a/src/Pure/Admin/isabelle_cronjob.scala Sat Jun 17 18:49:19 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sat Jun 17 20:24:22 2017 +0200
@@ -243,8 +243,8 @@
isabelle_identifier = "cronjob_build_history",
self_update = self_update,
push_isabelle_home = push_isabelle_home,
+ rev = rev,
options =
- "-r " + Bash.string(rev) +
" -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
" -f " + r.options,
args = "-o timeout=10800 " + r.args)
--- a/src/Pure/General/mercurial.scala Sat Jun 17 18:49:19 2017 +0200
+++ b/src/Pure/General/mercurial.scala Sat Jun 17 20:24:22 2017 +0200
@@ -51,15 +51,16 @@
}
}
- def clone_repository(
- source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
+ def clone_repository(source: String, root: Path, rev: String = "", options: String = "",
+ ssh: Option[SSH.Session] = None): Repository =
{
val hg = new Repository(root, ssh)
ssh match {
case None => Isabelle_System.mkdirs(hg.root.dir)
case Some(ssh) => ssh.mkdirs(hg.root.dir)
}
- hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root), options).check
+ hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev), options)
+ .check
hg
}
@@ -71,7 +72,7 @@
case Some(ssh) => ssh.is_dir(root)
}
if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
- else clone_repository(source, root, options = "--pull --noupdate", ssh = ssh)
+ else clone_repository(source, root, options = "--noupdate", ssh = ssh)
}
class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session])
--- a/src/Pure/PIDE/query_operation.scala Sat Jun 17 18:49:19 2017 +0200
+++ b/src/Pure/PIDE/query_operation.scala Sat Jun 17 20:24:22 2017 +0200
@@ -185,15 +185,15 @@
remove_overlay()
current_state.change(_ => Query_Operation.State.empty)
consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
- if (!snapshot.is_outdated) {
- editor.current_command(editor_context, snapshot) match {
- case Some(command) =>
- val state = Query_Operation.State.make(command, query)
- current_state.change(_ => state)
- editor.insert_overlay(command, print_function, state.instance :: query)
- case None =>
- }
+
+ editor.current_command(editor_context, snapshot) match {
+ case Some(command) =>
+ val state = Query_Operation.State.make(command, query)
+ current_state.change(_ => state)
+ editor.insert_overlay(command, print_function, state.instance :: query)
+ case None =>
}
+
consume_status(current_state.value.status)
editor.flush()
case None =>