# HG changeset patch
# User wenzelm
# Date 1471001699 -7200
# Node ID 2314e99c18a78a8ba34f9dea3b532027767a90c1
# Parent  5a7c919a4ada696ad4b1201e2bbfccb57b997696
clarified error;

diff -r 5a7c919a4ada -r 2314e99c18a7 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Aug 12 13:16:04 2016 +0200
+++ b/src/Pure/PIDE/resources.ML	Fri Aug 12 13:34:59 2016 +0200
@@ -220,8 +220,10 @@
   Thy_Output.antiquotation @{binding dir} (Scan.lift (Parse.position Parse.path))
     (path_antiq (SOME File.check_dir) o #context) #>
   ML_Antiquotation.value @{binding file}
-    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
-      let val path = check_path ctxt Path.current arg |> File.check_file
+    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
+      let
+        val path = check_path ctxt Path.current (name, pos);
+        val _ = File.check_file path handle ERROR msg => err msg pos;
       in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
 
 end;