src/Pure/PIDE/document.ML
Sat, 27 Aug 2011 13:26:06 +0200 wenzelm more precise treatment of nodes that are fully required for partially visible ones;
Fri, 26 Aug 2011 21:27:58 +0200 wenzelm tuned signature -- iterate subsumes both fold and get_first;
Fri, 26 Aug 2011 21:18:42 +0200 wenzelm further clarification of Document.updated, based on last_common and after_entry;
Fri, 26 Aug 2011 16:06:58 +0200 wenzelm tuned signature;
Fri, 26 Aug 2011 15:56:30 +0200 wenzelm improved Document.edit: more accurate update_start and no_execs;
Fri, 26 Aug 2011 15:09:54 +0200 wenzelm refined document state assignment: observe perspective, more explicit assignment message;
Thu, 25 Aug 2011 19:12:58 +0200 wenzelm tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
Thu, 25 Aug 2011 16:44:06 +0200 wenzelm propagate information about last command with exec state assignment through document model;
Wed, 24 Aug 2011 17:25:45 +0200 wenzelm misc tuning and simplification;
Wed, 24 Aug 2011 17:16:48 +0200 wenzelm tuned pri: prefer purging of canceled execution;
Wed, 24 Aug 2011 17:14:31 +0200 wenzelm tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
Wed, 24 Aug 2011 15:55:43 +0200 wenzelm misc tuning and simplification;
Wed, 24 Aug 2011 15:30:43 +0200 wenzelm ignore irrelevant timings;
Wed, 24 Aug 2011 13:40:10 +0200 wenzelm print state only for visible command, to avoid wasting resources for the larger part of the text;
Wed, 24 Aug 2011 13:03:39 +0200 wenzelm update_perspective without actual edits, bypassing the full state assignment protocol;
Tue, 23 Aug 2011 21:19:24 +0200 wenzelm tuned;
Tue, 23 Aug 2011 15:48:41 +0200 wenzelm some support for toplevel printing wrt. editor perspective (still inactive);
Tue, 23 Aug 2011 12:20:12 +0200 wenzelm propagate editor perspective through document model;
Mon, 22 Aug 2011 21:42:02 +0200 wenzelm some support for editor perspective;
Sat, 20 Aug 2011 23:35:30 +0200 wenzelm refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
Sat, 20 Aug 2011 15:52:29 +0200 wenzelm added Future.joins convenience;
Fri, 19 Aug 2011 18:01:23 +0200 wenzelm tuned;
Fri, 19 Aug 2011 17:39:37 +0200 wenzelm tuned signature (again);
Fri, 19 Aug 2011 16:13:26 +0200 wenzelm tuned signature -- treat structure Task_Queue as private to implementation;
Fri, 19 Aug 2011 15:56:26 +0200 wenzelm refined Future.cancel: explicit future allows to join actual cancellation;
Thu, 18 Aug 2011 18:07:40 +0200 wenzelm more precise treatment of exception nesting and serial numbers;
Thu, 18 Aug 2011 17:53:32 +0200 wenzelm more careful treatment of exception serial numbers, with propagation to message channel;
Wed, 17 Aug 2011 22:14:22 +0200 wenzelm more systematic handling of parallel exceptions;
Tue, 16 Aug 2011 23:17:26 +0200 wenzelm workaround for Cygwin, to make it work in the important special case without extra files;
Tue, 16 Aug 2011 21:50:53 +0200 wenzelm more robust treatment of node dependencies in incremental edits;
Tue, 16 Aug 2011 21:13:52 +0200 wenzelm use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
Mon, 15 Aug 2011 21:54:32 +0200 wenzelm touch descendants of edited nodes;
Mon, 15 Aug 2011 21:05:30 +0200 wenzelm parellel scheduling of node edits and execution;
Mon, 15 Aug 2011 20:38:16 +0200 wenzelm tuned error message;
Mon, 15 Aug 2011 20:19:41 +0200 wenzelm retrieve imports from document state, with fall-back on theory loader for preloaded theories;
Mon, 15 Aug 2011 19:27:55 +0200 wenzelm explicit check of finished evaluation;
Mon, 15 Aug 2011 16:38:42 +0200 wenzelm refined Document.edit: less stateful update via Graph.schedule;
Mon, 15 Aug 2011 14:54:36 +0200 wenzelm simplified exec: eliminated unused status flag;
Sat, 13 Aug 2011 20:41:29 +0200 wenzelm simplified Toplevel.init_theory: discontinued special master argument;
Sat, 13 Aug 2011 20:20:36 +0200 wenzelm provide node header via Scala layer;
Sat, 13 Aug 2011 15:59:26 +0200 wenzelm clarified node header -- exclude master_dir;
Sat, 13 Aug 2011 13:42:35 +0200 wenzelm maintain node header;
Fri, 12 Aug 2011 15:28:30 +0200 wenzelm clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
Thu, 11 Aug 2011 20:32:44 +0200 wenzelm uniform treatment of header edits as document edits;
Thu, 11 Aug 2011 18:01:28 +0200 wenzelm explicit datatypes for document node edits;
Wed, 10 Aug 2011 16:05:14 +0200 wenzelm future_job: explicit indication of interrupts;
Mon, 11 Jul 2011 22:55:47 +0200 wenzelm tuned signature -- corresponding to Scala version;
Sun, 10 Jul 2011 00:21:19 +0200 wenzelm propagate header changes to prover process;
Fri, 08 Jul 2011 22:00:53 +0200 wenzelm moved global state to structure Document (again);
Tue, 05 Jul 2011 20:36:49 +0200 wenzelm get theory from last executation state;
Tue, 05 Jul 2011 11:45:48 +0200 wenzelm clarified cancel_execution/await_cancellation;
Sat, 02 Jul 2011 20:22:02 +0200 wenzelm tuned;
Mon, 11 Apr 2011 17:23:20 +0200 wenzelm more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;
Sun, 20 Mar 2011 21:28:11 +0100 wenzelm structure Timing: covers former start_timing/end_timing and Output.timeit etc;
Mon, 31 Jan 2011 23:02:53 +0100 wenzelm tuned signature;
Mon, 31 Jan 2011 22:57:01 +0100 wenzelm support named tasks, for improved tracing;
Mon, 31 Jan 2011 21:54:49 +0100 wenzelm more direct Future.bulk, which potentially reduces overhead for Par_List;
Thu, 27 Jan 2011 12:24:00 +0100 wenzelm cancel document execution before editing, to improve reactivity on systems with few cores;
Tue, 25 Jan 2011 21:26:25 +0100 wenzelm singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);
Tue, 25 Jan 2011 20:06:32 +0100 wenzelm workaround for odd x86_64 problem in Poly/ML 5.4.0 (actually SVN 1151?), which causes unexpected nontermination of Isabelle/Scala document editing;
less more (0) -60 tip