# HG changeset patch
# User wenzelm
# Date 1626550275 -7200
# Node ID 39e05601faebe1a44cc7e96e1d40a0ad74d3285d
# Parent  0701ff55780d7250bbc34c66eaa24ebb6c661094
more accurate scala_project, based on build.props of components;

diff -r 0701ff55780d -r 39e05601faeb Admin/components/components.sha1
--- a/Admin/components/components.sha1	Sat Jul 17 13:42:21 2021 +0200
+++ b/Admin/components/components.sha1	Sat Jul 17 21:31:15 2021 +0200
@@ -128,6 +128,7 @@
 d2c9fd7b73457a460111edd6eb93a133272935fb  isabelle_setup-20210715.tar.gz
 a5f478ba1088f67c2c86dc2fa7764b6d884e5ae5  isabelle_setup-20210716-1.tar.gz
 79fad009cb22aa5e7cb4aed3c810ad5f61790293  isabelle_setup-20210716.tar.gz
+692a39f716998e556ec9559c9ca362fc8fc9d5b6  isabelle_setup-20210717-1.tar.gz
 14f8508bcae9140815bb23e430e26d2cbc504b81  isabelle_setup-20210717.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544  jdk-11+28.tar.gz
 e12574d838ed55ef2845acf1152329572ab0cc56  jdk-11.0.10+9.tar.gz
@@ -173,6 +174,7 @@
 2ac389babd15aa5ddd1a424c1509e1c459e6fbb1  jdk-8u72.tar.gz
 caa0cf65481b6207f66437576643f41dabae3c83  jdk-8u92.tar.gz
 778fd85c827ec49d2d658a832d20e63916186b0d  jedit-20210715.tar.gz
+beb99f2cb0bd4e595c5c597d3970c46aa21616e4  jedit-20210717.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0  jedit_build-20111217.tar.gz
 a242a688810f2bccf24587b0062ce8027bf77fa2  jedit_build-20120304.tar.gz
 4c948dee53f74361c097c08f49a1a5ff9b17bd1d  jedit_build-20120307.tar.gz
diff -r 0701ff55780d -r 39e05601faeb Admin/components/main
--- a/Admin/components/main	Sat Jul 17 13:42:21 2021 +0200
+++ b/Admin/components/main	Sat Jul 17 21:31:15 2021 +0200
@@ -8,9 +8,9 @@
 flatlaf-1.2
 idea-icons-20210508
 isabelle_fonts-20210322
-isabelle_setup-20210717
+isabelle_setup-20210717-1
 jdk-15.0.2+7
-jedit-20210715
+jedit-20210717
 jfreechart-1.5.1
 jortho-1.0-2
 kodkodi-1.5.6-1
diff -r 0701ff55780d -r 39e05601faeb Admin/lib/Tools/build_setup
--- a/Admin/lib/Tools/build_setup	Sat Jul 17 13:42:21 2021 +0200
+++ b/Admin/lib/Tools/build_setup	Sat Jul 17 21:31:15 2021 +0200
@@ -48,17 +48,39 @@
 [ -d "$COMPONENT_DIR" ] && fail "Directory already exists: \"$COMPONENT_DIR\""
 
 
+# etc/settings
+
+mkdir -p "$COMPONENT_DIR/etc"
+cat > "$COMPONENT_DIR/etc/settings" <<EOF
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_SETUP_JAR="\$COMPONENT/lib/isabelle_setup.jar"
+classpath "\$ISABELLE_SETUP_JAR"
+EOF
+
+BUILD_PROPS="$COMPONENT_DIR/etc/build.props"
+echo >> "$BUILD_PROPS" "no_module = lib/isabelle_setup.jar"
+
+
 # build jar
 
+SOURCE_DIR="$COMPONENT_DIR/src"
 TARGET_DIR="$COMPONENT_DIR/lib"
