added ML antiquotation @{master_dir};
authorwenzelm
Sat Nov 10 19:39:38 2018 +0100 (10 months ago ago)
changeset 6928794fa3376ba33
parent 69286 599b6d0d199b
child 69288 a885a4ceaeb6
child 69289 3273692de24a
child 69290 39044da8bb5a
added ML antiquotation @{master_dir};
NEWS
src/Doc/Tutorial/ToyList/ToyList_Test.thy
src/Pure/PIDE/resources.ML
src/Tools/Haskell/haskell.ML
     1.1 --- a/NEWS	Sat Nov 10 19:01:20 2018 +0100
     1.2 +++ b/NEWS	Sat Nov 10 19:39:38 2018 +0100
     1.3 @@ -114,6 +114,9 @@
     1.4    |> writeln
     1.5  \<close>
     1.6  
     1.7 +* ML antiquotation @{master_dir} refers to the master directory of the
     1.8 +underlying theory, i.e. the directory of the theory file.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Sat Nov 10 19:01:20 2018 +0100
     2.2 +++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Sat Nov 10 19:39:38 2018 +0100
     2.3 @@ -4,8 +4,7 @@
     2.4  
     2.5  ML \<open>
     2.6    let val text =
     2.7 -    map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
     2.8 -      ["ToyList1.txt", "ToyList2.txt"]
     2.9 +    map (File.read o Path.append \<^master_dir>) [\<^path>\<open>ToyList1.txt\<close>, \<^path>\<open>ToyList2.txt\<close>]
    2.10      |> implode
    2.11    in Thy_Info.script_thy Position.start text @{theory} end
    2.12  \<close>
     3.1 --- a/src/Pure/PIDE/resources.ML	Sat Nov 10 19:01:20 2018 +0100
     3.2 +++ b/src/Pure/PIDE/resources.ML	Sat Nov 10 19:39:38 2018 +0100
     3.3 @@ -286,7 +286,9 @@
     3.4    Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
     3.5    ML_Antiquotation.value \<^binding>\<open>path\<close> (ML_antiq check_path) #>
     3.6    ML_Antiquotation.value \<^binding>\<open>file\<close> (ML_antiq check_file) #>
     3.7 -  ML_Antiquotation.value \<^binding>\<open>dir\<close> (ML_antiq check_dir));
     3.8 +  ML_Antiquotation.value \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
     3.9 +  ML_Antiquotation.value \<^binding>\<open>master_dir\<close>
    3.10 +    (Args.theory >> (ML_Syntax.print_path o master_directory)));
    3.11  
    3.12  end;
    3.13  
     4.1 --- a/src/Tools/Haskell/haskell.ML	Sat Nov 10 19:01:20 2018 +0100
     4.2 +++ b/src/Tools/Haskell/haskell.ML	Sat Nov 10 19:39:38 2018 +0100
     4.3 @@ -61,9 +61,7 @@
     4.4    \<^path>\<open>Term_XML/Encode.hs\<close>,
     4.5    \<^path>\<open>Term_XML/Decode.hs\<close>];
     4.6  
     4.7 -val master_dir = Resources.master_directory \<^theory>;
     4.8 -
     4.9  fun install_sources dir =
    4.10 -  sources |> List.app (fn path => Isabelle_System.copy_file_base (master_dir, path) dir);
    4.11 +  sources |> List.app (fn path => Isabelle_System.copy_file_base (\<^master_dir>, path) dir);
    4.12  
    4.13  end;