# HG changeset patch
# User wenzelm
# Date 1554327313 -7200
# Node ID c1226e4c273e285d24f86a900d5fdf9b523482c8
# Parent  198bbe73b1006c4380cd9de3c72a489abe8910ba
tuned signature;

diff -r 198bbe73b100 -r c1226e4c273e src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Apr 03 23:29:19 2019 +0200
+++ b/src/Pure/PIDE/resources.ML	Wed Apr 03 23:35:13 2019 +0200
@@ -34,9 +34,9 @@
   val provide_file: Token.file -> 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
+  val check_path: Proof.context -> Path.T option -> string * Position.T -> Path.T
+  val check_file: Proof.context -> Path.T option -> string * Position.T -> Path.T
+  val check_dir: Proof.context -> Path.T option -> string * Position.T -> Path.T
 end;
 
 structure Resources: RESOURCES =
@@ -242,11 +242,15 @@
 
 (* formal check *)
 
-fun formal_check check_file ctxt dir (name, pos) =
+fun formal_check check_file ctxt opt_dir (name, pos) =
   let
     fun err msg = error (msg ^ Position.here pos);
 
     val _ = Context_Position.report ctxt pos Markup.language_path;
+    val dir =
+      (case opt_dir of
+        SOME dir => dir
+      | NONE => master_directory (Proof_Context.theory_of ctxt));
     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));
@@ -262,11 +266,10 @@
 
 local
 
-fun document_antiq check =
+fun document_antiq (check: Proof.context -> Path.T option -> string * Position.T -> Path.T) =
   Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
     let
-      val dir = master_directory (Proof_Context.theory_of ctxt);
-      val _: Path.T = check ctxt dir (name, pos);
+      val _ = check ctxt NONE (name, pos);
       val latex =
         space_explode "/" name
         |> map Latex.output_ascii
@@ -275,7 +278,7 @@
 
 fun ML_antiq check =
   Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
-    check ctxt Path.current (name, pos) |> ML_Syntax.print_path);
+    check ctxt (SOME Path.current) (name, pos) |> ML_Syntax.print_path);
 
 in
 
diff -r 198bbe73b100 -r c1226e4c273e src/Pure/Thy/sessions.ML
--- a/src/Pure/Thy/sessions.ML	Wed Apr 03 23:29:19 2019 +0200
+++ b/src/Pure/Thy/sessions.ML	Wed Apr 03 23:35:13 2019 +0200
@@ -64,7 +64,7 @@
       let
         val ctxt = Toplevel.context_of state;
         val thy = Toplevel.theory_of state;
-        val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir;
+        val session_dir = Resources.check_dir ctxt NONE dir;
 
         val _ =
           (the_list parent @ sessions) |> List.app (fn arg =>
@@ -88,19 +88,19 @@
                 Resources.import_name session session_dir s
                   handle ERROR msg => error (msg ^ Position.here pos);
               val theory_path = the_default node_name (Resources.known_theory theory_name);
-              val _ = Resources.check_file ctxt Path.current (Path.implode theory_path, pos);
+              val _ = Resources.check_file ctxt (SOME Path.current) (Path.implode theory_path, pos);
             in () end);
 
         val _ =
           document_files |> List.app (fn (doc_dir, doc_files) =>
             let
-              val dir = Resources.check_dir ctxt session_dir doc_dir;
-              val _ = List.app (ignore o Resources.check_file ctxt dir) doc_files;
+              val dir = Resources.check_dir ctxt (SOME session_dir) doc_dir;
+              val _ = List.app (ignore o Resources.check_file ctxt (SOME dir)) doc_files;
             in () end);
 
         val _ =
           export_files |> List.app (fn ((export_dir, _), _) =>
-            ignore (Resources.check_path ctxt session_dir export_dir));
+            ignore (Resources.check_path ctxt (SOME session_dir) export_dir));
       in () end));
 
 end;
diff -r 198bbe73b100 -r c1226e4c273e src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Wed Apr 03 23:29:19 2019 +0200
+++ b/src/Pure/Tools/generated_files.ML	Wed Apr 03 23:35:13 2019 +0200
@@ -271,7 +271,7 @@
 fun path_antiquotation binding check =
   antiquotation binding
     (Args.context -- Scan.lift (Parse.position Parse.path) >>
-      (fn (ctxt, (name, pos)) => (check ctxt Path.current (name, pos) |> Path.implode)))
+      (fn (ctxt, (name, pos)) => (check ctxt (SOME Path.current) (name, pos) |> Path.implode)))
     (fn {file_type, argument, ...} => #make_string file_type argument);
 
 val _ =