--- 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
--- 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;
--- 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 _ =