--- 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 */
--- a/src/Pure/Thy/latex.scala Sun Nov 14 15:21:40 2021 +0100
+++ b/src/Pure/Thy/latex.scala Sun Nov 14 15:42:38 2021 +0100
@@ -37,18 +37,16 @@
def traverse(body: XML.Body): Unit =
{
body.foreach {
- case XML.Wrapped_Elem(_, _, _) =>
- case XML.Elem(markup, body) =>
- if (markup.name == Markup.DOCUMENT_LATEX) {
- for { l <- Position.Line.unapply(markup.properties) if positions.nonEmpty } {
- val s = position(Value.Int(line), Value.Int(l))
- if (positions.last != s) positions += s
- }
- traverse(body)
- }
case XML.Text(s) =>
line += s.count(_ == '\n')
result += s
+ case XML.Elem(Markup.Document_Latex(props), body) =>
+ for { l <- Position.Line.unapply(props) if positions.nonEmpty } {
+ val s = position(Value.Int(line), Value.Int(l))
+ if (positions.last != s) positions += s
+ }
+ traverse(body)
+ case _: XML.Elem =>
}
}
traverse(latex_text)