basic setup for Admin/build_history -- outside of Isabelle environment;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/build_history	Mon Oct 03 16:50:29 2016 +0200
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+#
+# DESCRIPTION: build history versions from another repository clone
+
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+
+"$THIS/build" jars || exit $?
+
+exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@"

--- a/src/Pure/System/isabelle_system.scala	Mon Oct 03 16:15:59 2016 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Oct 03 16:50:29 2016 +0200
@@ -260,7 +260,10 @@
     val proc = new ProcessBuilder
     proc.command(command_line:_*)  // fragile on Windows
     if (cwd != null) proc.directory(cwd)
-    proc.environment.clear; for ((x, y) <- env) proc.environment.put(x, y)
+    if (env != null) {
+      proc.environment.clear
+      for ((x, y) <- env) proc.environment.put(x, y)
+    }
     proc.redirectErrorStream(redirect)
     proc.start
   }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/build_history.scala	Mon Oct 03 16:50:29 2016 +0200
@@ -0,0 +1,79 @@
+/*  Title:      Pure/Tools/build_history.scala
+    Author:     Makarius
+
+Build other history versions.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+
+object Build_History
+{
+  val rev0 = "0cebcbeac4c7"  // wenzelm 29-Aug-2012: provide polyml-5.4.1 as regular component
+
+  def apply(hg: Mercurial.Repository, rev: String = "",
+    isabelle_identifier: String = "build_history"): Build_History =
+      new Build_History(hg, rev, isabelle_identifier)
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool0 {
+      var force = false
+
+      val getopts = Getopts("""
+Usage: isabelle build_history [OPTIONS] REPOSITORY [REV]
+
+  Options are:
+    -f           force -- allow irreversible operations on REPOSITORY
+
+  Build Isabelle sessions from the history of another REPOSITORY clone,
+  starting at changeset REV (default: tip).
+""",
+        "f" -> (_ => force = true))
+
+      val more_args = getopts(args)
+
+      val (root, rev) =
+        more_args match {
+          case List(root, rev) => (root, rev)
+          case List(root) => (root, "tip")
+          case _ => getopts.usage()
+        }
+
+      using(Mercurial.open_repository(Path.explode(root)))(hg =>
+        {
+          val build_history = Build_History(hg, rev)
+
+          if (!force)
+            error("Repository " + hg + " will be cleaned by force!\n" +
+              "Need to provide option -f to confirm this.")
+
+          build_history.init()
+
+          Output.writeln(
+            build_history.bash("bin/isabelle getenv ISABELLE_HOME ISABELLE_HOME_USER").check.out)
+        })
+    }
+  }
+}
+
+class Build_History private(hg: Mercurial.Repository, rev: String, isabelle_identifier: String)
+{
+  override def toString: String =
+    List(hg.toString, rev, isabelle_identifier).mkString("Build_History(", ",", ")")
+
+  def bash(script: String): Process_Result =
+    Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) +
+      " " + script, cwd = hg.root.file, env = null)
+
+  def init()
+  {
+    hg.update(rev = rev, clean = true)
+  }
+}

--- a/src/Pure/build-jars	Mon Oct 03 16:15:59 2016 +0200
+++ b/src/Pure/build-jars	Mon Oct 03 16:50:29 2016 +0200
@@ -107,6 +107,7 @@
   Tools/bibtex.scala
   Tools/build.scala
   Tools/build_doc.scala
+  Tools/build_history.scala
   Tools/build_stats.scala
   Tools/check_keywords.scala
   Tools/check_sources.scala