# HG changeset patch
# User wenzelm
# Date 1674136645 -3600
# Node ID 87552565d1a514f0128812bac66f939fde4a9d98
# Parent  9107e103754ce8491791058580ae22a458d9a376
tuned signature;

diff -r 9107e103754c -r 87552565d1a5 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Thu Jan 19 11:46:21 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Thu Jan 19 14:57:25 2023 +0100
@@ -779,27 +779,70 @@
     }
   }
 
-  object Cite_Parsers extends Parse.Parsers {
-    val keywords: Keyword.Keywords = Thy_Header.bootstrap_keywords + "in" + "and" + "using"
-
-    val location: Parser[String] = embedded ~ $$$("in") ^^ { case x ~ _ => x } | success("")
-    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))))
-      }
-  }
-
 
   /* parse within raw source */
 
+  object Cite {
+    object Parsers extends Parse.Parsers {
+      val keywords: Keyword.Keywords = Thy_Header.bootstrap_keywords + "in" + "and" + "using"
+
+      val location: Parser[String] = embedded ~ $$$("in") ^^ { case x ~ _ => x } | success("")
+      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 parse(
+      cite_commands: List[String],
+      text: String,
+      start: Isar_Token.Pos = Isar_Token.Pos.start
+    ): List[Cite] = {
+      val controls = cite_commands.map(s => Symbol.control_prefix + s + Symbol.control_suffix)
+      val special = (controls ::: controls.map(Symbol.decode)).toSet
+
+      val Parsers = Antiquote.Parsers
+      Parsers.parseAll(Parsers.rep(Parsers.antiquote_special(special)), text) match {
+        case Parsers.Success(ants, _) =>
+          var pos = start
+          val result = new mutable.ListBuffer[Cite]
+          for (ant <- ants) {
+            ant match {
+              case Antiquote.Control(source) =>
+                for {
+                  head <- Symbol.iterator(source).nextOption
+                  kind <- Symbol.control_name(Symbol.encode(head))
+                } {
+                  val rest = source.substring(head.length)
+                  val (body, pos1) =
+                    if (rest.isEmpty) (rest, pos)
+                    else (Scan.Parsers.cartouche_content(rest), pos.advance(Symbol.open))
+                  result += Cite(kind, body, pos1)
+                }
+              case _ =>
+            }
+            pos = pos.advance(ant.source)
+          }
+          result.toList
+        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 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))
@@ -811,45 +854,4 @@
       if (nocite_latex.nonEmpty) Nil
       else List("Malformed citation" + Position.here(position))
   }
-
-  def parse_citations(
-    cite_commands: List[String],
-    text: String,
-    start: Isar_Token.Pos = Isar_Token.Pos.start
-  ): List[Cite] = {
-    val controls = cite_commands.map(s => Symbol.control_prefix + s + Symbol.control_suffix)
-    val special = (controls ::: controls.map(Symbol.decode)).toSet
-
-    val Parsers = Antiquote.Parsers
-    Parsers.parseAll(Parsers.rep(Parsers.antiquote_special(special)), text) match {
-      case Parsers.Success(ants, _) =>
-        var pos = start
-        val result = new mutable.ListBuffer[Cite]
-        for (ant <- ants) {
-          ant match {
-            case Antiquote.Control(source) =>
-              for {
-                head <- Symbol.iterator(source).nextOption
-                kind <- Symbol.control_name(Symbol.encode(head))
-              } {
-                val rest = source.substring(head.length)
-                val (body, pos1) =
-                  if (rest.isEmpty) (rest, pos)
-                  else (Scan.Parsers.cartouche_content(rest), pos.advance(Symbol.open))
-                result += Cite(kind, body, pos1)
-              }
-            case _ =>
-          }
-          pos = pos.advance(ant.source)
-        }
-        result.toList
-      case _ => error("Unexpected failure parsing special antiquotations:\n" + text)
-    }
-  }
-
-  def parse_citations_latex(
-    cite_commands: List[String],
-    text: String,
-    start: Isar_Token.Pos = Isar_Token.Pos.start
-  ): Latex.Text = parse_citations(cite_commands, text, start = start).flatMap(_.nocite_latex)
 }