more robust;
authorwenzelm
Fri, 19 Aug 2022 21:04:14 +0200
changeset 75913 540aad9405b1
parent 75912 4d5221c51f8e
child 75914 4da80799352f
more robust;
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
       }
   }