more robust isabelle_scala_files;
authorwenzelm
Sat, 28 Nov 2020 20:18:29 +0100
changeset 72762 d9a54c4c9da9
parent 72761 4519eeefe3b5
child 72763 3cc73d00553c
more robust isabelle_scala_files; clarified evaluation;
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) =