# HG changeset patch
# User wenzelm
# Date 1606682535 -3600
# Node ID ed75dde8061a81ebc05147aef9b95646a7220a33
# Parent  fbee4d09a221cd92997bbab7014cc06168189459
Path.implode_symbolic as in ML;

diff -r fbee4d09a221 -r ed75dde8061a src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sun Nov 29 21:09:46 2020 +0100
+++ b/src/Pure/General/path.scala	Sun Nov 29 21:42:15 2020 +0100
@@ -257,9 +257,27 @@
   def file_name: String = expand.base.implode
 
 
-  /* source position */
+  /* implode wrt. given directories */
 
-  def position: Position.T = Position.File(implode)
+  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)
+  }
+
+  def position: Position.T = Position.File(implode_symbolic)
 
 
   /* platform files */