src/Pure/PIDE/document.ML
2011-09-01 wenzelm 2011-09-01 amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example); clarified touch_node: reset result explicitly;
2011-09-01 wenzelm 2011-09-01 more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
2011-08-31 wenzelm 2011-08-31 explicit running_color; stronger colors for overview, more transparent colors for status within text;
2011-08-31 wenzelm 2011-08-31 tuned join_commands: avoid traversing cumulative table;
2011-08-27 wenzelm 2011-08-27 more precise treatment of nodes that are fully required for partially visible ones;
2011-08-26 wenzelm 2011-08-26 tuned signature -- iterate subsumes both fold and get_first;
2011-08-26 wenzelm 2011-08-26 further clarification of Document.updated, based on last_common and after_entry; tuned;
2011-08-26 wenzelm 2011-08-26 tuned signature;
2011-08-26 wenzelm 2011-08-26 improved Document.edit: more accurate update_start and no_execs; tuned;
2011-08-26 wenzelm 2011-08-26 refined document state assignment: observe perspective, more explicit assignment message; misc tuning and clarification;
2011-08-25 wenzelm 2011-08-25 tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
2011-08-25 wenzelm 2011-08-25 propagate information about last command with exec state assignment through document model;
2011-08-24 wenzelm 2011-08-24 misc tuning and simplification;
2011-08-24 wenzelm 2011-08-24 tuned pri: prefer purging of canceled execution;
2011-08-24 wenzelm 2011-08-24 tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
2011-08-24 wenzelm 2011-08-24 misc tuning and simplification;
2011-08-24 wenzelm 2011-08-24 ignore irrelevant timings;
2011-08-24 wenzelm 2011-08-24 print state only for visible command, to avoid wasting resources for the larger part of the text;
2011-08-24 wenzelm 2011-08-24 update_perspective without actual edits, bypassing the full state assignment protocol; edit_nodes/Perspective: do not touch_descendants here; propagate editor scroll events via update_perspective; misc tuning;
2011-08-23 wenzelm 2011-08-23 tuned;
2011-08-23 wenzelm 2011-08-23 some support for toplevel printing wrt. editor perspective (still inactive);
2011-08-23 wenzelm 2011-08-23 propagate editor perspective through document model;
2011-08-22 wenzelm 2011-08-22 some support for editor perspective;
2011-08-20 wenzelm 2011-08-20 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-08-20 wenzelm 2011-08-20 added Future.joins convenience; clarified Future.map: based on Future.cond_forks;
2011-08-19 wenzelm 2011-08-19 tuned;
2011-08-19 wenzelm 2011-08-19 tuned signature (again); tuned;
2011-08-19 wenzelm 2011-08-19 tuned signature -- treat structure Task_Queue as private to implementation;
2011-08-19 wenzelm 2011-08-19 refined Future.cancel: explicit future allows to join actual cancellation; Document.cancel_execution: join nested future groups as well;
2011-08-18 wenzelm 2011-08-18 more precise treatment of exception nesting and serial numbers;
2011-08-18 wenzelm 2011-08-18 more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-17 wenzelm 2011-08-17 more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;
2011-08-16 wenzelm 2011-08-16 workaround for Cygwin, to make it work in the important special case without extra files;
2011-08-16 wenzelm 2011-08-16 more robust treatment of node dependencies in incremental edits;
2011-08-16 wenzelm 2011-08-16 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; more robust treatment of node dependencies; misc tuning;
2011-08-15 wenzelm 2011-08-15 touch descendants of edited nodes; more precise handling of Graph exceptions;
2011-08-15 wenzelm 2011-08-15 parellel scheduling of node edits and execution;
2011-08-15 wenzelm 2011-08-15 tuned error message;
2011-08-15 wenzelm 2011-08-15 retrieve imports from document state, with fall-back on theory loader for preloaded theories; misc tuning;
2011-08-15 wenzelm 2011-08-15 explicit check of finished evaluation;
2011-08-15 wenzelm 2011-08-15 refined Document.edit: less stateful update via Graph.schedule; clarified node result -- more direct get_theory; clarified Document.joint_commands;
2011-08-15 wenzelm 2011-08-15 simplified exec: eliminated unused status flag;
2011-08-13 wenzelm 2011-08-13 simplified Toplevel.init_theory: discontinued special master argument;
2011-08-13 wenzelm 2011-08-13 provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment;
2011-08-13 wenzelm 2011-08-13 clarified node header -- exclude master_dir;
2011-08-13 wenzelm 2011-08-13 maintain node header; misc tuning and clarification;
2011-08-12 wenzelm 2011-08-12 clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-08-11 wenzelm 2011-08-11 uniform treatment of header edits as document edits;
2011-08-11 wenzelm 2011-08-11 explicit datatypes for document node edits;
2011-08-10 wenzelm 2011-08-10 future_job: explicit indication of interrupts;
2011-07-11 wenzelm 2011-07-11 tuned signature -- corresponding to Scala version;
2011-07-10 wenzelm 2011-07-10 propagate header changes to prover process; simplified Document case classes; Document.State.assignments: indexed by Version_ID;
2011-07-08 wenzelm 2011-07-08 moved global state to structure Document (again);
2011-07-05 wenzelm 2011-07-05 get theory from last executation state; tuned error messages;
2011-07-05 wenzelm 2011-07-05 clarified cancel_execution/await_cancellation;
2011-07-02 wenzelm 2011-07-02 tuned;
2011-04-11 wenzelm 2011-04-11 more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2011-01-31 wenzelm 2011-01-31 tuned signature; tuned vacous forks;
2011-01-31 wenzelm 2011-01-31 support named tasks, for improved tracing;