| Sat, 19 Dec 2020 00:04:32 +0100 |
wenzelm |
clarified markup: open URL as editor file;
|
file |
diff |
annotate
|
| Fri, 18 Dec 2020 23:30:29 +0100 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Fri, 18 Dec 2020 23:19:07 +0100 |
wenzelm |
improved markup for theory header imports;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 13:51:56 +0200 |
wenzelm |
more accurate context position reports;
|
file |
diff |
annotate
|
| Wed, 02 Oct 2019 14:45:37 +0200 |
wenzelm |
more robust: avoid update/interrupt of long-running print_consolidation;
|
file |
diff |
annotate
|
| Mon, 30 Sep 2019 17:28:40 +0200 |
wenzelm |
obsolete (see 030a6baa5cb2 and d14ddb1df52c);
|
file |
diff |
annotate
|
| Fri, 13 Sep 2019 11:00:59 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2019 19:44:54 +0200 |
wenzelm |
prefer commands_accepted: fewer protocol messages;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2019 17:10:23 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2019 16:48:28 +0200 |
wenzelm |
tuned signature -- prefer bulk messages;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Sun, 19 May 2019 18:10:45 +0200 |
wenzelm |
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
|
file |
diff |
annotate
|
| Sun, 19 May 2019 14:14:56 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 18 May 2019 13:23:36 +0200 |
wenzelm |
tuned signature (following Scala version);
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 23:57:07 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 13:19:13 +0100 |
wenzelm |
clarified Toplevel.state: more explicit types;
|
file |
diff |
annotate
|
| Wed, 20 Feb 2019 21:54:52 +0100 |
wenzelm |
physical vs. logical events, the latter takes GC time into account;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2018 17:16:36 +0200 |
wenzelm |
clarified message;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2018 13:38:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 14:02:14 +0200 |
wenzelm |
always consolidate: allow errors in presentation;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2018 16:12:26 +0200 |
wenzelm |
less wasteful consolidation, based on PIDE front-end state and recent changes;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2018 14:15:49 +0200 |
wenzelm |
tuned -- short-circuit result;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2018 22:16:44 +0200 |
wenzelm |
proper function invocation with all arguments;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2018 22:02:20 +0200 |
wenzelm |
fork parallel prints early in execution: avoid degradation of priority due to main eval task;
|
file |
diff |
annotate
|
| Sat, 02 Jun 2018 21:59:11 +0200 |
wenzelm |
record active execution task and depend on it -- avoid new executions bumping into old ones;
|
file |
diff |
annotate
|
| Fri, 01 Jun 2018 10:56:01 +0200 |
wenzelm |
clarified priority;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 29 May 2018 22:25:59 +0200 |
wenzelm |
more node status information;
|
file |
diff |
annotate
|
| Wed, 16 May 2018 21:07:12 +0200 |
wenzelm |
clarified "consolidation" vs. "presentation";
|
file |
diff |
annotate
|
| Mon, 14 May 2018 22:22:47 +0200 |
wenzelm |
support for dynamic document output while editing;
|
file |
diff |
annotate
|
| Wed, 24 Jan 2018 19:50:00 +0100 |
wenzelm |
tuned: prefer list operations over Source.source;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 22:36:02 +0100 |
wenzelm |
clarified implicit Pure.thy;
|
file |
diff |
annotate
|
| Sat, 16 Dec 2017 16:46:01 +0100 |
wenzelm |
PIDE markup for session ROOT files;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 14:06:24 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 11:20:19 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 22 Jun 2017 15:20:32 +0200 |
wenzelm |
more informative task_statistics;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2017 22:36:32 +0200 |
wenzelm |
more qualifier treatment, but in the end it is still ignored;
|
file |
diff |
annotate
|
| Mon, 03 Apr 2017 13:39:13 +0200 |
wenzelm |
simplified direct theory name (again, see also 570ba266f5b5, 2a7f9e79cb28);
|
file |
diff |
annotate
|
| Tue, 19 Apr 2016 12:06:34 +0200 |
wenzelm |
more IDE support for Isabelle/Pure bootstrap;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 19:30:15 +0200 |
wenzelm |
support ROOT0.ML as well -- independently of ROOT.ML;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 23:45:19 +0200 |
wenzelm |
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 23:29:05 +0200 |
wenzelm |
prefer infix operations;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 15:23:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 23:10:23 +0200 |
wenzelm |
thread context for exceptions from forks, e.g. relevant when printing errors;
|
file |
diff |
annotate
|
| Sat, 15 Aug 2015 19:42:35 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Mon, 10 Aug 2015 20:22:49 +0200 |
wenzelm |
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
|
file |
diff |
annotate
|
| Fri, 24 Apr 2015 20:33:10 +0200 |
wenzelm |
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:23:36 +0200 |
wenzelm |
clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 16:00:19 +0200 |
wenzelm |
more position information and PIDE markup for command keywords;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 15:21:41 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 14:15:15 +0100 |
wenzelm |
more precises positions;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 13:32:31 +0100 |
wenzelm |
avoid duplicate header errors, more precise positions;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 19:21:15 +0100 |
wenzelm |
hybrid use of command blobs: inlined errors and auxiliary files;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2015 12:58:49 +0100 |
wenzelm |
simplified Command.resolve_files in ML, using blobs_index from Scala;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2015 11:47:42 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2015 22:00:51 +0100 |
wenzelm |
clarified markup for embedded files, early before execution;
|
file |
diff |
annotate
|
| Sun, 11 Jan 2015 12:46:19 +0100 |
wenzelm |
more explicit errors;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 22:34:28 +0100 |
wenzelm |
node-specific keywords, with session base syntax as default;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 20:45:20 +0100 |
wenzelm |
clarified define_command: send tokens more directly, without requiring keywords in ML;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 14:04:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 15:44:32 +0100 |
wenzelm |
even more exception traces for Document.update, which goes through additional execution wrappers;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 20:06:18 +0100 |
wenzelm |
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 15:47:04 +0100 |
wenzelm |
more explicit Keyword.keywords;
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 11:44:41 +0100 |
wenzelm |
simplified keyword kinds;
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 20:18:27 +0200 |
wenzelm |
tuned signature according to Scala version -- prefer explicit argument;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 00:08:32 +0200 |
wenzelm |
separate module Command_Span: mostly syntactic representation;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2014 11:43:58 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 13:48:00 +0200 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 10:38:46 +0200 |
wenzelm |
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 14:50:20 +0200 |
wenzelm |
avoid redundant data structure;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 13:01:30 +0200 |
wenzelm |
more explicit discrimination of empty nodes -- suppress from Theories panel;
|
file |
diff |
annotate
|
| Wed, 30 Apr 2014 22:34:11 +0200 |
wenzelm |
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
|
file |
diff |
annotate
|
| Mon, 07 Apr 2014 23:02:29 +0200 |
wenzelm |
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
|
file |
diff |
annotate
|
| Mon, 07 Apr 2014 13:06:34 +0200 |
wenzelm |
separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 17:39:03 +0100 |
wenzelm |
clarifed module name;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 11:48:14 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 11:46:54 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 17:29:58 +0100 |
wenzelm |
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
|
file |
diff |
annotate
|
| Fri, 22 Nov 2013 21:13:44 +0100 |
wenzelm |
clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
|
file |
diff |
annotate
|
| Fri, 22 Nov 2013 20:28:49 +0100 |
wenzelm |
more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 11:55:52 +0100 |
wenzelm |
load files that are not provided by PIDE blobs;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 19:33:27 +0100 |
wenzelm |
maintain blobs within document state: digest + text in ML, digest-only in Scala;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 13:13:51 +0100 |
wenzelm |
proper theory name vs. node name;
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 17:16:56 +0100 |
wenzelm |
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 15:29:10 +0200 |
wenzelm |
tuned signature -- more uniform treatment of overlays as command mapping;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 16:00:14 +0200 |
wenzelm |
support print functions with explicit arguments, as provided by overlays;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 14:26:09 +0200 |
wenzelm |
maintain overlays within node perspective;
|
file |
diff |
annotate
|
| Wed, 31 Jul 2013 12:46:53 +0200 |
wenzelm |
simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
|
file |
diff |
annotate
|
| Wed, 31 Jul 2013 12:14:13 +0200 |
wenzelm |
allow explicit indication of required node: full eval, no prints;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 18:19:16 +0200 |
wenzelm |
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 16:22:07 +0200 |
wenzelm |
more timing;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 16:01:19 +0200 |
wenzelm |
more timing;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 11:38:43 +0200 |
wenzelm |
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 19:55:38 +0200 |
wenzelm |
traverse node on change of "required" state;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 18:59:58 +0200 |
wenzelm |
keep memo_exec execution running, which is important to cancel goal forks eventually;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 16:52:04 +0200 |
wenzelm |
maintain explicit execution frontier: avoid conflict with former task via static dependency;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 15:59:47 +0200 |
wenzelm |
clarified conditions for node traversal;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 15:20:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 13:24:15 +0200 |
wenzelm |
discontinued notion of "stable" result -- running execution is never canceled;
|
file |
diff |
annotate
|
| Sat, 20 Jul 2013 16:29:06 +0200 |
wenzelm |
document update at high priority -- important;
|
file |
diff |
annotate
|
| Sat, 20 Jul 2013 16:27:55 +0200 |
wenzelm |
option editor_execution_priority;
|
file |
diff |
annotate
|
| Mon, 15 Jul 2013 10:25:35 +0200 |
wenzelm |
more careful termination of removed execs, leaving running execs undisturbed;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 12:04:16 +0200 |
wenzelm |
clarified execution: maintain running execs only, check "stable" separately via memo (again);
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 11:28:03 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 11:07:02 +0200 |
wenzelm |
clarified module name;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 23:24:40 +0200 |
wenzelm |
more explicit type Exec.context;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 18:41:05 +0200 |
wenzelm |
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 16:26:14 +0200 |
wenzelm |
more abstract types;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 16:01:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 14:42:11 +0200 |
wenzelm |
global management of command execution fragments;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 12:28:24 +0200 |
wenzelm |
fully synchronized guard of running execution;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 11:37:06 +0200 |
wenzelm |
re-assign prints of unchanged eval only -- avoid crash of new_exec;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 11:09:23 +0200 |
wenzelm |
tuned -- refrain from odd optimization;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 10:43:53 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|