NEWS
changeset 70011 9dde788b0128
parent 70009 435fb018e8ee
child 70022 49e178cbf923
     1.1 --- a/NEWS	Fri Mar 29 12:24:34 2019 +0100
     1.2 +++ b/NEWS	Fri Mar 29 13:42:17 2019 +0100
     1.3 @@ -133,20 +133,20 @@
     1.4  to lift specifications to the global theory level.
     1.5  
     1.6  * Command 'export_code' produces output as logical files within the
     1.7 -theory context, as well as session exports that can be materialized
     1.8 -using the command-line tools "isabelle export" or "isabelle build -e"
     1.9 -(with 'export_files' in the session ROOT), or browsed in Isabelle/jEdit
    1.10 -via the "isabelle-export:" file-system. A 'file_prefix' argument allows
    1.11 -to specify an explicit prefix, the default is "export" with a
    1.12 -consecutive number within each theory. The overall prefix "code" is
    1.13 -always prepended.
    1.14 +theory context, as well as formal session exports that can be
    1.15 +materialized via command-line tools "isabelle export" or "isabelle build
    1.16 +-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
    1.17 +provides a virtual file-system "isabelle-export:" that can be explored
    1.18 +in the regular file-browser. A 'file_prefix' argument allows to specify
    1.19 +an explicit name prefix for the target file (SML, OCaml, Scala) or
    1.20 +directory (Haskell); the default is "export" with a consecutive number
    1.21 +within each theory.
    1.22  
    1.23  * Command 'export_code': the 'file' argument is now legacy and will be
    1.24  removed soon: writing to the physical file-system is not well-defined in
    1.25 -a reactive/parallel application like Isabelle. The empty 'file' has been
    1.26 -discontinued already: it has been superseded by the file-browser in
    1.27 -Isabelle/jEdit with "isabelle-export:" as file-system. Minor
    1.28 -INCOMPATIBILITY.
    1.29 +a reactive/parallel application like Isabelle. The empty 'file' argument
    1.30 +has been discontinued already: it is superseded by the file-browser in
    1.31 +Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
    1.32  
    1.33  * Code generation for OCaml: proper strings are used for literals.
    1.34  Minor INCOMPATIBILITY.