diff -r fd8d82c4433b -r 6aae62f55c2b src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Dec 07 16:09:06 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Dec 07 16:24:39 2020 +0100
@@ -194,6 +194,15 @@
           }
         case _ => None
       }
+
+    object Path
+    {
+      def unapply(markup: Markup): Option[Boolean] =
+        markup match {
+          case Language(PATH, _, _, delimited) => Some(delimited)
+          case _ => None
+        }
+    }
   }