author | wenzelm |
Sat, 14 Jan 2023 19:47:02 +0100 | |
changeset 76971 | d1776c5ddc93 |
parent 76970 | 7d23555fda83 |
child 76972 | 6c542f2aab85 |
--- 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)) }