# HG changeset patch
# User wenzelm
# Date 1513441380 -3600
# Node ID 53867014e299f2fe0a6aad80a5fe44dce9387239
# Parent  99815211970cd6d147e9e2968ef460a960ac5b13
tuned;

diff -r 99815211970c -r 53867014e299 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Dec 16 16:57:06 2017 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 17:23:00 2017 +0100
@@ -197,11 +197,9 @@
       | SOME ((_, id'), _) => id = id'));
 
 
-(* antiquotations *)
+(* formal check *)
 
-local
-
-fun gen_check check_file ctxt dir (name, pos) =
+fun formal_check check_file ctxt dir (name, pos) =
   let
     fun err msg = error (msg ^ Position.here pos);
 
@@ -212,6 +210,15 @@
     val _ = check_file path handle ERROR msg => err msg;
   in path end;
 
+val check_path = formal_check I;
+val check_file = formal_check File.check_file;
+val check_dir = formal_check File.check_dir;
+
+
+(* antiquotations *)
+
+local
+
 fun document_antiq check ctxt (name, pos) =
   let
     val dir = master_directory (Proof_Context.theory_of ctxt);
@@ -229,10 +236,6 @@
 
 in
 
-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))
     (document_antiq check_path o #context) #>