# HG changeset patch
# User wenzelm
# Date 1543863888 -3600
# Node ID d1c4a1dee9e739b54076e8ff6d62118be00f5e6d
# Parent  f3240f3aa698bc9de6db3b16c07e27ba66e8fbcf
more explicit support for Isabelle system components;
activate_bundled_components: check component dir as in makedist_bundle;

diff -r f3240f3aa698 -r d1c4a1dee9e7 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Mon Dec 03 15:15:54 2018 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Mon Dec 03 20:04:48 2018 +0100
@@ -268,7 +268,7 @@
 
     // etc/settings
 
-    val settings_path = target_dir + Path.explode("etc/settings")
+    val settings_path = Components.settings(target_dir)
     Isabelle_System.mkdirs(settings_path.dir)
     File.write(settings_path,
       "# -*- shell-script -*- :mode=shellscript:\n\nisabelle_fonts \\\n" +
diff -r f3240f3aa698 -r d1c4a1dee9e7 src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Mon Dec 03 15:15:54 2018 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Mon Dec 03 20:04:48 2018 +0100
@@ -163,7 +163,7 @@
         val component_dir = dir + jdk_path
 
         Isabelle_System.mkdirs(component_dir + Path.explode("etc"))
-        File.write(component_dir + Path.explode("etc/settings"), settings)
+        File.write(Components.settings(component_dir), settings)
         File.write(component_dir + Path.explode("README"), readme(version))
 
         for ((_, platform) <- extracted)
diff -r f3240f3aa698 -r d1c4a1dee9e7 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Mon Dec 03 15:15:54 2018 +0100
+++ b/src/Pure/Admin/build_release.scala	Mon Dec 03 20:04:48 2018 +0100
@@ -129,46 +129,69 @@
   }
 
 
