--- a/src/Pure/General/path.scala Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Pure/General/path.scala Tue Jan 03 16:05:07 2023 +0100
@@ -293,26 +293,6 @@
def file_name: String = expand.base.implode
- /* implode wrt. given directories */
-
- def implode_symbolic: String = {
- val directories =
- Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
- val full_name = expand.implode
- directories.view.flatMap(a =>
- try {
- val b = Path.explode(a).expand.implode
- if (full_name == b) Some(a)
- else {
- Library.try_unprefix(b + "/", full_name) match {
- case Some(name) => Some(a + "/" + name)
- case None => None
- }
- }
- } catch { case ERROR(_) => None }).headOption.getOrElse(implode)
- }
-
-
/* platform files */
def file: JFile = File.platform_file(this)