--- 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) =