-mkdir -p "$TARGET_DIR/isabelle/setup"
+mkdir -p "$SOURCE_DIR" "$TARGET_DIR/isabelle/setup"
 
 declare -a ARGS=("-Xlint:unchecked")
+echo -n >> "$BUILD_PROPS" "sources ="
+
 for SRC in "${SOURCES[@]}"
 do
   ARGS["${#ARGS[@]}"]="$(platform_path "$ISABELLE_HOME/src/Tools/Setup/isabelle/setup/$SRC")"
+  cp "$ISABELLE_HOME/src/Tools/Setup/isabelle/setup/$SRC" "$SOURCE_DIR"
+  echo >> "$BUILD_PROPS" " \\"
+  echo -n >> "$BUILD_PROPS" "  src/$SRC"
 done
 
+echo >> "$BUILD_PROPS"
+
 isabelle_jdk javac $ISABELLE_JAVAC_OPTIONS -d "$TARGET_DIR" \
   -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "${ARGS[@]}" || \
   fail "Failed to compile sources"
@@ -69,17 +91,6 @@
 rm -rf "$TARGET_DIR/isabelle"
 
 
-# etc/settings
-
-mkdir -p "$COMPONENT_DIR/etc"
-cat > "$COMPONENT_DIR/etc/settings" <<EOF
-# -*- shell-script -*- :mode=shellscript:
-
-ISABELLE_SETUP_JAR="\$COMPONENT/lib/isabelle_setup.jar"
-classpath "\$ISABELLE_SETUP_JAR"
-EOF
-
-
 # README
 
 cat > "$COMPONENT_DIR/README" <<EOF
diff -r 0701ff55780d -r 39e05601faeb src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala	Sat Jul 17 13:42:21 2021 +0200
+++ b/src/Pure/Admin/build_jedit.scala	Sat Jul 17 21:31:15 2021 +0200
@@ -115,6 +115,8 @@
 
     Isabelle_System.new_directory(component_dir)
 
+    val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
+
 
     /* jEdit directory */
 
@@ -177,6 +179,21 @@
       progress.bash("env JAVA_HOME=" + File.bash_platform_path(java_home) + " ant",
         cwd = tmp_source_dir.file, echo = true).check
       Isabelle_System.copy_file(tmp_source_dir + Path.explode("build/jedit.jar"), jedit_patched_dir)
+
+      val java_sources =
+        File.find_files(source_dir.file, file => file.getName.endsWith(".java")).
+          flatMap(file =>
+            {
+              if (Scala_Project.package_dir(File.path(file)).isDefined) {
+                Some(File.path(component_dir.java_path.relativize(file.toPath).toFile))
+              }
+              else None
+            })
+
+      File.write(etc_dir + Path.explode("build.props"),
+        "no_module = " + jedit_patched + "/jedit.jar\n" +
+        "requirements = env:JEDIT_JARS\n" +
+        ("sources =" :: java_sources.map(p => "  " + p.implode)).mkString("", " \\\n", "\n"))
     })
 
 
@@ -459,9 +476,7 @@
     if (!original) Isabelle_System.rm_tree(jedit_dir)
 
 
