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);

fixed odd runtime type error, which appears to have escaped the scala-2.8.0.final compiler;

YXML.parse: refrain from interning, let XML.Cache do it (partially);

cache_string: store trimmed string value;

simple_dialog: allow scala.swing.Component as well;

simplified some Markup;

simplified type XML.Tree: embed Markup directly, avoid slightly odd triple; XML.cache_tree: actually store XML.Text as well; added Isabelle_Process.Result.properties;

more robust treatment of Markup.token;

simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;

concentrate structural document notions in document.scala; tuned;

maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);

tuned;

more explicit model of pending text edits;

more explicit treatment of Swing thread context; Document_Model.snapshot: require Swing thread;

replaced individual Document_Model history by all-inclusive one in Session; Document_Model: provide thy_name externally, i.e. by central Isabelle plugin; tuned;

misc tuning and clarification;

avoid null in Scala; tuned comments;

updated keywords;

removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);

merged

merged

quotient types registered as codatatypes are no longer quotient types

added a friendly warning

extend the scope of limitation about nonconservative extensions

improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"

Remove duplicate locale activation code; performance improvement.

added record field

added "whack"

handle "Rep_unit" & Co. gracefully

added support for "Abs_" and "Rep_" functions on quotient types

fiddle with specialization etc.

handle inductive predicates correctly after change in "def" semantics

don't specialize built-ins or constructors

more docs

prevent the expansion of too large definitions -- use equations for these instead

make nitpick accept "==" for "nitpick_(p)simp"s

fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization

deal correctly with Pure.conjunction in mono check

rename internal functions

remove buggy and needless condition

renamed internal function

Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities

avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)

improve datatype symmetry breaking; all based on "datatype bin_list = BNil | B0Cons bin_list | B1Cons bin_list" example

merged

make SML/NJ happy

get rid of all "optimizations" regarding "unit" and other cardinality-1 types

tuning

better "Pretty" handling

change formula for enumerating scopes

example tweaking -- also prevents Nitpick_Tests from using more than 1 thread

speed up Nitpick examples a little bit

minor changes

updated example timings

more helpful message

also mention gfp

bump up the max cardinalities, to use up more of the time given to us by the user

make tracing monotonicity easier

more documentation, based on email discussions with a user

make example easier to parse

clarify attribute documentation