--- a/src/Pure/General/path.scala Sat Jul 24 13:09:48 2021 +0200
+++ b/src/Pure/General/path.scala Sat Jul 24 15:38:41 2021 +0200
@@ -207,6 +207,14 @@
def dir: Path = split_path._1
def base: Path = new Path(List(Path.Basic(split_path._2)))
+ def ends_with(a: String): Boolean =
+ elems match {
+ case Path.Basic(b) :: _ => b.endsWith(a)
+ case _ => false
+ }
+ def is_java: Boolean = ends_with(".java")
+ def is_scala: Boolean = ends_with(".scala")
+
def ext(e: String): Path =
if (e == "") this
else {
--- a/src/Pure/Tools/scala_build.scala Sat Jul 24 13:09:48 2021 +0200
+++ b/src/Pure/Tools/scala_build.scala Sat Jul 24 15:38:41 2021 +0200
@@ -15,7 +15,26 @@
object Scala_Build
{
- type Context = isabelle.setup.Build.Context
+ class Context private[Scala_Build](java_context: isabelle.setup.Build.Context)
+ {
+ def is_module(path: Path): Boolean =
+ {
+ val module_name: String = java_context.module_name()
+ module_name.nonEmpty && File.eq(java_context.path(module_name).toFile, path.file)
+ }
+
+ def sources: List[Path] =
+ java_context.sources().asScala.toList.map(s => File.path(java_context.path(s).toFile))
+
+ def requirements: List[Path] =
+ (for {
+ s <- java_context.requirements().asScala.iterator
+ p <- java_context.requirement_paths(s).asScala.iterator
+ } yield (File.path(p.toFile))).toList
+
+ def build(fresh: Boolean = false): Unit =
+ isabelle.setup.Build.build(java_context, fresh)
+ }
def context(dir: Path,
component: Boolean = false,
@@ -30,7 +49,7 @@
props.load(Files.newBufferedReader(props_path.java_path))
for ((a, b) <- more_props) props.put(a, b)
- new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode)
+ new Context(new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode))
}
def build(dir: Path,
@@ -38,10 +57,9 @@
component: Boolean = false,
more_props: Properties.T = Nil): Unit =
{
- isabelle.setup.Build.build(
- context(dir, component = component, more_props = more_props), fresh)
+ context(dir, component = component, more_props = more_props).build(fresh = fresh)
}
def component_contexts(): List[Context] =
- isabelle.setup.Build.component_contexts().asScala.toList
+ isabelle.setup.Build.component_contexts().asScala.toList.map(new Context(_))
}
--- a/src/Pure/Tools/scala_project.scala Sat Jul 24 13:09:48 2021 +0200
+++ b/src/Pure/Tools/scala_project.scala Sat Jul 24 15:38:41 2021 +0200
@@ -7,8 +7,6 @@
package isabelle
-import scala.jdk.CollectionConverters._
-
object Scala_Project
{
@@ -35,27 +33,17 @@
val contexts = Scala_Build.component_contexts() ::: plugin_contexts()
val jars1 = Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH"))
- val jars2 =
- (for {
- context <- contexts.iterator
- s <- context.requirements().asScala.iterator
- path <- context.requirement_paths(s).asScala.iterator
- } yield File.path(path.toFile)).toList
+ val jars2 = contexts.flatMap(_.requirements)
val jar_files =
- Library.distinct(jars1 ::: jars2).filterNot(path =>
- contexts.exists(context =>
- {
- val name: String = context.module_name()
- name.nonEmpty && File.eq(context.path(name).toFile, path.file)
- }))
+ Library.distinct(jars1 ::: jars2).filterNot(path => contexts.exists(_.is_module(path)))
val source_files =
(for {
context <- contexts.iterator
- file <- context.sources.asScala.iterator
- if file.endsWith(".scala") || file.endsWith(".java")
- } yield File.path(context.path(file).toFile)).toList
+ path <- context.sources.iterator
+ if path.is_scala || path.is_java
+ } yield path).toList
(jar_files, source_files)
}
@@ -63,10 +51,9 @@
lazy val isabelle_scala_files: Map[String, Path] =
{
val context = Scala_Build.context(Path.ISABELLE_HOME, component = true)
- context.sources().asScala.iterator.foldLeft(Map.empty[String, Path]) {
- case (map, name) =>
- if (name.endsWith(".scala")) {
- val path = File.path(context.path(name).toFile)
+ context.sources.iterator.foldLeft(Map.empty[String, Path]) {
+ case (map, path) =>
+ if (path.is_scala) {
val base = path.base.implode
map.get(base) match {
case None => map + (base -> path)
@@ -107,13 +94,12 @@
def package_dir(source_file: Path): Option[Path] =
{
- val is_java = source_file.file_name.endsWith(".java")
val lines = split_lines(File.read(source_file))
val Package = """\s*\bpackage\b\s*(?:object\b\s*)?((?:\w|\.)+)\b.*""".r
lines.collectFirst(
{
case Package(name) =>
- if (is_java) Path.explode(space_explode('.', name).mkString("/"))
+ if (source_file.is_java) Path.explode(space_explode('.', name).mkString("/"))
else Path.basic(name)
})
}
@@ -136,7 +122,7 @@
isabelle_scala_files
for (source <- source_files) {
- val dir = if (source.file_name.endsWith(".java")) java_src_dir else scala_src_dir
+ val dir = if (source.is_java) java_src_dir else scala_src_dir
val target = dir + the_package_dir(source)
Isabelle_System.make_directory(target)
if (symlinks) Isabelle_System.symlink(source, target)
--- a/src/Tools/jEdit/src/main.scala Sat Jul 24 13:09:48 2021 +0200
+++ b/src/Tools/jEdit/src/main.scala Sat Jul 24 15:38:41 2021 +0200
@@ -82,7 +82,7 @@
</PERSPECTIVE>""")
}
- Scala_Project.plugin_contexts().foreach(isabelle.setup.Build.build(_, false))
+ Scala_Project.plugin_contexts().foreach(_.build())
/* args */