simplified/generalized ISABELLE_FONTS handling;

updated to jedit_build-20110620;

added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;

clean up SPASS FLOTTER hack

remove automatic recovery from (some) unsound proofs, now that we use sound encodings for all the interesting provers

only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded

slightly better setup for E

respect "really_all" argument, which is used by "ATP_Export"

slightly better setup for SPASS and Vampire as more results have come in

optimized SPASS and Vampire time slices, like E before

optimized E's time slicing, based on latest exhaustive Judgment Day results

deal with ATP time slices in a more flexible/robust fashion

literal unicode in README.html allows to copy/paste from Lobo output;

merged;

explain special control symbols;

accept control symbols;

fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies

recognize one more E failure message

tweaked TPTP formula kind for typing information used in the conjecture

more forceful message

treat quotes as non-controllable, to reduce surprise in incremental editing;

abbreviations for special control symbols;

completion for control symbols;

updated to jedit_build-20110619;

support for bold style within text buffer; hidden: white foreground;

tuned;

discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);

added glyphs 21e0..21e4, 21e6..21e9, 2759 from DejaVuSansMono;

names for control symbols without "^", which is relevant for completion;

some unicode chars for special control symbols;

tuned;

tuned markup;

avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;

proper gfx.setColor;

proper x1; tuned;

convenience functions;

more robust caret painting wrt. surrogate characters; discontinued glyphvector drawing -- less special cases;

do not control malformed symbols;

Buffer.editSyntaxStyle: mask extended syntax styles;

hardwired abbreviations for standard control symbols;

updated to jedit_build-20110618, which is required for sub/superscript rendering;

basic support for extended syntax styles: sub/superscript;

tuned -- Map.empty serves as partial function;

proper place for config files (cf. 55866987a7d9);

tuned signature;

merged

IMP compiler with int, added reverse soundness direction

proper place for config files;

tuned markup;

highlight via foreground painter, using alpha channel;

tuned signature;

tuned text;

inner literal/delimiter corresponds to outer keyword/operator;

tuned markup;

more uniform treatment of "keyword" vs. "operator";

simplified Line_Context (again);

more robust treatment of partial range restriction;

select_markup: no filtering here -- results may be distorted anyway;

more explicit treatment of ranges after revert/convert, which may well distort the overall start/end positions;

more explicit error message; convert/revert range; tuned;

merged

gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"

added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users

fixed soundness bug related to extensionality

unconditional recovery from bad context (e.g. Quoted with malformed quoted_body);

flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);

recovered markup for non-alphabetic keywords;

more precise imitation of original TextAreaPainter: no locking;

more precise imitatation of original TokenMarker: no locking, interned context etc.;

brute-force range restriction to avoid spurious crashes;

static token markup, based on outer syntax only; eliminated obsolete buffer.propertiesChanged (expensive due to remarking of full buffer etc.);

explicit dependency on Pure.jar;

partial scans of nested comments;

some support for partial scans with explicit context; clarified junk vs. junk1;

tuned spelling

updated generated file;

merged

spelling

avoid compiler warning -- this is unchecked anyway;

tuned messages;

uniform use of Document_View.robust_body;

merged

merge

fixed soundness bug made more visible by previous change

use more appropriate type systems for ATP exporter

type arguments now (unlike back when fa2cf11d6351 was done) normally carry enough information to reconstruct the type of an applied constant, so no need to constraint the argument types in those cases

more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);

more robust init;

recovered orig_text_painter from f4141da52e92;

tuned;

more elaborate syntax styles;

more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);

paint caret according to precise font metrics;

include scala mode;

builtin sub/superscript styles for jedit-4.3.2;

merged