src/Pure/Pure.thy
changeset 67283 0493be7f2d9b
parent 67281 338fb884286b
child 67386 998e01d6f8fd
     1.1 --- a/src/Pure/Pure.thy	Thu Dec 28 12:06:54 2017 +0100
     1.2 +++ b/src/Pure/Pure.thy	Thu Dec 28 12:07:52 2017 +0100
     1.3 @@ -111,17 +111,14 @@
     1.4  
     1.5  ML \<open>
     1.6  local
     1.7 -  fun check_path ctxt (s, pos) =
     1.8 -    let
     1.9 -      val _ = Context_Position.report ctxt pos Markup.language_path;
    1.10 -      val path = Path.explode s;
    1.11 -      val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
    1.12 -    in () end;
    1.13 -
    1.14    val _ =
    1.15      Outer_Syntax.command \<^command_keyword>\<open>external_file\<close> "formal dependency on external file"
    1.16        (Parse.position Parse.path >> (fn path => Toplevel.keep (fn st =>
    1.17 -        check_path (Toplevel.context_of st) path)));
    1.18 +        let
    1.19 +          val ctxt = Toplevel.context_of st;
    1.20 +          val thy = Toplevel.theory_of st;
    1.21 +          val _ = Resources.check_path ctxt (Resources.master_directory thy) path;
    1.22 +        in () end)));
    1.23  
    1.24    val _ =
    1.25      Outer_Syntax.command \<^command_keyword>\<open>bibtex_file\<close> "check bibtex database file in Prover IDE"
    1.26 @@ -129,7 +126,8 @@
    1.27          Toplevel.keep (fn st =>
    1.28            let
    1.29              val ctxt = Toplevel.context_of st;
    1.30 -            val _ = check_path ctxt path;
    1.31 +            val thy = Toplevel.theory_of st;
    1.32 +            val _ = Resources.check_path ctxt (Resources.master_directory thy) path;
    1.33              val _ =
    1.34                (case Token.get_files tok of
    1.35                  [Exn.Res {lines, pos, ...}] => Bibtex.check_database_output pos (cat_lines lines)