--- a/NEWS Sat Nov 10 19:01:20 2018 +0100
+++ b/NEWS Sat Nov 10 19:39:38 2018 +0100
@@ -114,6 +114,9 @@
|> writeln
\<close>
+* ML antiquotation @{master_dir} refers to the master directory of the
+underlying theory, i.e. the directory of the theory file.
+
*** System ***
--- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy Sat Nov 10 19:01:20 2018 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy Sat Nov 10 19:39:38 2018 +0100
@@ -4,8 +4,7 @@
ML \<open>
let val text =
- map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
- ["ToyList1.txt", "ToyList2.txt"]
+ map (File.read o Path.append \<^master_dir>) [\<^path>\<open>ToyList1.txt\<close>, \<^path>\<open>ToyList2.txt\<close>]
|> implode
in Thy_Info.script_thy Position.start text @{theory} end
\<close>
--- a/src/Pure/PIDE/resources.ML Sat Nov 10 19:01:20 2018 +0100
+++ b/src/Pure/PIDE/resources.ML Sat Nov 10 19:39:38 2018 +0100
@@ -286,7 +286,9 @@
Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
ML_Antiquotation.value \<^binding>\<open>path\<close> (ML_antiq check_path) #>
ML_Antiquotation.value \<^binding>\<open>file\<close> (ML_antiq check_file) #>
- ML_Antiquotation.value \<^binding>\<open>dir\<close> (ML_antiq check_dir));
+ ML_Antiquotation.value \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
+ ML_Antiquotation.value \<^binding>\<open>master_dir\<close>
+ (Args.theory >> (ML_Syntax.print_path o master_directory)));
end;
--- a/src/Tools/Haskell/haskell.ML Sat Nov 10 19:01:20 2018 +0100
+++ b/src/Tools/Haskell/haskell.ML Sat Nov 10 19:39:38 2018 +0100
@@ -61,9 +61,7 @@
\<^path>\<open>Term_XML/Encode.hs\<close>,
\<^path>\<open>Term_XML/Decode.hs\<close>];
-val master_dir = Resources.master_directory \<^theory>;
-
fun install_sources dir =
- sources |> List.app (fn path => Isabelle_System.copy_file_base (master_dir, path) dir);
+ sources |> List.app (fn path => Isabelle_System.copy_file_base (\<^master_dir>, path) dir);
end;