--- 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) #>