find command span in buffer; tuned signature;

'notepad' requires proper nesting of begin/end;

explicit keyword category for commands that may start a block;

updated keywords;

'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;

more abstract type;

tuned;

tuned;

updated to jdk-7u72;

increase chances that HOL-Proofs image still works for polyml-5.3.0;

JRE is sufficient for official release -- javac and jar are only needed for self-build;

clarified ISABELLE_JDK_HOME vs. JAVA_HOME;

ISABELLE_JAVA_EXT is obsolete; no censorship of ISABELLE_JDK_HOME;

further generalization of natfloor_div_nat

generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div

eliminated redundancies; more simp rules

more simp rules; slight proof tuning

clarified default;

support negative extraLineSpacing; updated ErrorList.jar 2.3;

tuned whitespace; more symbols;

made SML/NJ happy;

merged;

discontinued python from standard system environment;

more generous default;

even further downshift of theory Parity in the hierarchy

further downshift of theory Parity in the hierarchy

use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating

move NO_MATCH simproc from the AFP entry Graph_Theory to HOL

repaired long-standing accident

explicit definition restores HOL Light import after cb9d84d3e7f2

tuned language and spelling

slight generalization and unification of simp rules for algebraic procedures

downshift of theory Parity in the hierarchy

parity induction over natural numbers

merged

proper line height and text base line, like regular TextAreaPainter.PaintText;

tuned imports;

merged

add print translation for probability notation \<P>

find main command keyword of 'begin';

restricted scanning;

repaired rail diagram (cf. 8450b944e58a);

foldPainter like Windows L&F;

merged

NEWS;

tuned whitespace;

ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);

support for proof structure matching;

tuned;

tuned;

support for begin/end matching;

proper token kind;

added option jedit_structure_limit; tuned signature;

some structure matching, based on line token iterators;

support for structure matching; misc tuning;

tuned rendering;