--- a/NEWS Fri Feb 15 12:34:29 2019 +0100
+++ b/NEWS Fri Feb 15 17:00:21 2019 +0100
@@ -104,10 +104,10 @@
* Code generation: command 'export_code' without file keyword exports
code as regular theory export, which can be materialized using the
-command-line tool "isabelle export" or 'export_files' in the session
-ROOT, or browsed in Isabelle/jEdit via the "isabelle-export:"
-file-system. To get generated code dumped into output, use "file \<open>\<close>".
-Minor INCOMPATIBILITY.
+command-line tools "isabelle export" or "isabelle build -e" (with
+'export_files' in the session ROOT), or browsed in Isabelle/jEdit via
+the "isabelle-export:" file-system. To get generated code dumped into
+output, use "file \<open>\<close>". Minor INCOMPATIBILITY.
* Code generation for OCaml: proper strings are used for literals.
Minor INCOMPATIBILITY.
@@ -721,7 +721,9 @@
*** ML ***
* Operation Export.export emits theory exports (arbitrary blobs), which
-are stored persistently in the session build database.
+are stored persistently in the session build database. Command-line
+tools "isabelle export" and "isabelle build -e" allow to materialize
+exports in the physical file-system.
* Command 'ML_export' exports ML toplevel bindings to the global
bootstrap environment of the ML process. This allows ML evaluation
@@ -777,8 +779,9 @@
* Command-line tool "isabelle imports -I" also reports actual session
imports. This helps to minimize the session dependency graph.
-* The command-line tool "export" and 'export_files' in session ROOT
-entries retrieve theory exports from the session build database.
+* The command-line tool "export" and "isabelle build -e" (with
+'export_files' in session ROOT entries) retrieve theory exports from the
+session build database.
* The command-line tools "isabelle server" and "isabelle client" provide
access to the Isabelle Server: it supports responsive session management