more standard Resources.provide_parse_files: avoid duplicate markup reports;
authorwenzelm
Thu Nov 08 13:42:36 2018 +0100 (6 months ago)
changeset 69262f94726501b37
parent 69261 a41f49148525
child 69263 c546e37f6cb9
more standard Resources.provide_parse_files: avoid duplicate markup reports;
src/Pure/Pure.thy
     1.1 --- a/src/Pure/Pure.thy	Thu Nov 08 12:32:06 2018 +0100
     1.2 +++ b/src/Pure/Pure.thy	Thu Nov 08 13:42:36 2018 +0100
     1.3 @@ -107,26 +107,16 @@
     1.4  local
     1.5    val _ =
     1.6      Outer_Syntax.command \<^command_keyword>\<open>external_file\<close> "formal dependency on external file"
     1.7 -      (Parse.position Parse.path >> (fn path => Toplevel.keep (fn st =>
     1.8 -        let
     1.9 -          val ctxt = Toplevel.context_of st;
    1.10 -          val thy = Toplevel.theory_of st;
    1.11 -          val _ = Resources.check_path ctxt (Resources.master_directory thy) path;
    1.12 -        in () end)));
    1.13 +      (Resources.provide_parse_files "external_file" >> (fn files => Toplevel.theory (#2 o files)));
    1.14  
    1.15    val _ =
    1.16      Outer_Syntax.command \<^command_keyword>\<open>bibtex_file\<close> "check bibtex database file in Prover IDE"
    1.17 -      (Scan.ahead Parse.not_eof -- Parse.position Parse.path >> (fn (tok, path) =>
    1.18 -        Toplevel.keep (fn st =>
    1.19 +      (Resources.provide_parse_files "bibtex_file" >> (fn files =>
    1.20 +        Toplevel.theory (fn thy =>
    1.21            let
    1.22 -            val ctxt = Toplevel.context_of st;
    1.23 -            val thy = Toplevel.theory_of st;
    1.24 -            val _ = Resources.check_path ctxt (Resources.master_directory thy) path;
    1.25 -            val _ =
    1.26 -              (case Token.get_files tok of
    1.27 -                [Exn.Res {lines, pos, ...}] => Bibtex.check_database_output pos (cat_lines lines)
    1.28 -              | _ => ());
    1.29 -          in () end)));
    1.30 +            val ([{lines, pos, ...}], thy') = files thy;
    1.31 +            val _ = Bibtex.check_database_output pos (cat_lines lines);
    1.32 +          in thy' end)));
    1.33  in end\<close>
    1.34  
    1.35