# HG changeset patch
# User wenzelm
# Date 1673722022 -3600
# Node ID d1776c5ddc93e6f3cc8bc228a4a2b332034dcf8c
# Parent  7d23555fda8354c8f3cae7e59752d56b24036087
more operations: use proper constants;

diff -r 7d23555fda83 -r d1776c5ddc93 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Jan 14 19:36:02 2023 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Jan 14 19:47:02 2023 +0100
@@ -217,7 +217,9 @@
   ) {
     override def toString: String = name
 
-    def is_path: Boolean = name == PATH
+    def is_document: Boolean = name == Language.DOCUMENT
+    def is_path: Boolean = name == Language.PATH
+
     def description: String = Word.implode(Word.explode('_', name))
   }