# HG changeset patch
# User wenzelm
# Date 1513433751 -3600
# Node ID 87038a574d098b7d7d2143ae8d79a7033c292384
# Parent  01576aebc398d0e20ca04e82f69336c510d94123
tuned;

diff -r 01576aebc398 -r 87038a574d09 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Dec 16 15:11:19 2017 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 15:15:51 2017 +0100
@@ -199,19 +199,15 @@
 
 local
 
-fun err msg pos = error (msg ^ Position.here pos);
-
-fun gen_check_path check_file ctxt dir (name, pos) =
+fun gen_check check_file ctxt dir (name, pos) =
   let
-    val _ = Context_Position.report ctxt pos Markup.language_path;
+    fun err msg = error (msg ^ Position.here pos);
 
-    val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
-    val _ = Path.expand path handle ERROR msg => err msg pos;
+    val _ = Context_Position.report ctxt pos Markup.language_path;
+    val path = Path.append dir (Path.explode name) handle ERROR msg => err msg;
+    val _ = Path.expand path handle ERROR msg => err msg;
     val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
-    val _ =
-      (case check_file of
-        NONE => path
-      | SOME check => (check path handle ERROR msg => err msg pos));
+    val _ = check_file path handle ERROR msg => err msg;
   in path end;
 
 fun document_antiq check ctxt (name, pos) =
@@ -231,9 +227,9 @@
 
 in
 
-val check_path = gen_check_path NONE;
-val check_file = gen_check_path (SOME File.check_file);
-val check_dir = gen_check_path (SOME File.check_dir);
+val check_path = gen_check I;
+val check_file = gen_check File.check_file;
+val check_dir = gen_check File.check_dir;
 
 val _ = Theory.setup
  (Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))