2010-01-01 nipkow 2010-01-01 added lemmas
2010-01-01 nipkow 2010-01-01 added lemma
2010-01-01 nipkow 2010-01-01 removed FIXME
2010-01-02 wenzelm 2010-01-02 tuned error handling;
2010-01-02 wenzelm 2010-01-02 Standard_System.raw_execute: optional cwd; basic Cygwin.setup with download and unattended installation;
2010-01-02 wenzelm 2010-01-02 Download URLs -- with progress monitor.
2010-01-01 wenzelm 2010-01-01 Future values -- Scala version.
2009-12-31 wenzelm 2009-12-31 added simple dialogs;
2009-12-31 wenzelm 2009-12-31 added is_ready;
2009-12-30 wenzelm 2009-12-30 simplified init message -- removed redundant session property;
2009-12-30 wenzelm 2009-12-30 removed obsolete version check -- sanity delegated to Isabelle_System; tuned;
2009-12-30 wenzelm 2009-12-30 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;
2009-12-30 wenzelm 2009-12-30 tuned signature;
2009-12-30 wenzelm 2009-12-30 less ambitious isatest for SML/NJ;
2009-12-30 krauss 2009-12-30 killed a few warnings
2009-12-30 krauss 2009-12-30 more regular axiom of infinity, with no (indirect) reference to overloaded constants
2009-12-29 wenzelm 2009-12-29 back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
2009-12-29 wenzelm 2009-12-29 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;
2009-12-29 wenzelm 2009-12-29 explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
2009-12-28 wenzelm 2009-12-28 tuned;
2009-12-28 wenzelm 2009-12-28 crude Cygwin.setup;
2009-12-28 wenzelm 2009-12-28 ignore undefined environment;
2009-12-28 wenzelm 2009-12-28 separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
2009-12-28 wenzelm 2009-12-28 tuned;
2009-12-28 wenzelm 2009-12-28 system shutdown hook: strict kill;
2009-12-28 wenzelm 2009-12-28 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);
2009-12-28 wenzelm 2009-12-28 pid without newline -- required for Scala version of system_out;
2009-12-28 wenzelm 2009-12-28 higher-order treatment of temporary files;
2009-12-28 wenzelm 2009-12-28 isabelle_tool: apply platform_path only once; tuned;
2009-12-28 wenzelm 2009-12-28 slightly more paranoid cleanup of process (cf. http://kylecartmell.com/?p=9 "Five Common java.lang.Process Pitfalls");
2009-12-28 wenzelm 2009-12-28 some sanity checks for symbol interpretation;
2009-12-27 wenzelm 2009-12-27 allow UTF-8 in theory and file names;
2009-12-27 wenzelm 2009-12-27 factored-out Library.decode_permissive_utf8;
2009-12-27 wenzelm 2009-12-27 read header by scanning/parsing file;
2009-12-27 wenzelm 2009-12-27 quoted_content: handle escapes;
2009-12-27 wenzelm 2009-12-27 scan: operate on file (via Scan.byte_reader), more robust exception handling;
2009-12-27 wenzelm 2009-12-27 added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
2009-12-27 wenzelm 2009-12-27 removed unused read_file;
2009-12-24 paulson 2009-12-24 tidied proofs
2009-12-24 haftmann 2009-12-24 made sml/nj happy
2009-12-23 boehmes 2009-12-23 updated certificates
2009-12-23 boehmes 2009-12-23 updated example
2009-12-23 boehmes 2009-12-23 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)
2009-12-23 haftmann 2009-12-23 merged
2009-12-23 haftmann 2009-12-23 updated generated document sources
2009-12-23 haftmann 2009-12-23 take care for destructive print mode properly using dedicated pretty builders
2009-12-23 wenzelm 2009-12-23 merged
2009-12-23 haftmann 2009-12-23 made sml/nj happy
2009-12-23 haftmann 2009-12-23 merged
2009-12-23 haftmann 2009-12-23 dropped junk
2009-12-23 haftmann 2009-12-23 reduced code generator cache to the baremost minimum
2009-12-23 haftmann 2009-12-23 updated documentation
2009-12-23 haftmann 2009-12-23 updated generated examples
2009-12-23 haftmann 2009-12-23 reduced code generator cache to the baremost minimum; corrected spelling
2009-12-22 wenzelm 2009-12-22 basic setup for header scanning/parsing;
2009-12-22 wenzelm 2009-12-22 clarified atom parser: return content; added tags parser;
2009-12-22 wenzelm 2009-12-22 tuned;
2009-12-22 wenzelm 2009-12-22 renamed class Outer_Keyword to Outer_Syntax; renamed tokenize to scan (cf. ML version);
2009-12-22 wenzelm 2009-12-22 Isabelle session manager -- most basic setup;
2009-12-22 wenzelm 2009-12-22 actually closer file reader;