Parsing errors during proof reconstruction now give rise to an intelligible error message.

rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs; misc cleanup of mathematical glyphs, with bold version synthesized by fontforge;

tuned initial properties/perspective;

provide JEDIT_SETTINGS via settings; provide default perspective; tuned default properties;

updated version and dependencies;

recovered subscript (cf. ded5b770ec1c);

formal antiquotations for ML snippets; no "open" unsynchronized references

clarified terminology;

merged

added code certificates

tuned code equations

Matrices form a semiring with 0

incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);

ignore some src/Tools/jEdit stuff;

merged with converted/relocated copy of http://isabelle.in.tum.de/repos/isabelle-jedit/rev/93d884afa74b

more timing;

more tobust treatment of Document.current_state; some timing;

new unparsed span for text right after existing command; tuned;

Outer_Lex.is_ignored;

simplified Text_Edit;

eliminated strange mutable var commands; removed_commands: refer to old commands; misc tuning;

updated header;

eliminated obsolete isabelle.proofdocument.Token;

do not override Command.hashCode -- which was inconsistent with eq anyway; unparsed: no id, commands observe pointer equality; actually invoke edit_commands; more correct doc_edits; tuned;

renamed Command.content to source; reorganization of document parsing, using command spans etc. -- initial setup;

further tuning of command_start;

refrain from poking blink rate -- might get stuck in invisible state;

eliminated Command.stop, which tends to case duplicate traversal of commands;

iterators for ranges of commands/starts -- avoid extra array per document; try/finally for saved_color; misc tuning;

tuned document changes;

misc tuning and clarification of Document/Change;

adhoc reset of blink rate; bind "console" instance;