clarified proof_result: finish proof formally via head tr, not end_tr;

tuned;

more robust Future.fulfill wrt. duplicate assignment and interrupt;

tuned message;

always signal after cancel_group: passive tasks may have become active;

just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update; explicit terminate_execution; tuned source structure;

merged

moved lift_raw_const wrapper out of the Quotient-package into Nominal2

misc tuning and simplification;

static relevance of proof via syntax keywords;

tuned future priorities: print 0, goal ~1, execute ~2;

updated for Poly/ML SVN 1476;

some coverage of HOL/TPTP;

added graph-conversion utility for TPTP files

moved non-interpret-specific code to different module

disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts;

tuned proofs;

slightly faster default compilation of Isabelle/Scala;

more explicit last exec result;

dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result; discontinued odd "touched" field -- check given edits directly;

tuned;

simplified Future.cancel/cancel_group (again) -- running threads only; more robust update/cancel_execution: full join_tasks of group before exec state assignment; tuned signature;

added ML pretty-printing;

merged