tweaked E, SPASS, Vampire setup based on latest Judgment Day results

remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations

avoid double ASCII-fication

make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity

generate type predicates for existentials/skolems, otherwise some problems might not be provable

insert rather than append special facts to make it less likely that they're truncated away

hidden font: full height makes cursor more visible;

more uniform treatment of recode_set/recode_map; HTML spans with user fonts;

tuned iteration over short symbols;

Symbol.is_ctrl: handle decoded version as well; clarified user font font index handling;

some support for user symbol fonts;

removed obsolete font specification;

more tolerant Symbol.decode;

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