recode utf8 for ML, as done in feeder.pl;

more explicit read-only non-TTY mode;

clarified options;

specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;

tuned;

test recent polyml-svn, which is becoming polyml-5.5.1;

minor doc fixes

more (co)datatype docs

more (co)datatype documentation

merged

removed duplicate lemma

more (co)datatype documentation

tuning

more (co)datatype docs

tuned proof;

recovered "\<phi>\<^isub>i" from 0b02aaf7c7c5;

proper border (again) -- avoid NPE on Windows; uniform non-opaqueness -- relevant for Windows L&F;

NEWS;

added home-made tooltips; tuned signature;

home-grown mouse handling to pretend that the painted checkbox is actually a Swing component; tuned signature;

actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable); just one module for Isabelle/jEdit actions;

added Getting Started text

more robust tactic

merged

clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);

simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;

paint unassigned/unchanged nodes as unprocessed -- relevant for editor_continuous_checking = false;

allow explicit indication of required node: full eval, no prints;

simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);

more work on (co)datatype docs

more (co)datatype documentation

merged

tuned proofs;

more uniform border;

proper PIDE markup for codegen arguments;

less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace; propagate flush from ML to Scala via special protocol message; more formal type Message_Channel.message;

tuned -- more uniform ML vs. Scala;

recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;

more timing;

more timing; tuned -- Execution.is_running always holds due to immediate start;

removed spurious headings

more (co)datatype documentation

avoid DUP error in local context

sketched documentation for new (co)datatype package

tuned docs (the function package isn't so new anymore)

tuned comments;

tuned;

type theory is purely value-oriented;

pro-forma Execution.reset, despite lack of final join/commit;

tuned signature; removed notoriously outdated comments;

tuned;

de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;

merged

tuned intro

silenced subsumption warnings for default code equations entirely

merged

NEWS; tuned description;

tuned proofs;

updated key bindings to execution range;

traverse node on change of "required" state;

keep memo_exec execution running, which is important to cancel goal forks eventually; run as nested worker task to keep main group valid, even after cancelation of removed subgroups; do not memoize interrupt, but absorb it silently in main execution; Goal.purge_futures: rough sanity check of group status;

maintain explicit execution frontier: avoid conflict with former task via static dependency; start execution immediate after assignment, to keep frontier simple;

afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;

clarified conditions for node traversal;