# HG changeset patch
# User wenzelm
# Date 1674056941 -3600
# Node ID fead2b33acdca651056429871f0c204994a21e36
# Parent  2342b4cc118f0c5950daf395d759822885d7f02e
tuned signature: fewer warnings in IntelliJ IDEA;

diff -r 2342b4cc118f -r fead2b33acdc src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Wed Jan 18 16:27:44 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Wed Jan 18 16:49:01 2023 +0100
@@ -385,7 +385,7 @@
   }
 
   case class Chunk(kind: String, tokens: List[Token]) {
-    val source = tokens.map(_.source).mkString
+    val source: String = tokens.map(_.source).mkString
 
     private val content: Option[List[Token]] =
       tokens match {
@@ -433,7 +433,7 @@
   case class Item(kind: String, end: String, delim: Delimited) extends Line_Context
 
   case class Delimited(quoted: Boolean, depth: Int)
-  val Closed = Delimited(false, 0)
+  val Closed: Delimited = Delimited(false, 0)
 
   private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source)
   private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
@@ -469,7 +469,7 @@
         require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0,
           "bad delimiter depth")
 
-        def apply(in: Input) = {
+        def apply(in: Input): ParseResult[(String, Delimited)] = {
           val start = in.offset
           val end = in.source.length
 
@@ -526,7 +526,7 @@
 
     private val ident = identifier ^^ token(Token.Kind.IDENT)
 
-    val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space))
+    val other_token: Parser[Token] = "[=#,]".r ^^ keyword | (nat | (ident | space))
 
 
     /* body */