# HG changeset patch
# User wenzelm
# Date 1627133921 -7200
# Node ID fb8d5c0133c98ac2ed9301e517adeb43ece97a86
# Parent  0ee44ed80290b618dd573bb22ba6b8ab4b726847
clarified signature;

diff -r 0ee44ed80290 -r fb8d5c0133c9 src/Pure/General/path.scala
--- 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 {
diff -r 0ee44ed80290 -r fb8d5c0133c9 src/Pure/Tools/scala_build.scala
--- 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(_))
 }
diff -r 0ee44ed80290 -r fb8d5c0133c9 src/Pure/Tools/scala_project.scala
--- 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)
diff -r 0ee44ed80290 -r fb8d5c0133c9 src/Tools/jEdit/src/main.scala
--- 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 */