src/Pure/Thy/bibtex.scala

--- a/src/Pure/Thy/bibtex.scala	Thu Jan 19 14:57:25 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Thu Jan 19 15:51:09 2023 +0100
@@ -783,6 +783,44 @@
   /* parse within raw source */
 
   object Cite {
+    def unapply(tree: XML.Tree): Option[Inner] =
+      tree match {
+        case XML.Elem(Markup(Markup.Latex_Cite.name, props), body) =>
+          val kind = Markup.Kind.unapply(props).getOrElse(CITE)
+          val citations = Markup.Citations.get(props)
+          val pos = props.filter(Markup.position_property)
+          Some(Inner(kind, citations, body, pos))
+        case _ => None
+      }
+
+    sealed case class Inner(kind: String, citation: String, location: XML.Body, pos: Position.T) {
+      def nocite: Inner = copy(kind = NOCITE, location = Nil)
+
+      override def toString: String = citation
+    }
+
+    sealed case class Outer(kind: String, body: String, start: Isar_Token.Pos) {
+      def pos: Position.T = start.position()
+
+      def parse: Option[Inner] = {
+        val tokens = Isar_Token.explode(Parsers.keywords, body)
+        Parsers.parse_all(Parsers.inner(pos), Isar_Token.reader(tokens, start)) match {
+          case Parsers.Success(res, _) => Some(res)
+          case _ => None
+        }
+      }
+
+      def errors: List[String] =
+        if (parse.isDefined) Nil
+        else List("Malformed citation" + Position.here(pos))
+
+      override def toString: String =
+        parse match {
+          case Some(inner) => inner.toString
+          case None => "<malformed>"
+        }
+    }
+
     object Parsers extends Parse.Parsers {
       val keywords: Keyword.Keywords = Thy_Header.bootstrap_keywords + "in" + "and" + "using"
 
@@ -790,17 +828,16 @@
       val citations: Parser[String] = rep1sep(name, $$$("and")) ^^ (x => x.mkString(","))
       val kind: Parser[String] = $$$("using") ~! name ^^ { case _ ~ x => x } | success(CITE)
 
-      val nocite: Parser[Latex.Text] =
-        location ~ citations ~ kind ^^ { case _ ~ x ~ _ =>
-          List(XML.elem(Markup.Latex_Cite(Markup.Kind(NOCITE) ::: Markup.Citations(x))))
-        }
+      def inner(pos: Position.T): Parser[Inner] =
+        location ~ citations ~ kind ^^
+          { case x ~ y ~ z => Inner(z, y, XML.string(x), pos) }
     }
 
     def parse(
       cite_commands: List[String],
       text: String,
       start: Isar_Token.Pos = Isar_Token.Pos.start
-    ): List[Cite] = {
+    ): List[Outer] = {
       val controls = cite_commands.map(s => Symbol.control_prefix + s + Symbol.control_suffix)
       val special = (controls ::: controls.map(Symbol.decode)).toSet
 
@@ -808,7 +845,7 @@
       Parsers.parseAll(Parsers.rep(Parsers.antiquote_special(special)), text) match {
         case Parsers.Success(ants, _) =>
           var pos = start
-          val result = new mutable.ListBuffer[Cite]
+          val result = new mutable.ListBuffer[Outer]
           for (ant <- ants) {
             ant match {
               case Antiquote.Control(source) =>
@@ -820,7 +857,7 @@
                   val (body, pos1) =
                     if (rest.isEmpty) (rest, pos)
                     else (Scan.Parsers.cartouche_content(rest), pos.advance(Symbol.open))
-                  result += Cite(kind, body, pos1)
+                  result += Outer(kind, body, pos1)
                 }
               case _ =>
             }
@@ -830,28 +867,5 @@
         case _ => error("Unexpected failure parsing special antiquotations:\n" + text)
       }
     }
-
-    def parse_latex(
-      cite_commands: List[String],
-      text: String,
-      start: Isar_Token.Pos = Isar_Token.Pos.start
-    ): Latex.Text = parse(cite_commands, text, start = start).flatMap(_.nocite_latex)
-  }
-
-  sealed case class Cite(kind: String, body: String, pos: Isar_Token.Pos) {
-    def position: Position.T = pos.position()
-
-    def nocite_latex: Latex.Text = {
-      val Parsers = Cite.Parsers
-      val tokens = Isar_Token.explode(Parsers.keywords, body)
-      Parsers.parse_all(Parsers.nocite, Isar_Token.reader(tokens, pos)) match {
-        case Parsers.Success(nocite, _) => List(XML.Elem(Markup.Latex_Output(position), nocite))
-        case _ => Nil
-      }
-    }
-
-    def errors: List[String] =
-      if (nocite_latex.nonEmpty) Nil
-      else List("Malformed citation" + Position.here(position))
   }
 }