# HG changeset patch
# User wenzelm
# Date 1541875178 -3600
# Node ID 94fa3376ba33a7768fefcb8183420c34390e33b6
# Parent  599b6d0d199b16d573e9d85aba10f05761b8cc88
added ML antiquotation @{master_dir};

diff -r 599b6d0d199b -r 94fa3376ba33 NEWS
--- 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 ***
 
diff -r 599b6d0d199b -r 94fa3376ba33 src/Doc/Tutorial/ToyList/ToyList_Test.thy
--- 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>
diff -r 599b6d0d199b -r 94fa3376ba33 src/Pure/PIDE/resources.ML
--- 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;
 
diff -r 599b6d0d199b -r 94fa3376ba33 src/Tools/Haskell/haskell.ML
--- 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;