NEWS
changeset 69811 18f61ce86425
parent 69791 195aeee8b30a
child 69822 8c587dd44f51
     1.1 --- a/NEWS	Fri Feb 15 12:34:29 2019 +0100
     1.2 +++ b/NEWS	Fri Feb 15 17:00:21 2019 +0100
     1.3 @@ -104,10 +104,10 @@
     1.4  
     1.5  * Code generation: command 'export_code' without file keyword exports
     1.6  code as regular theory export, which can be materialized using the
     1.7 -command-line tool "isabelle export" or 'export_files' in the session
     1.8 -ROOT, or browsed in Isabelle/jEdit via the "isabelle-export:"
     1.9 -file-system. To get generated code dumped into output, use "file \<open>\<close>".
    1.10 -Minor INCOMPATIBILITY.
    1.11 +command-line tools "isabelle export" or "isabelle build -e" (with
    1.12 +'export_files' in the session ROOT), or browsed in Isabelle/jEdit via
    1.13 +the "isabelle-export:" file-system. To get generated code dumped into
    1.14 +output, use "file \<open>\<close>". Minor INCOMPATIBILITY.
    1.15  
    1.16  * Code generation for OCaml: proper strings are used for literals.
    1.17  Minor INCOMPATIBILITY.
    1.18 @@ -721,7 +721,9 @@
    1.19  *** ML ***
    1.20  
    1.21  * Operation Export.export emits theory exports (arbitrary blobs), which
    1.22 -are stored persistently in the session build database.
    1.23 +are stored persistently in the session build database. Command-line
    1.24 +tools "isabelle export" and "isabelle build -e" allow to materialize
    1.25 +exports in the physical file-system.
    1.26  
    1.27  * Command 'ML_export' exports ML toplevel bindings to the global
    1.28  bootstrap environment of the ML process. This allows ML evaluation
    1.29 @@ -777,8 +779,9 @@
    1.30  * Command-line tool "isabelle imports -I" also reports actual session
    1.31  imports. This helps to minimize the session dependency graph.
    1.32  
    1.33 -* The command-line tool "export" and 'export_files' in session ROOT
    1.34 -entries retrieve theory exports from the session build database.
    1.35 +* The command-line tool "export" and "isabelle build -e" (with
    1.36 +'export_files' in session ROOT entries) retrieve theory exports from the
    1.37 +session build database.
    1.38  
    1.39  * The command-line tools "isabelle server" and "isabelle client" provide
    1.40  access to the Isabelle Server: it supports responsive session management