src/Pure/PIDE/document.ML
Fri, 18 Dec 2020 23:30:29 +0100 wenzelm more robust;
Fri, 18 Dec 2020 23:19:07 +0100 wenzelm improved markup for theory header imports;
Fri, 27 Nov 2020 21:59:23 +0100 wenzelm clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
Fri, 03 Apr 2020 13:51:56 +0200 wenzelm more accurate context position reports;
Wed, 02 Oct 2019 14:45:37 +0200 wenzelm more robust: avoid update/interrupt of long-running print_consolidation;
Mon, 30 Sep 2019 17:28:40 +0200 wenzelm obsolete (see 030a6baa5cb2 and d14ddb1df52c);
Fri, 13 Sep 2019 11:00:59 +0200 wenzelm tuned;
Fri, 06 Sep 2019 19:44:54 +0200 wenzelm prefer commands_accepted: fewer protocol messages;
Fri, 06 Sep 2019 17:10:23 +0200 wenzelm clarified signature;
Fri, 06 Sep 2019 16:48:28 +0200 wenzelm tuned signature -- prefer bulk messages;
Mon, 26 Aug 2019 20:01:28 +0200 wenzelm added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier);
Sun, 19 May 2019 18:10:45 +0200 wenzelm more thorough assignment, e.g. when "purge" removes commands that were not assigned;
Sun, 19 May 2019 14:14:56 +0200 wenzelm tuned whitespace;
Sat, 18 May 2019 13:23:36 +0200 wenzelm tuned signature (following Scala version);
Sat, 09 Mar 2019 23:57:07 +0100 wenzelm clarified signature;
Sat, 09 Mar 2019 13:19:13 +0100 wenzelm clarified Toplevel.state: more explicit types;
Wed, 20 Feb 2019 21:54:52 +0100 wenzelm physical vs. logical events, the latter takes GC time into account;
Sat, 01 Sep 2018 17:16:36 +0200 wenzelm clarified message;
Sat, 01 Sep 2018 13:38:44 +0200 wenzelm tuned;
Fri, 29 Jun 2018 14:02:14 +0200 wenzelm always consolidate: allow errors in presentation;
Tue, 05 Jun 2018 16:12:26 +0200 wenzelm less wasteful consolidation, based on PIDE front-end state and recent changes;
Tue, 05 Jun 2018 14:15:49 +0200 wenzelm tuned -- short-circuit result;
Sun, 03 Jun 2018 22:16:44 +0200 wenzelm proper function invocation with all arguments;
Sun, 03 Jun 2018 22:02:20 +0200 wenzelm fork parallel prints early in execution: avoid degradation of priority due to main eval task;
Sat, 02 Jun 2018 21:59:11 +0200 wenzelm record active execution task and depend on it -- avoid new executions bumping into old ones;
Fri, 01 Jun 2018 10:56:01 +0200 wenzelm clarified priority;
Thu, 31 May 2018 22:27:13 +0200 wenzelm Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
Tue, 29 May 2018 22:25:59 +0200 wenzelm more node status information;
Wed, 16 May 2018 21:07:12 +0200 wenzelm clarified "consolidation" vs. "presentation";
Mon, 14 May 2018 22:22:47 +0200 wenzelm support for dynamic document output while editing;
Wed, 24 Jan 2018 19:50:00 +0100 wenzelm tuned: prefer list operations over Source.source;
Mon, 08 Jan 2018 22:36:02 +0100 wenzelm clarified implicit Pure.thy;
Sat, 16 Dec 2017 16:46:01 +0100 wenzelm PIDE markup for session ROOT files;
Tue, 08 Aug 2017 22:13:05 +0200 wenzelm maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
Mon, 07 Aug 2017 14:06:24 +0200 wenzelm tuned spelling;
Mon, 07 Aug 2017 11:20:19 +0200 wenzelm tuned;
Thu, 22 Jun 2017 15:20:32 +0200 wenzelm more informative task_statistics;
Sat, 08 Apr 2017 22:36:32 +0200 wenzelm more qualifier treatment, but in the end it is still ignored;
Mon, 03 Apr 2017 13:39:13 +0200 wenzelm simplified direct theory name (again, see also 570ba266f5b5, 2a7f9e79cb28);
Tue, 19 Apr 2016 12:06:34 +0200 wenzelm more IDE support for Isabelle/Pure bootstrap;
Sat, 09 Apr 2016 19:30:15 +0200 wenzelm support ROOT0.ML as well -- independently of ROOT.ML;
Wed, 06 Apr 2016 23:45:19 +0200 wenzelm treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
Sat, 02 Apr 2016 23:29:05 +0200 wenzelm prefer infix operations;
Thu, 03 Mar 2016 15:23:02 +0100 wenzelm clarified modules;
Tue, 01 Sep 2015 23:10:23 +0200 wenzelm thread context for exceptions from forks, e.g. relevant when printing errors;
Sat, 15 Aug 2015 19:42:35 +0200 wenzelm clarified context;
Mon, 10 Aug 2015 20:22:49 +0200 wenzelm set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
Fri, 24 Apr 2015 20:33:10 +0200 wenzelm always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
Sun, 12 Apr 2015 11:23:36 +0200 wenzelm clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
Mon, 06 Apr 2015 16:00:19 +0200 wenzelm more position information and PIDE markup for command keywords;
Tue, 17 Mar 2015 15:21:41 +0100 wenzelm misc tuning and simplification;
Mon, 16 Mar 2015 14:15:15 +0100 wenzelm more precises positions;
Mon, 16 Mar 2015 13:32:31 +0100 wenzelm avoid duplicate header errors, more precise positions;
Sun, 15 Mar 2015 19:21:15 +0100 wenzelm hybrid use of command blobs: inlined errors and auxiliary files;
Fri, 13 Mar 2015 12:58:49 +0100 wenzelm simplified Command.resolve_files in ML, using blobs_index from Scala;
Fri, 13 Mar 2015 11:47:42 +0100 wenzelm tuned;
Thu, 12 Mar 2015 22:00:51 +0100 wenzelm clarified markup for embedded files, early before execution;
Sun, 11 Jan 2015 12:46:19 +0100 wenzelm more explicit errors;
Mon, 29 Dec 2014 20:51:42 +0100 wenzelm clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
Sun, 28 Dec 2014 21:34:45 +0100 wenzelm eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
less more (0) -100 -60 tip