tuning

export ML function (for primcorec)

more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;

tuned proofs;

slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;

remove overlay after result has arrived -- one-shot query operation;

more message markup, provided by prover;

tuned signature -- more uniform treatment of overlays as command mapping;

commands with overlay remain visible, to avoid loosing printed output;

initial update of nodes_required, for proper GUI state;

tuned signature;

avoid repeated PIDE.flush_buffers when manipulating overlays;

tuned proofs;

merged

some actual find_theorems functionality;

more general Output.result: allow to update arbitrary properties; clarified kind/instance of overlay GUI component, with separate output (subject to version as main Output);

prefer canonical order, to avoid potential fluctuation due to front-end edits;

tuned signature;

minimal print function "find_theorems", which merely echos its arguments;

support print functions with explicit arguments, as provided by overlays;

maintain overlays within node perspective; tuned signature;

some tracking of command location; tuned;

tuned proofs;

dockable window for "find" dialog (GUI only);

tuned;

more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)

more (co)datatype docs

tuned exercises

more (co)datatype documentation

more (co)datatype documentation

store relator induction in fp_result

merged

optional static analysis for Poly/ML 5.5.x;

exception trace for Poly/ML 5.5.1, using regular Isabelle output;

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;