# HG changeset patch
# User wenzelm
# Date 1606591109 -3600
# Node ID d9a54c4c9da9d118335a611c50fb28e106a4f32a
# Parent  4519eeefe3b5337125f9db518b4014914a2a7b99
more robust isabelle_scala_files;
clarified evaluation;

diff -r 4519eeefe3b5 -r d9a54c4c9da9 src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Sat Nov 28 20:14:46 2020 +0100
+++ b/src/Pure/Tools/scala_project.scala	Sat Nov 28 20:18:29 2020 +0100
@@ -23,7 +23,7 @@
 
   /* file and directories */
 
-  def isabelle_files(): List[String] =
+  lazy val isabelle_files: List[String] =
   {
     val files1 =
     {
@@ -51,6 +51,20 @@
     files1 ::: files2
   }
 
+  lazy val isabelle_scala_files: Map[String, Path] =
+    (Map.empty[String, Path] /: isabelle_files)({
+      case (map, name) =>
+        if (!name.startsWith("src/Tools/jEdit/") && name.endsWith(".scala")) {
+          val path = Path.explode("~~/" + name)
+          val base = path.base.implode
+          map.get(base) match {
+            case None => map + (base -> path)
+            case Some(path1) => error("Conflicting base names: " + path + " vs. " + path1)
+          }
+        }
+        else map
+    })
+
   val isabelle_dirs: List[(String, Path)] =
     List(
       "src/Pure/" -> Path.explode("isabelle"),
@@ -80,16 +94,10 @@
   {
     override def toString: String = name + ":" + line
     def position: Position.T =
-    {
-      if (name.startsWith("<")) Position.none
-      else {
-        val suffix = "/" + name
-        isabelle_files().find(_.endsWith(suffix)) match {
-          case None => Position.none
-          case Some(file) => Position.Line_File(line, "$ISABELLE_HOME/" + file)
-        }
+      isabelle_scala_files.get(name) match {
+        case Some(path) => Position.Line_File(line, path.implode)
+        case None => Position.none
       }
-    }
   }
 
 
@@ -109,7 +117,8 @@
 
     Isabelle_System.copy_dir(Path.explode("~~/src/Tools/jEdit/dist/jEdit"), java_src_dir)
 
-    val files = isabelle_files()
+    val files = isabelle_files
+    isabelle_scala_files
 
     for (file <- files if file.endsWith(".scala")) {
       val (path, target) =