src/Pure/Tools/build_history.scala

--- a/src/Pure/Tools/build_history.scala	Mon Oct 03 20:09:50 2016 +0200
+++ b/src/Pure/Tools/build_history.scala	Mon Oct 03 20:26:32 2016 +0200
@@ -8,13 +8,71 @@
 
 
 import java.io.{File => JFile}
+import java.util.Calendar
 
 
 object Build_History
 {
-  def apply(hg: Mercurial.Repository, rev: String = "",
-    isabelle_identifier: String = "build_history"): Build_History =
-      new Build_History(hg, rev, isabelle_identifier)
+  /* build_history */
+
+  private val default_rev = "tip"
+  private val default_isabelle_identifier = "build_history"
+
+  def build_history(
+    hg: Mercurial.Repository,
+    rev: String = default_rev,
+    isabelle_identifier: String = default_isabelle_identifier,
+    components_base: String = "",
+    nonfree: Boolean = false,
+    verbose: Boolean = false)
+  {
+    hg.update(rev = rev, clean = true)
+    if (verbose) hg.command("log -l1").check.print
+
+    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 isabelle(cmdline: String): Process_Result = bash("bin/isabelle " + cmdline)
+
+    val isabelle_home_user: Path = Path.explode(isabelle("getenv -b ISABELLE_HOME_USER").check.out)
+
+
+    /* init settings */
+
+    {
+      val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
+      if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
+        error("User settings file already exists: " + etc_settings)
+
+      Isabelle_System.mkdirs(etc_settings.dir)
+
+      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 settings =
+        catalogs.map(catalog =>
+          "init_components " + File.bash_path(components_base_path) +
+            " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
+
+      File.write(etc_settings,
+        "# generated by Isabelle " + Calendar.getInstance.getTime + "\n" +
+        "#-*- shell-script -*- :mode=shellscript:\n\n" +
+        Library.terminate_lines(settings))
+    }
+
+
+    /* components */
+
+    isabelle("components -a").check.print_if(verbose)
+    isabelle("jedit -b -f").check.print_if(verbose)
+
+    isabelle("build -?").print
+  }
 
 
   /* command line entry point */
@@ -22,56 +80,46 @@
   def main(args: Array[String])
   {
     Command_Line.tool0 {
+      var components_base = ""
+      var isabelle_identifier = default_isabelle_identifier
       var force = false
+      var nonfree = false
+      var rev = default_rev
+      var verbose = false
 
       val getopts = Getopts("""
-Usage: isabelle build_history [OPTIONS] REPOSITORY [REV]
+Usage: isabelle build_history [OPTIONS] REPOSITORY
 
   Options are:
-    -f           force -- allow irreversible operations on REPOSITORY
+    -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
+    -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
+    -f           force -- allow irreversible operations on REPOSITORY clone
+    -n           include nonfree components
+    -r REV       update to revision
+    -v           verbose
 
   Build Isabelle sessions from the history of another REPOSITORY clone,
-  starting at changeset REV (default: tip).
+  starting at changeset REV (default: """ + default_rev + """).
 """,
-        "f" -> (_ => force = true))
+        "C:" -> (arg => components_base = arg),
+        "N:" -> (arg => isabelle_identifier = arg),
+        "f" -> (_ => force = true),
+        "n" -> (_ => nonfree = true),
+        "r:" -> (arg => rev = arg),
+        "v" -> (_ => verbose = 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()
-        }
+      val root = more_args match { case List(root) => (root) 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)
+          build_history(hg, rev = rev, isabelle_identifier = isabelle_identifier,
+            components_base = components_base, nonfree = nonfree, verbose = verbose)
         })
     }
   }
 }
-
-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)
-  }
-}