# HG changeset patch
# User wenzelm
# Date 1508241103 -7200
# Node ID 4f0ccfe1bcb6a33da1093e5ac53cb6b869e7f99e
# Parent  b540a5a64a311ac40ed011b41afc48f0545a65f9
uniform execute, with proper isabelle_identifier (notably for "isabelle components -I");

diff -r b540a5a64a31 -r 4f0ccfe1bcb6 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Oct 17 11:51:39 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Oct 17 13:51:43 2017 +0200
@@ -498,6 +498,14 @@
     val isabelle_hg =
       Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh)
 
+    def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit =
+      ssh.execute(
+        Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
+          ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args,
+        progress_stdout = progress.echo_if(echo, _),
+        progress_stderr = progress.echo_if(echo, _),
+        strict = strict).check
+
     if (self_update) {
       val self_rev =
         if (push_isabelle_home) {
@@ -511,12 +519,9 @@
           isabelle_hg.id()
         }
       isabelle_hg.update(rev = self_rev, clean = true)
-      for (cmd <- List("components -I", "components -a")) {
-        ssh.execute(
-          ssh.bash_path(isabelle_repos_self + Path.explode("bin/isabelle")) + " " + cmd).check
-      }
-      ssh.execute(
-        ssh.bash_path(isabelle_repos_self + Path.explode("Admin/build")) + " jars_fresh").check
+      execute("bin/isabelle", "components -I")
+      execute("bin/isabelle", "components -a")
+      execute("Admin/build", "jars_fresh")
     }
 
 
@@ -544,15 +549,11 @@
     {
       val output_file = tmp_dir + Path.explode("output")
 
-      ssh.execute(
-        Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
-        ssh.bash_path(isabelle_repos_self + Path.explode("Admin/build_history")) +
-          " -o " + ssh.bash_path(output_file) +
+      execute("Admin/build_history",
+        "-o " + ssh.bash_path(output_file) +
           (if (rev == "") "" else " -r " + Bash.string(rev)) + " " +
           options + afp_options + " " + ssh.bash_path(isabelle_repos_other) + " " + args,
-        progress_stdout = progress.echo(_),
-        progress_stderr = progress.echo(_),
-        strict = false).check
+        echo = true, strict = false)
 
       for (line <- split_lines(ssh.read(output_file)))
       yield {