-    /* etc */
-
-    val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
+    /* settings */
 
     File.write(etc_dir + Path.explode("settings"),
       """# -*- shell-script -*- :mode=shellscript:
diff -r 0701ff55780d -r 39e05601faeb src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Sat Jul 17 13:42:21 2021 +0200
+++ b/src/Pure/Tools/scala_project.scala	Sat Jul 17 21:31:15 2021 +0200
@@ -6,6 +6,8 @@
 
 package isabelle
 
+import scala.jdk.CollectionConverters._
+
 
 object Scala_Project
 {
@@ -23,51 +25,52 @@
 
   /* file and directories */
 
-  lazy val isabelle_files: List[String] =
+  lazy val isabelle_files: (List[Path], List[Path]) =
   {
-    val files1 =
-    {
-      val isabelle_home = Path.ISABELLE_HOME.canonical
-      Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH")).
-        map(path => File.relative_path(isabelle_home, path).getOrElse(path).implode)
-    }
+    val component_contexts =
+      isabelle.setup.Build.component_contexts().asScala.toList
+
+    val jars1 = Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH"))
+    val jars2 =
+      (for {
+        context <- component_contexts.iterator
+        s <- context.requirements().asScala.iterator
+        path <- context.requirement_paths(s).asScala.iterator
+      } yield File.path(path.toFile)).toList
 
-    val isabelle_jar = Path.explode("$ISABELLE_SCALA_JAR").java_path
-    val isabelle_shasum = isabelle.setup.Build.get_shasum(isabelle_jar)
+    val jar_files =
+      (jars1 ::: jars2).filterNot(path =>
+        component_contexts.exists(context =>
+        {
+          val name: String = context.module_name()
+          name.nonEmpty && File.eq(context.path(name).toFile, path.file)
+        }))
 
-    val files2 =
-      for {
-        line <- Library.trim_split_lines(isabelle_shasum)
-        name =
-          if (line.length > 41 && line(40) == ' ') line.substring(41)
-          else error("Bad shasum entry: " + quote(line))
-        if Path.is_wellformed(name) && name != "<props>"
-      } yield name
+    val source_files =
+      (for {
+        context <- component_contexts.iterator
+        file <- context.sources.asScala.iterator
+        if file.endsWith(".scala") || file.endsWith(".java")
+      } yield File.path(context.path(file).toFile)).toList
 
-    files1 ::: files2
+    (jar_files, source_files)
   }
 
   lazy val isabelle_scala_files: Map[String, Path] =
-    isabelle_files.foldLeft(Map.empty[String, Path]) {
+  {
+    val context = isabelle.setup.Build.component_context(Path.ISABELLE_HOME.java_path)
+    context.sources().asScala.iterator.foldLeft(Map.empty[String, Path]) {
       case (map, name) =>
-        if (!name.startsWith("src/Tools/jEdit/") && name.endsWith(".scala")) {
-          val path = Path.explode("~~/" + name)
-          val base = path.base.implode
+        if (name.endsWith(".scala")) {
+        val path = File.path(context.path(name).toFile)
+        val base = path.base.implode
           map.get(base) match {
             case None => map + (base -> path)
-            case Some(path1) => error("Conflicting base names: " + path + " vs. " + path1)
+            case Some(path2) => error("Conflicting base names: " + path + " vs. " + path2)
           }
         }
         else map
     }
-
-  private def guess_package(path: Path): String =
-  {
-    val lines = split_lines(File.read(path))
-    val Package = """\bpackage\b +(?:object +)?\b((?:\w|\.)+)\b""".r
-
-    lines.collectFirst({ case Package(name) => name }) getOrElse
-      error("Failed to guess package from " + path)
   }
 
 
@@ -98,6 +101,22 @@
 
   /* scala project */
 
+  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("/"))
+          else Path.basic(name)
+      })
+  }
+
+  def the_package_dir(source_file: Path): Path =
+    package_dir(source_file) getOrElse error("Failed to guess package from " + source_file)
+
   def scala_project(project_dir: Path, symlinks: Boolean = false): Unit =
   {
     if (symlinks && Platform.is_windows)
@@ -106,33 +125,20 @@
     if (project_dir.is_file || project_dir.is_dir)
       error("Project directory already exists: " + project_dir)
 
-    val java_src_dir = project_dir + Path.explode("src/main/java")
+    val java_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/java"))
     val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala"))
 
-    Isabelle_System.copy_dir(Path.explode("$JEDIT_HOME/jEdit"), java_src_dir)
-
-    val isabelle_setup_dir = Path.explode("~~/src/Tools/Setup/isabelle")
-    if (symlinks) Isabelle_System.symlink(isabelle_setup_dir, java_src_dir)
-    else Isabelle_System.copy_dir(isabelle_setup_dir, java_src_dir)
-
-    val files = isabelle_files
+    val (jar_files, source_files) = isabelle_files
     isabelle_scala_files
 
-    for (file <- files if file.endsWith(".scala")) {
-      val path = Path.ISABELLE_HOME + Path.explode(file)
-      val target = scala_src_dir + Path.basic(guess_package(path))
+    for (source <- source_files) {
+      val dir = if (source.file_name.endsWith(".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(path, target)
-      else Isabelle_System.copy_file(path, target)
+      if (symlinks) Isabelle_System.symlink(source, target)
+      else Isabelle_System.copy_file(source, target)
     }
 
-    val jars =
-      for (file <- files if file.endsWith(".jar"))
-      yield {
-        if (file.startsWith("/")) file
-        else Isabelle_System.getenv("ISABELLE_HOME") + "/" + file
-      }
-
     File.write(project_dir + Path.explode("settings.gradle"), "rootProject.name = 'Isabelle'\n")
     File.write(project_dir + Path.explode("build.gradle"),
 """plugins {
@@ -146,7 +152,7 @@
 dependencies {
   implementation 'org.scala-lang:scala-library:""" + scala.util.Properties.versionNumberString + """'
   compile files(
-    """ + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n    ", ")") +
+    """ + jar_files.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n    ", ")") +
 """
 }
 """)
diff -r 0701ff55780d -r 39e05601faeb src/Tools/Setup/isabelle/setup/Build.java
--- a/src/Tools/Setup/isabelle/setup/Build.java	Sat Jul 17 13:42:21 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build.java	Sat Jul 17 21:31:15 2021 +0200
@@ -121,7 +121,15 @@
             else return title;
         }
 
+        public String no_module() { return _props.getProperty("no_module", ""); }
         public String module() { return _props.getProperty("module", ""); }
+        public String module_name() {
+            if (!module().isEmpty() && !no_module().isEmpty()) {
+              throw new RuntimeException(error_message("Conflict of module and no_module"));
+            }
+            if (!module().isEmpty()) { return module(); }
+            else { return no_module(); }
+        }
         public String scalac_options() { return _props.getProperty("scalac_options", ""); }
         public String javac_options() { return _props.getProperty("javac_options", ""); }
         public String main() { return _props.getProperty("main", ""); }
@@ -155,6 +163,22 @@
             return Files.exists(path(file));
         }
 
