distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names; asynchronous Isabelle_Process.init -- raw ML toplevel stays active; simplified Isabelle_Process using actors; misc tuning;

added Library.thread_actor -- thread as actor;

clarified JEDIT_JAVA_OPTIONS vs. JEDIT_SYSTEM_OPTIONS -- discontinued JEDIT_APPLE_PROPERTIES; static default Dactors.corePoolSize=4 for more reproducible concurrency, independently of number of cores;

auto_flush: higher frequency;

uniform raw_dump for input/output fifos on Cygwin;

more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;

Isabelle_Process: separate input fifo for commands (still using the old tty protocol); some partial workarounds for Cygwin;

tuned comments;

merged

added Lars Noschinski to isatest report

merged

discontinued separation of `define` and `declare_const`

unravelled target initialization code

added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)

added scanning of if-then-else expressions

merged

added support for partial quotient types; previously Nitpick was unsound for these

adapt occurrences of renamed Nitpick functions

document the non-legacy interfaces

local versions of Nitpick.register_xxx functions

parse_spans: somewhat faster low-level implementation;

proper context for Syntax.parse_token;

prefer Context_Position.report where a proper context is available -- notably for "inner" entities;

explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);