src/Pure/Tools/build_history.scala
changeset 64021 1e23caac8757
child 64023 41f7e383c19e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/build_history.scala	Mon Oct 03 16:50:29 2016 +0200
     1.3 @@ -0,0 +1,79 @@
     1.4 +/*  Title:      Pure/Tools/build_history.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Build other history versions.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.io.{File => JFile}
    1.14 +
    1.15 +
    1.16 +object Build_History
    1.17 +{
    1.18 +  val rev0 = "0cebcbeac4c7"  // wenzelm 29-Aug-2012: provide polyml-5.4.1 as regular component
    1.19 +
    1.20 +  def apply(hg: Mercurial.Repository, rev: String = "",
    1.21 +    isabelle_identifier: String = "build_history"): Build_History =
    1.22 +      new Build_History(hg, rev, isabelle_identifier)
    1.23 +
    1.24 +
    1.25 +  /* command line entry point */
    1.26 +
    1.27 +  def main(args: Array[String])
    1.28 +  {
    1.29 +    Command_Line.tool0 {
    1.30 +      var force = false
    1.31 +
    1.32 +      val getopts = Getopts("""
    1.33 +Usage: isabelle build_history [OPTIONS] REPOSITORY [REV]
    1.34 +
    1.35 +  Options are:
    1.36 +    -f           force -- allow irreversible operations on REPOSITORY
    1.37 +
    1.38 +  Build Isabelle sessions from the history of another REPOSITORY clone,
    1.39 +  starting at changeset REV (default: tip).
    1.40 +""",
    1.41 +        "f" -> (_ => force = true))
    1.42 +
    1.43 +      val more_args = getopts(args)
    1.44 +
    1.45 +      val (root, rev) =
    1.46 +        more_args match {
    1.47 +          case List(root, rev) => (root, rev)
    1.48 +          case List(root) => (root, "tip")
    1.49 +          case _ => getopts.usage()
    1.50 +        }
    1.51 +
    1.52 +      using(Mercurial.open_repository(Path.explode(root)))(hg =>
    1.53 +        {
    1.54 +          val build_history = Build_History(hg, rev)
    1.55 +
    1.56 +          if (!force)
    1.57 +            error("Repository " + hg + " will be cleaned by force!\n" +
    1.58 +              "Need to provide option -f to confirm this.")
    1.59 +
    1.60 +          build_history.init()
    1.61 +
    1.62 +          Output.writeln(
    1.63 +            build_history.bash("bin/isabelle getenv ISABELLE_HOME ISABELLE_HOME_USER").check.out)
    1.64 +        })
    1.65 +    }
    1.66 +  }
    1.67 +}
    1.68 +
    1.69 +class Build_History private(hg: Mercurial.Repository, rev: String, isabelle_identifier: String)
    1.70 +{
    1.71 +  override def toString: String =
    1.72 +    List(hg.toString, rev, isabelle_identifier).mkString("Build_History(", ",", ")")
    1.73 +
    1.74 +  def bash(script: String): Process_Result =
    1.75 +    Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) +
    1.76 +      " " + script, cwd = hg.root.file, env = null)
    1.77 +
    1.78 +  def init()
    1.79 +  {
    1.80 +    hg.update(rev = rev, clean = true)
    1.81 +  }
    1.82 +}