changeset 70009 435fb018e8ee
parent 69962 82e945d472d5
child 70011 9dde788b0128
     1.1 --- a/NEWS	Thu Mar 28 21:22:44 2019 +0100
     1.2 +++ b/NEWS	Thu Mar 28 21:24:55 2019 +0100
     1.3 @@ -132,12 +132,21 @@
     1.4  Minor INCOMPATIBILITY, prefer combinators Named_Target.theory_map[_result]
     1.5  to lift specifications to the global theory level.
     1.7 -* Code generation: command 'export_code' without file keyword exports
     1.8 -code as regular theory export, which can be materialized using the
     1.9 -command-line tools "isabelle export" or "isabelle build -e" (with
    1.10 -'export_files' in the session ROOT), or browsed in Isabelle/jEdit via
    1.11 -the "isabelle-export:" file-system. To get generated code dumped into
    1.12 -output, use "file \<open>\<close>". Minor INCOMPATIBILITY.
    1.13 +* Command 'export_code' produces output as logical files within the
    1.14 +theory context, as well as session exports that can be materialized
    1.15 +using the command-line tools "isabelle export" or "isabelle build -e"
    1.16 +(with 'export_files' in the session ROOT), or browsed in Isabelle/jEdit
    1.17 +via the "isabelle-export:" file-system. A 'file_prefix' argument allows
    1.18 +to specify an explicit prefix, the default is "export" with a
    1.19 +consecutive number within each theory. The overall prefix "code" is
    1.20 +always prepended.
    1.21 +
    1.22 +* Command 'export_code': the 'file' argument is now legacy and will be
    1.23 +removed soon: writing to the physical file-system is not well-defined in
    1.24 +a reactive/parallel application like Isabelle. The empty 'file' has been
    1.25 +discontinued already: it has been superseded by the file-browser in
    1.26 +Isabelle/jEdit with "isabelle-export:" as file-system. Minor
    1.29  * Code generation for OCaml: proper strings are used for literals.
    1.30  Minor INCOMPATIBILITY.