NEWS
changeset 62157 adcaaf6c9910
parent 62118 e60f1a925b4d
child 62159 56d35d0fda5b
equal deleted inserted replaced
62156:7355fd313cf8 62157:adcaaf6c9910
     6 
     6 
     7 New in Isabelle2016 (February 2016)
     7 New in Isabelle2016 (February 2016)
     8 -----------------------------------
     8 -----------------------------------
     9 
     9 
    10 *** General ***
    10 *** General ***
       
    11 
       
    12 * Better resource usage on all platforms (Linux, Windows, Mac OS X) for
       
    13 both Isabelle/ML and Isabelle/Scala.  Slightly reduced heap space usage.
    11 
    14 
    12 * Former "xsymbols" syntax with Isabelle symbols is used by default,
    15 * Former "xsymbols" syntax with Isabelle symbols is used by default,
    13 without any special print mode. Important ASCII replacement syntax
    16 without any special print mode. Important ASCII replacement syntax
    14 remains available under print mode "ASCII", but less important syntax
    17 remains available under print mode "ASCII", but less important syntax
    15 has been removed (see below).
    18 has been removed (see below).
    44 * Toplevel theorem statement 'proposition' is another alias for
    47 * Toplevel theorem statement 'proposition' is another alias for
    45 'theorem'.
    48 'theorem'.
    46 
    49 
    47 
    50 
    48 *** Prover IDE -- Isabelle/Scala/jEdit ***
    51 *** Prover IDE -- Isabelle/Scala/jEdit ***
       
    52 
       
    53 * Update to jedit-5.3.0, with improved GUI scaling and support of
       
    54 high-resolution displays (e.g. 4K).
    49 
    55 
    50 * IDE support for the source-level debugger of Poly/ML, to work with
    56 * IDE support for the source-level debugger of Poly/ML, to work with
    51 Isabelle/ML and official Standard ML. Configuration option "ML_debugger"
    57 Isabelle/ML and official Standard ML. Configuration option "ML_debugger"
    52 and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
    58 and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
    53 'SML_file_no_debug' control compilation of sources with debugging
    59 'SML_file_no_debug' control compilation of sources with debugging
   108 works better with GUI scaling for very high-resolution displays (e.g.
   114 works better with GUI scaling for very high-resolution displays (e.g.
   109 4K). Moreover, it is generally more robust than "Nimbus".
   115 4K). Moreover, it is generally more robust than "Nimbus".
   110 
   116 
   111 * The main Isabelle executable is managed as single-instance Desktop
   117 * The main Isabelle executable is managed as single-instance Desktop
   112 application uniformly on all platforms: Linux, Windows, Mac OS X.
   118 application uniformly on all platforms: Linux, Windows, Mac OS X.
   113 
       
   114 * Update to jedit-5.3.0, with improved GUI scaling and support of
       
   115 high-resolution displays (e.g. 4K).
       
   116 
   119 
   117 
   120 
   118 *** Document preparation ***
   121 *** Document preparation ***
   119 
   122 
   120 * Commands 'paragraph' and 'subparagraph' provide additional section
   123 * Commands 'paragraph' and 'subparagraph' provide additional section
   800     ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64
   803     ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64
   801 
   804 
   802 * Bash shell function "jvmpath" has been renamed to "platform_path": it
   805 * Bash shell function "jvmpath" has been renamed to "platform_path": it
   803 is relevant both for Poly/ML and JVM processes.
   806 is relevant both for Poly/ML and JVM processes.
   804 
   807 
   805 * Heap images are 10-15% smaller due to less wasteful persistent theory
       
   806 content (using ML type theory_id instead of theory);
       
   807 
       
   808 * Poly/ML default platform architecture may be changed from 32bit to
   808 * Poly/ML default platform architecture may be changed from 32bit to
   809 64bit via system option ML_system_64. A system restart (and rebuild)
   809 64bit via system option ML_system_64. A system restart (and rebuild)
   810 is required after change.
   810 is required after change.
   811 
   811 
   812 * Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which
   812 * Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which
   813 both allow larger heap space than former x86-cygwin.
   813 both allow larger heap space than former x86-cygwin.
       
   814 
       
   815 * Heap images are 10-15% smaller due to less wasteful persistent theory
       
   816 content (using ML type theory_id instead of theory);
   814 
   817 
   815 
   818 
   816 
   819 
   817 New in Isabelle2015 (May 2015)
   820 New in Isabelle2015 (May 2015)
   818 ------------------------------
   821 ------------------------------