NEWS
changeset 73008 dacf2598bb27
parent 73007 11140980a6b5
child 73009 56eae6d161db
equal deleted inserted replaced
73007:11140980a6b5 73008:dacf2598bb27
    37 * The visual feedback on caret entity focus is normally restricted to
    37 * The visual feedback on caret entity focus is normally restricted to
    38 definitions within the visible text area. The keyboard modifier "CS"
    38 definitions within the visible text area. The keyboard modifier "CS"
    39 overrides this: then all defining and referencing positions are shown.
    39 overrides this: then all defining and referencing positions are shown.
    40 See also option "jedit_focus_modifier".
    40 See also option "jedit_focus_modifier".
    41 
    41 
    42 * Auto nitpick is enabled by default: it is now reasonably fast due to
       
    43 Kodkod invocation within Isabelle/Scala.
       
    44 
       
    45 * The jEdit status line includes widgets both for JVM and ML heap usage.
    42 * The jEdit status line includes widgets both for JVM and ML heap usage.
    46 Ongoing ML ongoing garbage collection is shown as "ML cleanup".
    43 Ongoing ML ongoing garbage collection is shown as "ML cleanup".
    47 
    44 
    48 * The Monitor dockable provides buttons to request a full garbage
    45 * The Monitor dockable provides buttons to request a full garbage
    49 collection and sharing of live data on the ML heap. It also includes
    46 collection and sharing of live data on the ML heap. It also includes
   132 defect and two incompleteness defects. Very slight INCOMPATIBILITY.
   129 defect and two incompleteness defects. Very slight INCOMPATIBILITY.
   133 
   130 
   134 * Nitpick/Kodkod may be invoked directly within the running
   131 * Nitpick/Kodkod may be invoked directly within the running
   135 Isabelle/Scala session (instead of an external Java process): this
   132 Isabelle/Scala session (instead of an external Java process): this
   136 improves reactivity and saves resources. This experimental feature is
   133 improves reactivity and saves resources. This experimental feature is
   137 guarded by system option "kodkod_scala" (default: true).
   134 guarded by system option "kodkod_scala" (default: true in PIDE
       
   135 interaction, false in batch builds).
   138 
   136 
   139 * Simproc "defined_all" and rewrite rule "subst_all" perform more
   137 * Simproc "defined_all" and rewrite rule "subst_all" perform more
   140 aggressive substitution with variables from assumptions.
   138 aggressive substitution with variables from assumptions.
   141 INCOMPATIBILITY, consider repairing proofs locally like this:
   139 INCOMPATIBILITY, consider repairing proofs locally like this:
   142 
   140