# HG changeset patch
# User wenzelm
# Date 1513423630 -3600
# Node ID fca5f298809176cdbe89a1e3ebc56a37faa15b64
# Parent  16519cd83ed4c9ee4c18c92b587e8ad04ca57cd1
clarified signature;

diff -r 16519cd83ed4 -r fca5f2988091 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Dec 16 12:16:40 2017 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 12:27:10 2017 +0100
@@ -28,6 +28,9 @@
   val provide: Path.T * SHA1.digest -> theory -> theory
   val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   val loaded_files_current: theory -> bool
+  val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
+  val check_file: Proof.context -> Path.T -> string * Position.T -> Path.T
+  val check_dir: Proof.context -> Path.T -> string * Position.T -> Path.T
 end;
 
 structure Resources: RESOURCES =
@@ -198,7 +201,7 @@
 
 fun err msg pos = error (msg ^ Position.here pos);
 
-fun check_path check_file ctxt dir (name, pos) =
+fun gen_check_path check_file ctxt dir (name, pos) =
   let
     val _ = Context_Position.report ctxt pos Markup.language_path;
 
@@ -211,10 +214,10 @@
       | SOME check => (check path handle ERROR msg => err msg pos));
   in path end;
 
-fun document_antiq check_file ctxt (name, pos) =
+fun document_antiq check ctxt (name, pos) =
   let
     val dir = master_directory (Proof_Context.theory_of ctxt);
-    val _ = check_path check_file ctxt dir (name, pos);
+    val _ = check ctxt dir (name, pos);
   in
     space_explode "/" name
     |> map Latex.output_ascii
@@ -222,28 +225,29 @@
     |> enclose "\\isatt{" "}"
   end;
 
-fun ML_antiq check_file ctxt (name, pos) =
-  let val path = check_path check_file ctxt Path.current (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_path NONE;
+val check_file = gen_check_path (SOME File.check_file);
+val check_dir = gen_check_path (SOME File.check_dir);
+
 val _ = Theory.setup
  (Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
-    (document_antiq NONE o #context) #>
+    (document_antiq check_path o #context) #>
   Thy_Output.antiquotation \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
-    (document_antiq (SOME File.check_file) o #context) #>
+    (document_antiq check_file o #context) #>
   Thy_Output.antiquotation \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
-    (document_antiq (SOME File.check_dir) o #context) #>
+    (document_antiq check_dir o #context) #>
   ML_Antiquotation.value \<^binding>\<open>path\<close>
-    (Args.context -- Scan.lift (Parse.position Parse.path)
-      >> uncurry (ML_antiq NONE)) #>
+    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>
   ML_Antiquotation.value \<^binding>\<open>file\<close>
-    (Args.context -- Scan.lift (Parse.position Parse.path)
-      >> uncurry (ML_antiq (SOME File.check_file))) #>
+    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_file)) #>
   ML_Antiquotation.value \<^binding>\<open>dir\<close>
-    (Args.context -- Scan.lift (Parse.position Parse.path)
-      >> uncurry (ML_antiq (SOME File.check_dir))));
+    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_dir)));
 
 end;