tuned error handling;

Standard_System.raw_execute: optional cwd; basic Cygwin.setup with download and unattended installation;

Download URLs -- with progress monitor.

Future values -- Scala version.

added simple dialogs;

added is_ready;

simplified init message -- removed redundant session property;

removed obsolete version check -- sanity delegated to Isabelle_System; tuned;

eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id; eliminated ML interface of Isar_Document: the protocol only works with certain transaction positions, i.e. via Isar commands;

tuned signature;

less ambitious isatest for SML/NJ;

killed a few warnings

more regular axiom of infinity, with no (indirect) reference to overloaded constants

back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;

removed slightly odd Isar_Document.init; simplified begin_document: associate empty command/state with no_id, which is implicit start; replaced make_id by create_id (cf. Scala version); eliminated CRITICAL/Unsynchronized.ref in favour of Synchronized.var; tuned;

explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;

tuned;

crude Cygwin.setup;

ignore undefined environment;

separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);

tuned;

system shutdown hook: strict kill;

moved Library.decode_permissive_utf8 to Isabelle_System; moved Library.with_tmp_file to Isabelle_System; added Isabelle_System.read_file/write_file; added Isabelle_System.system_out, with propagation of thread interrupts and process shutdown (global CTRL-C);

pid without newline -- required for Scala version of system_out;

higher-order treatment of temporary files;

isabelle_tool: apply platform_path only once; tuned;

slightly more paranoid cleanup of process (cf. http://kylecartmell.com/?p=9 "Five Common java.lang.Process Pitfalls");

some sanity checks for symbol interpretation;

allow UTF-8 in theory and file names;

factored-out Library.decode_permissive_utf8;

read header by scanning/parsing file;

quoted_content: handle escapes;

scan: operate on file (via Scan.byte_reader), more robust exception handling;

added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);

removed unused read_file;

tidied proofs

made sml/nj happy

updated certificates

updated example

merged verification condition structure and term representation in one datatype, extended the set of operations on verification conditions (retrieve more information, advanced splitting of paths), simplified discharging of verification conditions (due to improved datatype), added variantions of commands (extract different parts of verification conditions, scan until first "hard" assertion)

merged

updated generated document sources

take care for destructive print mode properly using dedicated pretty builders

merged

made sml/nj happy

merged

dropped junk

reduced code generator cache to the baremost minimum

updated documentation

updated generated examples

reduced code generator cache to the baremost minimum; corrected spelling

basic setup for header scanning/parsing;

clarified atom parser: return content; added tags parser;

tuned;

renamed class Outer_Keyword to Outer_Syntax; renamed tokenize to scan (cf. ML version);

Isabelle session manager -- most basic setup;

actually closer file reader;

tuned;

added plain read_file;

consider proper input only; added wrappers;