# HG changeset patch
# User wenzelm
# Date 1674245951 -3600
# Node ID 02738f4333eecd4f94bceb2d679d7f2daad7b11d
# Parent  d7dc5b1e4381a3149a02c069c4b7f83ca5602f97
clarified signature;

diff -r d7dc5b1e4381 -r 02738f4333ee src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Fri Jan 20 21:08:18 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Jan 20 21:19:11 2023 +0100
@@ -245,7 +245,7 @@
   private val commands = List("preamble", "string")
   def is_command(s: String): Boolean = commands.contains(s.toLowerCase)
 
-  sealed case class Entry(
+  sealed case class Entry_Type(
     kind: String,
     required: List[String],
     optional_crossref: List[String],
@@ -266,69 +266,67 @@
       "@" + kind + "{,\n" + fields.map(x => "  " + x + " = {},\n").mkString + "}\n"
   }
 
-  val known_entries: List[Entry] =
+  val known_entries: List[Entry_Type] =
     List(
-      Entry("Article",
+      Entry_Type("Article",
         List("author", "title"),
         List("journal", "year"),
         List("volume", "number", "pages", "month", "note")),
-      Entry("InProceedings",
+      Entry_Type("InProceedings",
         List("author", "title"),
         List("booktitle", "year"),
         List("editor", "volume", "number", "series", "pages", "month", "address",
           "organization", "publisher", "note")),
-      Entry("InCollection",
+      Entry_Type("InCollection",
         List("author", "title", "booktitle"),
         List("publisher", "year"),
         List("editor", "volume", "number", "series", "type", "chapter", "pages",
           "edition", "month", "address", "note")),
-      Entry("InBook",
+      Entry_Type("InBook",
         List("author", "editor", "title", "chapter"),
         List("publisher", "year"),
         List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
-      Entry("Proceedings",
+      Entry_Type("Proceedings",
         List("title", "year"),
         List(),
         List("booktitle", "editor", "volume", "number", "series", "address", "month",
           "organization", "publisher", "note")),
-      Entry("Book",
+      Entry_Type("Book",
         List("author", "editor", "title"),
         List("publisher", "year"),
         List("volume", "number", "series", "address", "edition", "month", "note")),
-      Entry("Booklet",
+      Entry_Type("Booklet",
         List("title"),
         List(),
         List("author", "howpublished", "address", "month", "year", "note")),
-      Entry("PhdThesis",
+      Entry_Type("PhdThesis",
         List("author", "title", "school", "year"),
         List(),
         List("type", "address", "month", "note")),
-      Entry("MastersThesis",
+      Entry_Type("MastersThesis",
         List("author", "title", "school", "year"),
         List(),
         List("type", "address", "month", "note")),
-      Entry("TechReport",
+      Entry_Type("TechReport",
         List("author", "title", "institution", "year"),
         List(),
         List("type", "number", "address", "month", "note")),
-      Entry("Manual",
+      Entry_Type("Manual",
         List("title"),
         List(),
         List("author", "organization", "address", "edition", "month", "year", "note")),
-      Entry("Unpublished",
+      Entry_Type("Unpublished",
         List("author", "title", "note"),
         List(),
         List("month", "year")),
-      Entry("Misc",
+      Entry_Type("Misc",
         List(),
         List(),
         List("author", "title", "howpublished", "month", "year", "note")))
 
-  def get_entry(kind: String): Option[Entry] =
+  def known_entry(kind: String): Option[Entry_Type] =
     known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
 
-  def is_entry(kind: String): Boolean = get_entry(kind).isDefined
-
 
 
   /** tokens and chunks **/
@@ -398,7 +396,7 @@
     def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
     def is_malformed: Boolean = tokens.exists(_.is_malformed)
     def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
-    def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
+    def is_entry: Boolean = Bibtex.known_entry(kind).isDefined && name != "" && content.isDefined
   }
 
 
@@ -530,7 +528,7 @@
       identifier ^^ { case a =>
         val kind =
           if (is_command(a)) Token.Kind.COMMAND
-          else if (is_entry(a)) Token.Kind.ENTRY
+          else if (known_entry(a).isDefined) Token.Kind.ENTRY
           else Token.Kind.IDENT
         Token(kind, a)
       }
diff -r d7dc5b1e4381 -r 02738f4333ee src/Tools/jEdit/src/jedit_bibtex.scala
--- a/src/Tools/jEdit/src/jedit_bibtex.scala	Fri Jan 20 21:08:18 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala	Fri Jan 20 21:19:11 2023 +0100
@@ -31,11 +31,11 @@
       case buffer: Buffer
       if File.is_bib(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable =>
         val menu = new JMenu("BibTeX entries")
-        for (entry <- Bibtex.known_entries) {
-          val item = new JMenuItem(entry.kind)
+        for (entry_type <- Bibtex.known_entries) {
+          val item = new JMenuItem(entry_type.kind)
           item.addActionListener(new ActionListener {
             def actionPerformed(evt: ActionEvent): Unit =
-              Isabelle.insert_line_padding(text_area, entry.template)
+              Isabelle.insert_line_padding(text_area, entry_type.template)
           })
           menu.add(item)
         }
@@ -61,9 +61,9 @@
       case Bibtex.Token.Kind.IDENT =>
         if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
         else
-          Bibtex.get_entry(context) match {
-            case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
-            case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
+          Bibtex.known_entry(context) match {
+            case Some(entry_type) if entry_type.is_required(token.source) => JEditToken.KEYWORD3
+            case Some(entry_type) if entry_type.is_optional(token.source) => JEditToken.KEYWORD4
             case _ => JEditToken.DIGIT
           }
       case Bibtex.Token.Kind.SPACE => JEditToken.NULL