merged

added Lars Noschinski to isatest report

merged

discontinued separation of `define` and `declare_const`

unravelled target initialization code

added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)

added scanning of if-then-else expressions

merged

added support for partial quotient types; previously Nitpick was unsound for these

adapt occurrences of renamed Nitpick functions

document the non-legacy interfaces

local versions of Nitpick.register_xxx functions

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;