| Mon, 30 Jun 2025 12:42:21 +0200 |
wenzelm |
inline errors as "bad" markup;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2025 13:55:09 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 12 Nov 2024 11:32:07 +0100 |
wenzelm |
clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
|
file |
diff |
annotate
|
| Tue, 12 Nov 2024 11:16:36 +0100 |
wenzelm |
omit redundant compact_source (see e1abca2527da): Command_Span.unparsed consists of one token with the original source;
|
file |
diff |
annotate
|
| Tue, 12 Nov 2024 11:04:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 10 Nov 2024 15:11:04 +0100 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Sun, 10 Nov 2024 13:40:28 +0100 |
wenzelm |
minor performance tuning: avoid concatenation of existing string material;
|
file |
diff |
annotate
|
| Sat, 09 Nov 2024 21:34:38 +0100 |
wenzelm |
Document.Snapshot: support for multiple snippet_commands;
|
file |
diff |
annotate
|
| Fri, 08 Nov 2024 18:39:35 +0100 |
wenzelm |
clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);
|
file |
diff |
annotate
|
| Fri, 08 Nov 2024 18:34:33 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2023 12:00:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2023 19:48:54 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 12:53:28 +0200 |
wenzelm |
misc tuning: support "scalac -source 3.3";
|
file |
diff |
annotate
|
| Fri, 21 Jul 2023 17:06:53 +0200 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2023 17:14:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2023 17:00:22 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2023 16:44:15 +0100 |
wenzelm |
clarified session sources: theory and blobs are read from database, instead of physical file-system;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2023 15:53:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2023 15:42:00 +0100 |
wenzelm |
more direct access to session_sources, without somewhat fragile file-system operations;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2023 14:50:11 +0100 |
wenzelm |
tuned signature: avoid confusion with Document.Node.Blob and Command.Blob;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2023 12:58:00 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 01 Jan 2023 22:54:40 +0100 |
wenzelm |
tuned signature, following Url.append_path;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2022 20:26:28 +0100 |
wenzelm |
clarified generic path operations;
|
file |
diff |
annotate
|
| Sun, 18 Dec 2022 16:01:37 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2022 11:33:13 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 06 Nov 2022 19:25:48 +0100 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Sat, 01 Oct 2022 16:07:05 +0200 |
wenzelm |
tuned, following hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2022 15:05:28 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 16:08:30 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 15:59:28 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 15:41:46 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2021 22:31:11 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2021 13:04:29 +0100 |
wenzelm |
more informative errors: simplify diagnosis of spurious failures reported by users;
|
file |
diff |
annotate
|
| Sat, 09 Jan 2021 18:56:53 +0100 |
wenzelm |
discontinued odd absolute position (amending 85bcdd05c6d0, 1975f397eabb): it violates translation invariance of commands and may lead to redundant re-checking of PIDE document;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 22:22:34 +0100 |
wenzelm |
clarified signature: absorb XZ.Cache into XML.Cache;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2020 15:47:54 +0100 |
wenzelm |
present auxiliary files with PIDE markup;
|
file |
diff |
annotate
|
| Fri, 18 Dec 2020 23:19:07 +0100 |
wenzelm |
improved markup for theory header imports;
|
file |
diff |
annotate
|
| Thu, 10 Dec 2020 16:35:56 +0100 |
wenzelm |
clarified signature: more specific types;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2020 21:49:39 +0100 |
wenzelm |
read theory with PIDE markup from session database;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2020 19:45:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 06 Dec 2020 13:03:26 +0100 |
wenzelm |
silently ignore markup that starts out as singularity, e.g. <language/> from empty ML file;
|
file |
diff |
annotate
|
| Sat, 05 Dec 2020 19:09:39 +0100 |
wenzelm |
proper span position for blobs in batch-build (but: practically irrelevant);
|
file |
diff |
annotate
|
| Sat, 05 Dec 2020 18:14:55 +0100 |
wenzelm |
proper treatment of singleton Position.Offset within blob (amending cb9d5af781b4);
|
file |
diff |
annotate
|
| Sat, 05 Dec 2020 14:36:41 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 05 Dec 2020 12:43:21 +0100 |
wenzelm |
clarified signature, notably access to blob files;
|
file |
diff |
annotate
|
| Sat, 05 Dec 2020 12:14:40 +0100 |
wenzelm |
support for PIDE markup for auxiliary files ("blobs");
|
file |
diff |
annotate
|
| Wed, 02 Dec 2020 15:01:37 +0100 |
wenzelm |
clarified signature --- more explicit types;
|
file |
diff |
annotate
|
| Sun, 29 Nov 2020 16:45:29 +0100 |
wenzelm |
restrict report redirection to current node;
|
file |
diff |
annotate
|
| Sun, 29 Nov 2020 16:11:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 29 Nov 2020 15:41:36 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 29 Nov 2020 15:33:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 29 Nov 2020 14:57:15 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 28 Nov 2020 23:28:56 +0100 |
wenzelm |
clarified parsing vs. semantic errors;
|
file |
diff |
annotate
|
| Sat, 28 Nov 2020 15:53:46 +0100 |
wenzelm |
tuned signature --- more explicit types;
|
file |
diff |
annotate
|
| Fri, 27 Nov 2020 23:47:06 +0100 |
wenzelm |
more flexible syntax for theory load commands via Isabelle/Scala;
|
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, 27 Nov 2020 16:44:36 +0100 |
wenzelm |
more explicit types;
|
file |
diff |
annotate
|
| Fri, 27 Nov 2020 16:40:31 +0100 |
wenzelm |
unused (see 7634d33c1a79);
|
file |
diff |
annotate
|
| Fri, 27 Nov 2020 14:00:54 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 15:59:09 +0100 |
wenzelm |
clarified signature: initial markup is_empty, not init_markup;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 16:14:16 +0100 |
wenzelm |
more complete report positions, notably for command 'back' (amending eca176f773e0);
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 15:24:55 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 13:22:34 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 13:12:31 +0100 |
wenzelm |
removed pointless case: messages should always carry proper position;
|
file |
diff |
annotate
|
| Mon, 23 Nov 2020 15:14:58 +0100 |
wenzelm |
support for PIDE markup in batch build (inactive due to pide_reports=false);
|
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, 16 Sep 2019 19:35:08 +0200 |
wenzelm |
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
|
file |
diff |
annotate
|
| Mon, 02 Sep 2019 11:46:27 +0200 |
wenzelm |
clarified signature: prefer operations without position;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 21:12:29 +0100 |
wenzelm |
document markers are formal comments, and may thus occur anywhere in the command-span;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 00:21:34 +0100 |
wenzelm |
added semantic document markers;
|
file |
diff |
annotate
|
| Fri, 11 Jan 2019 22:34:28 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Sat, 18 Aug 2018 12:41:05 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2018 21:11:24 +0200 |
wenzelm |
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2018 21:06:09 +0200 |
wenzelm |
tuned signature;
|
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
|
| Thu, 31 May 2018 22:10:06 +0200 |
wenzelm |
clarified: consolidated result is last command;
|
file |
diff |
annotate
|
| Tue, 29 May 2018 22:25:59 +0200 |
wenzelm |
more node status information;
|
file |
diff |
annotate
|
| Mon, 28 May 2018 17:40:34 +0200 |
wenzelm |
clarified signature: Known.theories retains Document.Node.Entry (with header);
|
file |
diff |
annotate
|
| Tue, 08 May 2018 11:47:41 +0200 |
wenzelm |
more robust: self-export only;
|
file |
diff |
annotate
|
| Mon, 07 May 2018 17:11:01 +0200 |
wenzelm |
store exports within PIDE command state;
|
file |
diff |
annotate
|
| Sun, 11 Mar 2018 20:56:42 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 11 Mar 2018 20:47:17 +0100 |
wenzelm |
update XML cache for slightly modified messages;
|
file |
diff |
annotate
|
| Sun, 11 Mar 2018 20:31:25 +0100 |
wenzelm |
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 11:27:52 +0100 |
wenzelm |
discontinued old form of marginal comments;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2017 19:29:24 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 05 Oct 2017 17:37:47 +0200 |
wenzelm |
completion supports theory header imports;
|
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
|
| Thu, 20 Apr 2017 11:38:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Apr 2017 12:20:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 03 Apr 2017 16:36:45 +0200 |
wenzelm |
provide session qualifier via resources;
|
file |
diff |
annotate
|
| Sat, 01 Apr 2017 15:35:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2017 20:43:26 +0100 |
wenzelm |
support to encode/decode command state;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2017 20:37:48 +0100 |
wenzelm |
more uniform node_header (non-strict);
|
file |
diff |
annotate
|
| Sat, 07 Jan 2017 20:01:05 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2017 19:36:40 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2017 16:16:18 +0100 |
wenzelm |
suppress empty results;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2016 19:09:10 +0100 |
wenzelm |
more uniform path syntax, as in ML (see 5a7c919a4ada);
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 18:45:34 +0200 |
wenzelm |
tuned signature -- prover-independence is presently theoretical;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 11:31:13 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 00:02:30 +0100 |
wenzelm |
symbolic syntax "\<comment> text";
|
file |
diff |
annotate
|
| Sat, 19 Sep 2015 21:07:37 +0200 |
wenzelm |
straight-forward refresh, without special preconditions;
|
file |
diff |
annotate
|
| Wed, 12 Aug 2015 13:53:51 +0200 |
wenzelm |
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 00:01:10 +0200 |
wenzelm |
misc tuning, based on warnings by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 21:21:40 +0200 |
wenzelm |
more general notion of command span: command keyword not necessarily at start;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 15:21:41 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 13:32:31 +0100 |
wenzelm |
avoid duplicate header errors, more precise positions;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 11:07:56 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 22:15:08 +0100 |
wenzelm |
more markup, which helps to create missing imports;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 21:57:10 +0100 |
wenzelm |
proper command id for inlined errors, which is important for Command.State.accumulate;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 20:35:47 +0100 |
wenzelm |
clarified span position;
|
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
|
| Sun, 15 Mar 2015 12:42:30 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 14 Mar 2015 21:16:29 +0100 |
wenzelm |
value-oriented user error, for well-defined Thy_Syntax.chop_common;
|
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
|
| Thu, 12 Mar 2015 20:34:08 +0100 |
wenzelm |
clarified command content;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2014 23:45:03 +0100 |
wenzelm |
explicit message channel for "legacy", which is nonetheless a variant of "warning";
|
file |
diff |
annotate
|
| Mon, 01 Dec 2014 14:24:05 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:46:20 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:31:24 +0200 |
wenzelm |
clarified Position.Identified: do not require range from prover, default to command position;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 14:15:58 +0200 |
wenzelm |
maintain Command_Range position as in ML;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 00:08:32 +0200 |
wenzelm |
separate module Command_Span: mostly syntactic representation;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 22:59:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 22:43:26 +0200 |
wenzelm |
tuned output, in accordance to transaction name in ML;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 22:29:48 +0200 |
wenzelm |
more explicit type Span in Scala, according to ML version;
|
file |
diff |
annotate
|
| Sat, 02 Aug 2014 16:35:59 +0200 |
wenzelm |
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
|
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
|
| Tue, 29 Apr 2014 13:32:13 +0200 |
wenzelm |
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 13:34:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 13:07:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 14:36:29 +0200 |
wenzelm |
ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL;
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 10:44:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 22:24:00 +0200 |
wenzelm |
expose more bad cases;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 22:01:08 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 20:03:00 +0200 |
wenzelm |
simplified Text.Chunk -- eliminated ooddities;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 19:17:28 +0200 |
wenzelm |
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 16:07:02 +0200 |
wenzelm |
avoid data redundancy;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 15:12:54 +0200 |
wenzelm |
tuned signature -- moved Command.Chunk to Text.Chunk;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 12:31:17 +0200 |
wenzelm |
more uniform Command.Chunk operations;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 12:19:33 +0200 |
wenzelm |
more explicit Command.Chunk types, less ooddities;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 21:55:48 +0200 |
wenzelm |
more direct warning within persistent Protocol.Status;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 20:22:12 +0200 |
wenzelm |
more explicit iterator terminology, in accordance to Scala 2.8 library;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 12:26:11 +0200 |
wenzelm |
persistent protocol_status, to improve performance of node_status a little;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 15:05:24 +0200 |
wenzelm |
store blob content within document node: aux. files that were once open are made persistent;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 12:11:32 +0100 |
wenzelm |
more frugal merge of markup trees: filter wrt. subsequent query;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 10:43:43 +0100 |
wenzelm |
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 19:42:16 +0100 |
wenzelm |
clarified valid_id: always standardize towards static command.id;
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:54:12 +0100 |
wenzelm |
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 15:58:47 +0100 |
wenzelm |
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 14:51:14 +0100 |
wenzelm |
reparse only for actually changed blobs;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 20:56:55 +0100 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 15:22:06 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 15:12:50 +0100 |
wenzelm |
more general / abstract Command.Markups, with separate index for status elements;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 13:36:40 +0100 |
wenzelm |
tuned signature -- avoid obscure default arguments;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 16:56:51 +0100 |
wenzelm |
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 14:36:17 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 14:05:08 +0100 |
wenzelm |
more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 11:05:48 +0100 |
wenzelm |
more accurate eq_content;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 10:50:49 +0100 |
wenzelm |
clarified message_positions: cover alt_id as well;
|
file |
diff |
annotate
|
| Tue, 11 Feb 2014 21:58:31 +0100 |
wenzelm |
maintain multiple command chunks and markup trees: for main chunk and loaded files;
|
file |
diff |
annotate
|
| Tue, 11 Feb 2014 17:44:29 +0100 |
wenzelm |
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
|
file |
diff |
annotate
|
| Tue, 11 Feb 2014 15:55:05 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 11 Feb 2014 15:05:13 +0100 |
wenzelm |
report (but ignore) markup within auxiliary files;
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 15:53:59 +0100 |
wenzelm |
ranges of thy_load commands count as visible within perspective;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 22:12:54 +0100 |
wenzelm |
more explicit indication of missing files;
|
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:39:12 +0100 |
wenzelm |
proper Thy_Load.append of auxiliary file names;
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 23:26:15 +0100 |
wenzelm |
inline blobs into command, via SHA1 digest;
|
file |
diff |
annotate
|
| Sun, 17 Nov 2013 17:22:55 +0100 |
wenzelm |
explicit indication of thy_load commands;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 10:41:17 +0200 |
wenzelm |
retain original messages properties, e.g. for retrieval via Command.Results;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 14:26:09 +0200 |
wenzelm |
maintain overlays within node perspective;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 12:39:45 +0200 |
wenzelm |
full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 22:58:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 22:09:16 +0200 |
wenzelm |
tuned signature -- eliminated pointless type synonym;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 16:01:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 15:38:03 +0200 |
wenzelm |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
file |
diff |
annotate
|
| Thu, 04 Jul 2013 23:51:47 +0200 |
wenzelm |
separate exec_id assignment for Command.print states, without affecting result of eval;
|
file |
diff |
annotate
|
| Thu, 04 Jul 2013 12:02:11 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 16:19:57 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 15:11:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 19:39:31 +0100 |
wenzelm |
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 16:10:46 +0100 |
wenzelm |
structural equality for Command.Results;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2013 13:09:34 +0100 |
wenzelm |
clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 23:04:35 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 12:16:08 +0100 |
wenzelm |
tuned implementation according to Library.insert/merge in ML;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 12:09:08 +0100 |
wenzelm |
more formal class Command.Results;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:29:23 +0100 |
wenzelm |
more careful handling of Dialog_Result, with active area and color feedback;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 13:52:18 +0100 |
wenzelm |
identify dialogs via official serial and maintain as result message;
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 23:36:07 +0100 |
wenzelm |
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 13:21:02 +0100 |
wenzelm |
more abstract Sendback operations, with explicit id/exec_id properties;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 20:36:52 +0100 |
wenzelm |
always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 15:25:49 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 19:34:31 +0200 |
wenzelm |
operations to turn markup into XML;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 19:23:04 +0200 |
wenzelm |
accumulate under exec_id as well;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 19:16:48 +0200 |
wenzelm |
more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 16:50:44 +0200 |
wenzelm |
more realistic sendback: pick exec_id from message position and text from buffer;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 11:09:53 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 19 Sep 2012 17:07:25 +0200 |
wenzelm |
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 17:20:40 +0200 |
wenzelm |
more explicit message markup and rendering;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 14:51:12 +0200 |
wenzelm |
some actual rich text markup via XML.content_markup;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 13:18:45 +0200 |
wenzelm |
some support for inital command markup;
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 20:49:54 +0200 |
wenzelm |
refined output panel: more value-oriented approach to update and caret focus;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2012 14:35:04 +0200 |
wenzelm |
more markup for failed goal forks, reusing "bad";
|
file |
diff |
annotate
|
| Fri, 24 Aug 2012 19:35:44 +0200 |
wenzelm |
more precise counting of line/column;
|
file |
diff |
annotate
|
| Fri, 10 Aug 2012 13:33:07 +0200 |
wenzelm |
clarified undefined, unparsed, unfinished command spans;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2012 17:13:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 22:25:17 +0200 |
wenzelm |
more structural parsing for minor modes;
|
file |
diff |
annotate
|
| Mon, 30 Jul 2012 13:42:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 21:17:59 +0200 |
wenzelm |
include trailing comments in proper_command range;
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 14:59:31 +0100 |
wenzelm |
clarified command span classification: strict Command.is_command, permissive Command.name;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 21:17:37 +0100 |
wenzelm |
clarified command state -- markup within proper_range, excluding trailing whitespace;
|
file |
diff |
annotate
|
| Sun, 04 Mar 2012 19:03:28 +0100 |
wenzelm |
added Command.proper_range (still unused);
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 17:13:25 +0100 |
wenzelm |
prefer final ADTs -- prevent ooddities;
|
file |
diff |
annotate
|
| Mon, 09 Jan 2012 23:08:33 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2012 12:39:46 +0100 |
wenzelm |
accumulate status as regular markup for command range;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 14:29:14 +0100 |
wenzelm |
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
|
file |
diff |
annotate
|
| Tue, 29 Nov 2011 20:18:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Sat, 26 Nov 2011 17:10:03 +0100 |
wenzelm |
sharing of token source with span source;
|
file |
diff |
annotate
|
| Fri, 11 Nov 2011 14:24:38 +0100 |
wenzelm |
prefer statically typed Text.Markup;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2011 23:04:03 +0200 |
wenzelm |
Document.Node.Name convenience;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 13:34:45 +0200 |
wenzelm |
more abstract Document.Node.Name;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 15:41:22 +0200 |
wenzelm |
maintain name of *the* enclosing node as part of command -- avoid full document traversal;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 11:41:48 +0200 |
wenzelm |
slightly more abstract Command.Perspective;
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 12:20:12 +0200 |
wenzelm |
propagate editor perspective through document model;
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 21:42:02 +0200 |
wenzelm |
some support for editor perspective;
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 12:56:51 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2011 22:25:33 +0200 |
wenzelm |
Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
|
file |
diff |
annotate
|
| Thu, 23 Jun 2011 14:52:32 +0200 |
wenzelm |
explicit import java.lang.System to prevent odd scope problems;
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 22:40:45 +0100 |
wenzelm |
avoid spam;
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 15:00:40 +0100 |
wenzelm |
some support for nested source structure, based on section headings;
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 22:39:17 +0200 |
wenzelm |
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 17:10:44 +0200 |
wenzelm |
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 16:51:28 +0200 |
wenzelm |
Command.State.accumulate: check actual source range;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 16:40:30 +0200 |
wenzelm |
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 23:28:21 +0200 |
wenzelm |
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 20:11:21 +0200 |
wenzelm |
Command.newlines: account for physical newlines;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 13:01:32 +0200 |
wenzelm |
Command.results: ordered by serial number;
|
file |
diff |
annotate
|