-  /* components */
+  /* bundled components */
+
+  class Bundled(platform: String = "")
+  {
+    def detect(s: String): Boolean =
+      s.startsWith("#bundled") && !s.startsWith("#bundled ")
+
+    def apply(name: String): String =
+      "#bundled" + (if (platform == "") "" else "-" + platform) + ":" + name
 
-  def components_dir(dir: Path): Path = dir + Path.explode("Admin/components")
-  def components_file(dir: Path): Path = dir + Path.explode("etc/components")
+    private val Pattern1 = ("""^#bundled:(.*)$""").r
+    private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
+
+    def unapply(s: String): Option[String] =
+      s match {
+        case Pattern1(name) => Some(name)
+        case Pattern2(platform1, name) if platform == platform1 => Some(name)
+        case _ => None
+      }
+  }
 
   def record_bundled_components(dir: Path)
   {
     val catalogs =
-      List("main", "bundled").map((_, "#bundled:")) :::
-      default_platform_families.flatMap(
-        platform => List(platform, "bundled-" + platform).map((_, "#bundled-" + platform + ":")))
+      List("main", "bundled").map((_, new Bundled())) :::
+      default_platform_families.flatMap(platform =>
+        List(platform, "bundled-" + platform).map((_, new Bundled(platform = platform))))
 
-    File.append(components_file(dir),
+    File.append(Components.components(dir),
       terminate_lines("#bundled components" ::
         (for {
-          (catalog, prefix) <- catalogs.iterator
-          val path = components_dir(dir) + Path.basic(catalog)
+          (catalog, bundled) <- catalogs.iterator
+          val path = Components.admin(dir) + Path.basic(catalog)
           if path.is_file
           line <- split_lines(File.read(path))
           if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
-        } yield prefix + line).toList))
+        } yield bundled(line)).toList))
+  }
+
+  def get_bundled_components(dir: Path, platform: String): List[String] =
+  {
+    val Bundled = new Bundled(platform)
+    for (Bundled(name) <- Components.read_components(dir)) yield name
   }
 
   def activate_bundled_components(dir: Path, platform: String)
   {
-    val Bundled_Platform = ("""^#bundled(?:-\Q""" + platform + """\E)?:(.*)$""").r
-    val Bundled = ("""^#bundled.*:.*$""").r
-    File.write(components_file(dir),
-      cat_lines(split_lines(File.read(components_file(dir))).flatMap(line =>
+    val Bundled = new Bundled(platform)
+    Components.write_components(dir,
+      Components.read_components(dir).flatMap(line =>
         line match {
-          case Bundled_Platform(arg) => Some("contrib/" + arg)
-          case Bundled() => None
-          case _ => Some(line)
-        })))
+          case Bundled(name) =>
+            if (Components.check_dir(Components.contrib(dir, name)))
+              Some(Components.contrib(name = name).implode)
+            else None
+          case _ => if (Bundled.detect(line)) None else Some(line)
+        }))
   }
 
   def make_contrib(dir: Path)
   {
-    Isabelle_System.mkdirs(dir + Path.explode("contrib"))
-    File.write(dir + Path.explode("contrib/README"),
+    Isabelle_System.mkdirs(Components.contrib(dir))
+    File.write(Components.contrib(dir, "README"),
 """This directory contains add-on components that contribute to the main
 Isabelle distribution.  Separate licensing conditions apply, see each
 directory individually.
@@ -194,7 +217,7 @@
         case Some(rel_path) => rel_path
         case None =>
           File.relative_path(contrib_base, abs_path) match {
-            case Some(rel_path) => Path.explode("contrib") + rel_path
+            case Some(rel_path) => Components.contrib() + rel_path
             case None => error("Bad ISABELLE_CLASSPATH element: " + path)
           }
       }
@@ -305,7 +328,7 @@
           progress = progress)
 
       other_isabelle.init_settings(
-        other_isabelle.init_components(base = base_dir.absolute + Path.explode("contrib")))
+        other_isabelle.init_components(base = Components.contrib(base_dir.absolute)))
       other_isabelle.resolve_components(echo = true)
 
       try {
diff -r f3240f3aa698 -r d1c4a1dee9e7 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Mon Dec 03 15:15:54 2018 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Mon Dec 03 20:04:48 2018 +0100
@@ -68,8 +68,8 @@
 
   /* components */
 
-  def default_components_base: Path = isabelle_home_user.absolute.dir + Path.explode("contrib")
-  def default_components_dir: Path = isabelle_home.absolute + Path.explode("Admin/components")
+  def default_components_base: Path = Components.contrib(isabelle_home_user.absolute.dir)
+  def default_components_dir: Path = Components.admin(isabelle_home.absolute)
   def default_catalogs: List[String] = List("main")
 
   def init_components(
diff -r f3240f3aa698 -r d1c4a1dee9e7 src/Pure/System/components.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/components.scala	Mon Dec 03 20:04:48 2018 +0100
@@ -0,0 +1,33 @@
+/*  Title:      Pure/Admin/components.scala
+    Author:     Makarius
+
+Isabelle system components.
+*/
+
+package isabelle
+
+
+object Components
+{
+  /* component collections */
+
+  def admin(dir: Path): Path = dir + Path.explode("Admin/components")
+
+  def contrib(dir: Path = Path.current, name: String = ""): Path =
+    dir + Path.explode("contrib") + Path.explode(name)
+
+
+  /* component directory content */
+
+  def settings(dir: Path): Path = dir + Path.explode("etc/settings")
+  def components(dir: Path): Path = dir + Path.explode("etc/components")
+
+  def check_dir(dir: Path): Boolean =
+    settings(dir).is_file || components(dir).is_file
+
+  def read_components(dir: Path): List[String] =
+    split_lines(File.read(components(dir))).filter(_.nonEmpty)
+
+  def write_components(dir: Path, lines: List[String]): Unit =
+    File.write(components(dir), terminate_lines(lines))
+}
diff -r f3240f3aa698 -r d1c4a1dee9e7 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Dec 03 15:15:54 2018 +0100
+++ b/src/Pure/build-jars	Mon Dec 03 20:04:48 2018 +0100
@@ -113,6 +113,7 @@
   ROOT.scala
   System/bash.scala
   System/command_line.scala
+  System/components.scala
   System/cygwin.scala
   System/distribution.scala
   System/getopts.scala