equal
deleted
inserted
replaced
160 } yield path).toList |
160 } yield path).toList |
161 |
161 |
162 (jars, sources) |
162 (jars, sources) |
163 } |
163 } |
164 |
164 |
165 lazy val isabelle_scala_files: Map[String, Path] = { |
165 lazy val isabelle_scala_files: Map[String, Path] = |
166 val context = Scala_Build.context(Path.ISABELLE_HOME, component = true) |
166 Scala_Build.context(Path.ISABELLE_HOME, component = true) |
167 context.sources.iterator.foldLeft(Map.empty[String, Path]) { |
167 .sources.iterator.foldLeft(Map.empty[String, Path]) { |
168 case (map, path) => |
168 case (map, path) => |
169 if (path.is_scala) { |
169 if (path.is_scala) { |
170 val base = path.base.implode |
170 val base = path.base.implode |
171 map.get(base) match { |
171 map.get(base) match { |
172 case None => map + (base -> path) |
172 case None => map + (base -> path) |
173 case Some(path2) => error("Conflicting base names: " + path + " vs. " + path2) |
173 case Some(path2) => error("Conflicting base names: " + path + " vs. " + path2) |
|
174 } |
174 } |
175 } |
175 } |
176 else map |
176 else map |
177 } |
177 } |
|
178 } |
|
179 |
178 |
180 |
179 |
181 /* compile-time position */ |
180 /* compile-time position */ |
182 |
181 |
183 def here: Here = { |
182 def here: Here = { |