--- /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)
+ }
+}