# HG changeset patch
# User wenzelm
# Date 1541680956 -3600
# Node ID f94726501b37c851aa3a0ef5b974f19efd1d1189
# Parent  a41f491485257e296892fd438e13599dd5164365
more standard Resources.provide_parse_files: avoid duplicate markup reports;

diff -r a41f49148525 -r f94726501b37 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Nov 08 12:32:06 2018 +0100
+++ b/src/Pure/Pure.thy	Thu Nov 08 13:42:36 2018 +0100
@@ -107,26 +107,16 @@
 local
   val _ =
     Outer_Syntax.command \<^command_keyword>\<open>external_file\<close> "formal dependency on external file"
-      (Parse.position Parse.path >> (fn path => Toplevel.keep (fn st =>
-        let
-          val ctxt = Toplevel.context_of st;
-          val thy = Toplevel.theory_of st;
-          val _ = Resources.check_path ctxt (Resources.master_directory thy) path;
-        in () end)));
+      (Resources.provide_parse_files "external_file" >> (fn files => Toplevel.theory (#2 o files)));
 
   val _ =
     Outer_Syntax.command \<^command_keyword>\<open>bibtex_file\<close> "check bibtex database file in Prover IDE"
-      (Scan.ahead Parse.not_eof -- Parse.position Parse.path >> (fn (tok, path) =>
-        Toplevel.keep (fn st =>
+      (Resources.provide_parse_files "bibtex_file" >> (fn files =>
+        Toplevel.theory (fn thy =>
           let
-            val ctxt = Toplevel.context_of st;
-            val thy = Toplevel.theory_of st;
-            val _ = Resources.check_path ctxt (Resources.master_directory thy) path;
-            val _ =
-              (case Token.get_files tok of
-                [Exn.Res {lines, pos, ...}] => Bibtex.check_database_output pos (cat_lines lines)
-              | _ => ());
-          in () end)));
+            val ([{lines, pos, ...}], thy') = files thy;
+            val _ = Bibtex.check_database_output pos (cat_lines lines);
+          in thy' end)));
 in end\<close>