# HG changeset patch
# User wenzelm
# Date 1475660580 -7200
# Node ID ac3ed62c53c3172f56efeed006fa97584094042e
# Parent  b0c52944978e86ee3643b2a029425ddedbe1b0dc
misc tuning and clarification;

diff -r b0c52944978e -r ac3ed62c53c3 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Wed Oct 05 11:13:02 2016 +0200
+++ b/src/Pure/System/progress.scala	Wed Oct 05 11:43:00 2016 +0200
@@ -10,6 +10,7 @@
 class Progress
 {
   def echo(msg: String) {}
+  def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
   def theory(session: String, theory: String) {}
   def stopped: Boolean = false
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
diff -r b0c52944978e -r ac3ed62c53c3 src/Pure/Tools/build_history.scala
--- a/src/Pure/Tools/build_history.scala	Wed Oct 05 11:13:02 2016 +0200
+++ b/src/Pure/Tools/build_history.scala	Wed Oct 05 11:43:00 2016 +0200
@@ -13,6 +13,64 @@
 
 object Build_History
 {
+  /* other Isabelle environment */
+
+  private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
+  {
+    other_isabelle =>
+
+    def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
+      Isabelle_System.bash(
+        "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
+        env = null, cwd = isabelle_home.file, redirect = redirect,
+        progress_stdout = progress.echo_if(echo, _),
+        progress_stderr = progress.echo_if(echo, _))
+
+    def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
+      bash("bin/isabelle " + cmdline, redirect, echo)
+
+    def resolve_components(echo: Boolean): Unit =
+      other_isabelle("components -a", redirect = true, echo = echo).check
+
+    val isabelle_home_user =
+      Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
+  }
+
+
+  /* settings environment */
+
+  private def init_settings(
+    isabelle_home_user: Path, components_base: String, nonfree: Boolean): Path =
+  {
+    val etc_settings = isabelle_home_user + Path.explode("etc/settings")
+
+    if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
+      error("Cannot proceed with existing user settings file: " + etc_settings)
+
+    Isabelle_System.mkdirs(etc_settings.dir)
+    File.write(etc_settings,
+      "# generated by Isabelle " + Calendar.getInstance.getTime + "\n" +
+      "#-*- shell-script -*- :mode=shellscript:\n")
+
+    val component_settings =
+    {
+      val components_base_path =
+        if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
+        else Path.explode(components_base).expand
+
+      val catalogs =
+        if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
+
+      catalogs.map(catalog =>
+        "init_components " + File.bash_path(components_base_path) +
+          " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
+    }
+    File.append(etc_settings, "\n" + Library.terminate_lines(component_settings))
+
+    etc_settings
+  }
+
+
   /* build_history */
 
   private val default_rev = "tip"
@@ -36,12 +94,6 @@
     verbose: Boolean = false,
     build_args: List[String] = Nil): Process_Result =
   {
-    /* output */
-
-    def output(msg: String) { progress.echo(msg) }
-    def output_if(b: Boolean, msg: String) { if (b) output(msg) }
-
-
     /* sanity checks */
 
     if (File.eq(Path.explode("~~").file, hg.root.file))
@@ -60,61 +112,18 @@
     }
 
 
-    /* purge repository */
+    /* init repository */
 
     hg.update(rev = rev, clean = true)
-    output_if(verbose, hg.log(rev, options = "-l1"))
-
-
-    /* invoke isabelle tools */
-
-    def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
-      Isabelle_System.bash(
-        "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
-        env = null, cwd = hg.root.file, redirect = redirect,
-        progress_stdout = output_if(echo, _), progress_stderr = output_if(echo, _))
-
-    def isabelle(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
-      bash("bin/isabelle " + cmdline, redirect, echo)
-
-    val isabelle_home_user = Path.explode(isabelle("getenv -b ISABELLE_HOME_USER").check.out)
-    val isabelle_output = Path.explode(isabelle("getenv -b ISABELLE_OUTPUT").check.out)
+    progress.echo_if(verbose, hg.log(rev, options = "-l1"))
 
 
-    /* reset settings */
-
-    val etc_settings = isabelle_home_user + Path.explode("etc/settings")
-
-    if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
-      error("Cannot proceed with existing user settings file: " + etc_settings)
-
-    Isabelle_System.mkdirs(etc_settings.dir)
-
-    File.write(etc_settings,
-      "# generated by Isabelle " + Calendar.getInstance.getTime + "\n" +
-      "#-*- shell-script -*- :mode=shellscript:\n")
-
-
-    /* initial settings */
+    /* init settings */
 
-    val component_settings =
-    {
-      val components_base_path =
-        if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
-        else Path.explode(components_base).expand
-
-      val catalogs =
-        if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
+    val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
 
-      catalogs.map(catalog =>
-        "init_components " + File.bash_path(components_base_path) +
-          " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
-    }
-
-    File.append(etc_settings, "\n" + Library.terminate_lines(component_settings))
-
-
-    isabelle("components -a", redirect = true, echo = verbose).check
+    val etc_settings = init_settings(other_isabelle.isabelle_home_user, components_base, nonfree)
+    other_isabelle.resolve_components(verbose)
 
 
     /* augmented settings */
@@ -123,12 +132,12 @@
     {
       val windows_32 = "x86-windows"
       val windows_64 = "x86_64-windows"
-      val platform_32 = isabelle("getenv -b ISABELLE_PLATFORM32").check.out
-      val platform_64 = isabelle("getenv -b ISABELLE_PLATFORM64").check.out
-      val platform_family = isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
+      val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
+      val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
+      val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
 
       val polyml_home =
-        try { Path.explode(isabelle("getenv -b ML_HOME").check.out).dir }
+        try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
         catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
 
       def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
@@ -177,16 +186,18 @@
       File.append(etc_settings, "\n" + Library.terminate_lines(more_settings))
 
 
-    isabelle("components -a", redirect = true, echo = verbose).check
+    other_isabelle.resolve_components(verbose)
 
 
     /* build */
 
-    bash("env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
+    other_isabelle.bash(
+      "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
       "bin/isabelle jedit -b" + (if (fresh) " -f" else ""), redirect = true, echo = verbose).check
 
+    val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
     Isabelle_System.rm_tree(isabelle_output.file)
-    isabelle("build " + File.bash_args(build_args), redirect = true, echo = true)
+    other_isabelle("build " + File.bash_args(build_args), redirect = true, echo = true)
   }