more accurate Word.capitalize: do not touch name;
authorwenzelm
Tue, 31 Jan 2023 16:13:27 +0100
changeset 77148 9b3a8565464d
parent 77147 38077c938d01
child 77149 3991a35cd740
more accurate Word.capitalize: do not touch name;
src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Tue Jan 31 14:59:19 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Tue Jan 31 16:13:27 2023 +0100
@@ -132,7 +132,7 @@
               case (Error(msg, Value.Int(l)), _) =>
                 Some((true, (msg, get_line_pos(l))))
               case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
-                Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name))))
+                Some((false, (Word.capitalize(msg) + " in entry " + quote(name), chunk_pos(name))))
               case (Warning(msg), Warning_Line(Value.Int(l))) =>
                 Some((false, (Word.capitalize(msg), get_line_pos(l))))
               case (Warning(msg), _) =>