more explicit support for Isabelle system components;
activate_bundled_components: check component dir as in makedist_bundle;
--- 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" +
--- 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)
--- 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 {
--- 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(
--- /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))
+}
--- 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