src/Pure/General/path.scala

   def expand: Path = expand_env(Isabelle_System.settings())
 
   def file_name: String = expand.base.implode
 
 
-  /* source position */
-
-  def position: Position.T = Position.File(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)
+  }
+
+  def position: Position.T = Position.File(implode_symbolic)
 
 
   /* platform files */
 
   def file: JFile = File.platform_file(this)