# HG changeset patch
# User wenzelm
# Date 1660935854 -7200
# Node ID 540aad9405b15f913f6d27443f5aea9803827a61
# Parent  4d5221c51f8e9c5d086fbcf3cc918d06ccfa5d27
more robust;

diff -r 4d5221c51f8e -r 540aad9405b1 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Aug 19 20:59:29 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Fri Aug 19 21:04:14 2022 +0200
@@ -124,8 +124,8 @@
   object Entity_Ref {
     def unapply(props: Properties.T): Option[(String, String, String)] =
       (props, props, props, props) match {
-        case (Markup.Entity.Ref.Prop(_), Position.Def_File(file), Markup.Kind(kind), Markup.Name(name)) =>
-          Some((file, kind, name))
+        case (Markup.Entity.Ref.Prop(_), Position.Def_File(file), Markup.Kind(kind), Markup.Name(name))
+        if Path.is_wellformed(file) => Some((file, kind, name))
         case _ => None
       }
   }