+        public List<Path> requirement_paths(String s)
+            throws IOException, InterruptedException
+        {
+            if (s.startsWith("env:")) {
+                List<Path> paths = new LinkedList<Path>();
+                for (String p : Environment.getenv(s.substring(4)).split(":", -1)) {
+                    if (!p.isEmpty()) {
+                        Path path = Path.of(Environment.platform_path(p));
+                        paths.add(path);
+                    }
+                }
+                return List.copyOf(paths);
+            }
+            else { return List.of(path(s)); }
+        }
+
         public String item_name(String s)
         {
             int i = s.indexOf(':');
@@ -454,21 +478,9 @@
                     StringBuilder _shasum = new StringBuilder();
                     _shasum.append(context.shasum_props());
                     for (String s : requirements) {
-                        if (s.startsWith("env:")) {
-                            List<Path> paths = new LinkedList<Path>();
-                            for (String p : Environment.getenv(s.substring(4)).split(":", -1)) {
-                                if (!p.isEmpty()) {
-                                    Path path = Path.of(Environment.platform_path(p));
-                                    compiler_deps.add(path);
-                                    paths.add(path);
-                                }
-                            }
-                            _shasum.append(context.shasum(s, paths));
-                        }
-                        else {
-                            compiler_deps.add(context.path(s));
-                            _shasum.append(context.shasum(s));
-                        }
+                        List<Path> paths = context.requirement_paths(s);
+                        compiler_deps.addAll(paths);
+                        _shasum.append(context.shasum(s, paths));
                     }
                     for (String s : resources) {
                         _shasum.append(context.shasum(context.item_name(s)));