clarified error;
authorwenzelm
Fri, 12 Aug 2016 13:34:59 +0200
changeset 63673 2314e99c18a7
parent 63672 5a7c919a4ada
child 63674 f97f2ad2486a
clarified error;
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;