# HG changeset patch
# User wenzelm
# Date 1610973953 -3600
# Node ID 5f49f1149c1cf693f71232b08282b98ff50e2e2e
# Parent  cc71193891c26177334b176ec928049888583473
clarified reports before errors: support completion of bibtex entries in Isabelle/Scala (amending d01ea9e3bd2d);

diff -r cc71193891c2 -r 5f49f1149c1c src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Mon Jan 18 13:43:32 2021 +0100
+++ b/src/Pure/Thy/bibtex.ML	Mon Jan 18 13:45:53 2021 +0100
@@ -46,6 +46,10 @@
         (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position))
       (fn ctxt => fn (opt, citations) =>
         let
+          val _ =
+            Context_Position.reports ctxt
+              (map (fn (name, pos) => (pos, Markup.citation name)) citations);
+
           val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
           val bibtex_entries = Resources.theory_bibtex_entries thy_name;
           val _ =
@@ -54,9 +58,7 @@
               citations |> List.app (fn (name, pos) =>
                 if member (op =) bibtex_entries name then ()
                 else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
-          val _ =
-            Context_Position.reports ctxt
-              (map (fn (name, pos) => (pos, Markup.citation name)) citations);
+
           val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
           val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
         in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end));