# HG changeset patch
# User wenzelm
# Date 1673967352 -3600
# Node ID 9096703ed99edcfc7eed75b43cca2faabbb1b4ce
# Parent  d481dc154310782d2d86ab17c07329c9b723e97d
clarified formal check of bibtex entries (again), see also 86a099f896fc and 467f45e79ff9;

diff -r d481dc154310 -r 9096703ed99e src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Mon Jan 16 22:41:00 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Tue Jan 17 15:55:52 2023 +0100
@@ -57,14 +57,17 @@
           map (fn (name, pos) => (pos, Markup.citation name)) citations);
 
     val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
-    val bibtex_entries =
-      if thy_name = Context.PureN then []
-      else Resources.theory_bibtex_entries thy_name;
+    val bibtex_entries = Resources.theory_bibtex_entries thy_name;
     val _ =
       if null bibtex_entries andalso thy_name <> Context.PureN then ()
       else
         citations |> List.app (fn (name, pos) =>
           if member (op =) bibtex_entries name orelse name = "*" then ()
+          else if thy_name = Context.PureN then
+            (if Context_Position.is_visible ctxt then
+               warning ("Missing theory context --- unchecked Bibtex entry " ^
+                 quote name ^ Position.here pos)
+             else ())
           else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
 
     val kind = if macro_name = "" then get_kind ctxt else macro_name;