--- a/src/Pure/PIDE/markup.scala Sun Nov 14 15:21:40 2021 +0100
+++ b/src/Pure/PIDE/markup.scala Sun Nov 14 15:42:38 2021 +0100
@@ -61,6 +61,13 @@
val Empty: Markup = Markup("", Nil)
val Broken: Markup = Markup("broken", Nil)
+ class Markup_Elem(val name: String)
+ {
+ def apply(props: Properties.T = Nil): Markup = Markup(name, props)
+ def unapply(markup: Markup): Option[Properties.T] =
+ if (markup.name == name) Some(markup.properties) else None
+ }
+
class Markup_String(val name: String, prop: String)
{
val Prop: Properties.String = new Properties.String(prop)
@@ -359,7 +366,7 @@
val UNIMPORTANT = "unimportant"
}
- val DOCUMENT_LATEX = "document_latex"
+ val Document_Latex = new Markup_Elem("document_latex")
/* Markdown document structure */