# HG changeset patch
# User wenzelm
# Date 1674139869 -3600
# Node ID a19ea85409cdc770f700cefe4564470ac853487d
# Parent  87552565d1a514f0128812bac66f939fde4a9d98
clarified signature;

diff -r 87552565d1a5 -r a19ea85409cd 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))
   }
 }
diff -r 87552565d1a5 -r a19ea85409cd src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Thu Jan 19 14:57:25 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Thu Jan 19 15:51:09 2023 +0100
@@ -46,21 +46,6 @@
     else name
 
 
-  /* cite: references to bibliography */
-
-  object Cite {
-    sealed case class Value(kind: String, citation: String, location: XML.Body)
-    def unapply(tree: XML.Tree): Option[Value] =
-      tree match {
-        case XML.Elem(Markup(Markup.Latex_Cite.name, props), body) =>
-          val kind = Markup.Kind.unapply(props).getOrElse(Bibtex.CITE)
-          val citations = Markup.Citations.get(props)
-          Some(Value(kind, citations, body))
-        case _ => None
-      }
-  }
-
-
   /* index entries */
 
   def index_escape(str: String): String = {
@@ -235,11 +220,15 @@
       }
     }
 
-    def cite(value: Cite.Value): Text = {
-      latex_macro0(value.kind) :::
-      (if (value.location.isEmpty) Nil
-       else XML.string("[") ::: value.location ::: XML.string("]")) :::
-      XML.string("{" + value.citation + "}")
+    def cite(inner: Bibtex.Cite.Inner): Text = {
+      val body =
+        latex_macro0(inner.kind) :::
+        (if (inner.location.isEmpty) Nil
+         else XML.string("[") ::: inner.location ::: XML.string("]")) :::
+        XML.string("{" + inner.citation + "}")
+
+      if (inner.pos.isEmpty) body
+      else List(XML.Elem(Markup.Latex_Output(inner.pos), body))
     }
 
     def index_item(item: Index_Item.Value): String = {
@@ -299,7 +288,7 @@
                 case Markup.Latex_Tag(name) => latex_tag(name, body)
                 case Markup.Latex_Cite(_) =>
                   elem match {
-                    case Cite(value) => cite(value)
+                    case Bibtex.Cite(inner) => cite(inner)
                     case _ => unknown_elem(elem, file_position)
                   }
                 case Markup.Latex_Index_Entry(_) =>