# HG changeset patch
# User wenzelm
# Date 1478969891 -3600
# Node ID 545a7ab3c35f5a133f1cd90348451399f21210fa
# Parent  e4707c2655eba8307005c3817793059dca405214
optional component setup;

diff -r e4707c2655eb -r 545a7ab3c35f src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Nov 12 17:00:26 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sat Nov 12 17:58:11 2016 +0100
@@ -66,7 +66,8 @@
     progress: Progress = Ignore_Progress,
     arch_64: Boolean = false,
     options: List[String] = Nil,
-    msys_root: Option[Path] = None)
+    msys_root: Option[Path] = None,
+    component_root: Option[Path] = None)
   {
     if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
       error("Bad Poly/ML root directory: " + root)
@@ -103,6 +104,18 @@
     }
 
 
+    /* component setup */
+
+    component_root match {
+      case None =>
+      case Some(component) =>
+        val etc = component + Path.explode("etc")
+        Isabelle_System.mkdirs(etc)
+        File.copy(Path.explode("~~/Admin/polyml/settings"), etc)
+        File.copy(Path.explode("~~/Admin/polyml/README"), component)
+    }
+
+
     /* configure and make */
 
     val configure_options =
@@ -136,6 +149,11 @@
       if (sha1_root.isDefined) {
         val dir1 = sha1_root.get
         bash(dir1, "./build " + platform, redirect = true, echo = true).check
+
+        if (component_root.isDefined)
+          Mercurial.repository(dir1).
+            archive(File.standard_path(component_root.get + Path.explode("sha1")))
+
         val dir2 = dir1 + Path.explode(platform)
         File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
       }
@@ -144,7 +162,7 @@
 
     /* target */
 
-    val target = Path.explode(platform)
+    val target = component_root.getOrElse(Path.current) + Path.explode(platform)
     Isabelle_System.rm_tree(target)
     Isabelle_System.mkdirs(target)
 
@@ -165,6 +183,7 @@
   val isabelle_tool = Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
     {
       Command_Line.tool0 {
+        var component_root: Option[Path] = None
         var msys_root: Option[Path] = None
         var arch_64 = false
         var sha1_root: Option[Path] = None
@@ -173,6 +192,7 @@
 Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
 
   Options are:
+    -C DIR       Isabelle component root directory (for etc/settings ...)
     -M DIR       msys root directory (for Windows)
     -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
     -s DIR       sha1 sources, see https://bitbucket.org/isabelle_project/sha1
@@ -180,6 +200,7 @@
   Build Poly/ML in the ROOT directory of its sources, with additional
   CONFIGURE_OPTIONS (e.g. --with-gmp).
 """,
+          "C:" -> (arg => component_root = Some(Path.explode(arg))),
           "M:" -> (arg => msys_root = Some(Path.explode(arg))),
           "m:" ->
             {
@@ -196,7 +217,8 @@
             case Nil => getopts.usage()
           }
         build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
-          arch_64 = arch_64, options = options, msys_root = msys_root)
+          arch_64 = arch_64, options = options, component_root = component_root,
+          msys_root = msys_root)
       }
     }, admin = true)
 }
diff -r e4707c2655eb -r 545a7ab3c35f src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Nov 12 17:00:26 2016 +0100
+++ b/src/Pure/General/mercurial.scala	Sat Nov 12 17:58:11 2016 +0100
@@ -92,6 +92,9 @@
       }
     }
 
+    def archive(target: String, rev: String = "", options: String = ""): Unit =
+      hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
+
     def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
       hg.command("heads", opt_template(template), options).check.out_lines