merged
authornipkow
Sat, 17 Jun 2017 20:24:22 +0200
changeset 66111 20304512a33b
parent 66108 8b433b6f302f (diff)
parent 66110 d59f9f696110 (current diff)
child 66112 0e640e04fc56
child 66114 c137a9f038a6
merged
--- 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 =>