build session before start of jedit;

imitate "isabelle java" and "isabelle jedit" wrt. classpath and options;

more Proof General legacy;

use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);

warm start of Isabelle/jEdit from Isabelle/Scala; avoid mass confusion of plugins due to change of -classpath (cf. 5bef05f5ed58);

prefer explicit thread;

tuned proofs;

tuned proofs;

prefer Isabelle/Scala over bash; actual platform_path (in contrast to eb8806a2e348);

prefer Isabelle/Scala over bash;

prefer warm start via JEdit_Main;

slight cleanup of lemma locations; tuned proof

tuned

tuned;

tuned;

removed junk;

more standard header;

updated keywords;

merged

added examples for Simps_Case_Conv

allowed less exhaustive patterns

use case_of_simps

use case_of_simps

added simps_of_case and case_of_simps to convert between simps and case rules

merged

close window and start process asynchronously;

more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;

recovered cygwin.root from 1c87e79bb838; removed junk;

provide file indicator;

updated windows_app-20130905;

main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator; standardized jdk location;

standardize jdk name; check tar errors;

updated to jdk-7u25; less redundant directory structure;

support only one scala version; tuned;

updated to jedit_build-20130905 which is based on jedit-5.1.0; added jsr305-2.0.0.jar from http://code.google.com/p/findbugs (via ivy cache), which is required to resolve javax.annotation.*;

explicit module names have precedence over identifier declarations

check explicit module names for conformity

list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors

support indirect corecursion

tuned proofs;

tuned proofs;

tuned proofs;

tuned;

tuned proofs;

interpret keys more movement only when needed;

non-persistent print_state: trade-off between JVM space vs. ML time;

some explicit indication of Proof General legacy;

merge

various refactoring; handle self-mappings; handle range types containing function types;

expose basic Symbol.properties (uninterpreted);

tuned proofs;

remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); handle KP_UP/KP_DOWN keys as well, like Swing does;

no completion on backspace -- too intrusive, e.g. when deleting keywords;

more contributors;

updated TPTP parser to conform to version 5.5.0 (but excluding the TPI language since its parser spec is still incomplete);

updated TPTP parser to conform to version 5.4.0; clarified abstract syntax for 'let' in TPTP_Syntax (and in the parser); improved parsing of 'let' (in TFF) -- previously it wasn't looking at the structure of the definition; fixed bug when parsing 'let' (in TFF and THF) -- was only keeping the first quantified variable, and ignoring the rest; added comments to remind that 'let' support for THF is currently broken in TPTP;

included axiom formulas (removing a FIXME) in the imported problem; turned tests into asserts; changed problem to one which actually succeeds using z3;

updated syntax to use 'ML_file' rather than 'uses';

now allowing numeric identifiers to be used in 'file' annotations; more informative failure of missed cases by raising ANNOT_STRUCTURE instead of the default Match;

get_file_list now returns files sorted by size;