NEWS

--- a/NEWS	Fri Nov 30 23:30:42 2018 +0100
+++ b/NEWS	Fri Nov 30 23:43:10 2018 +0100
@@ -119,24 +119,27 @@
 potentially with variations on ML syntax (existing ML_Env.SML_operations
 observes the official standard).
 
-* GHC.read_source reads Haskell source text with antiquotations (only
-the control-cartouche form). The default "cartouche" antiquotation
-evaluates an ML expression of type string and inlines the result as
-Haskell string literal. This allows to refer to Isabelle items robustly,
-e.g. via Isabelle/ML antiquotations or library operations. For example:
-
-ML_command \<open>
-  GHC.read_source \<^context> \<open>
+* ML antiquotation @{master_dir} refers to the master directory of the
+underlying theory, i.e. the directory of the theory file.
+
+* Command 'generate_file' allows to produce sources for other languages,
+with antiquotations in the Isabelle context (only the control-cartouche
+form). The default "cartouche" antiquotation evaluates an ML expression
+of type string and inlines the result as a string literal of the target
+language. For example, this works for Haskell as follows:
+
+  generate_file "Pure.hs" = \<open>
+  module Isabelle.Pure where
     allConst, impConst, eqConst :: String
     allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
     impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
     eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
   \<close>
-  |> writeln
-\<close>
-
-* ML antiquotation @{master_dir} refers to the master directory of the
-underlying theory, i.e. the directory of the theory file.
+
+The ML function Generate_File.generate writes all generated files from a
+given theory to the file-system, e.g. a temporary directory where some
+external compiler is applied.
+
 
 
 *** System ***