src/Pure/PIDE/resources.ML

       (case try (load_file thy) src_path of
         NONE => false
       | SOME ((_, id'), _) => id = id'));
 
 
-(* antiquotations *)
-
-local
-
-fun gen_check check_file ctxt dir (name, pos) =
+(* formal check *)
+
+fun formal_check check_file ctxt dir (name, pos) =
   let
     fun err msg = error (msg ^ Position.here 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 _ = 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);
     val _ = check ctxt dir (name, pos);

 fun ML_antiq check ctxt (name, pos) =
   let val path = check ctxt Path.current (name, pos);
   in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
 
 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) #>
   Thy_Output.antiquotation \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))