| Thu, 04 Mar 2021 21:19:05 +0100 | 
wenzelm | 
clarified signature --- fewer warnings;
 | 
file |
diff |
annotate
 | 
| Thu, 04 Mar 2021 15:41:46 +0100 | 
wenzelm | 
tuned --- fewer warnings;
 | 
file |
diff |
annotate
 | 
| Mon, 01 Mar 2021 23:17:47 +0100 | 
wenzelm | 
tuned --- fewer warnings;
 | 
file |
diff |
annotate
 | 
| Mon, 01 Mar 2021 22:22:12 +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
 | 
| Fri, 27 Mar 2020 22:01:27 +0100 | 
wenzelm | 
misc tuning based on hints by IntelliJ IDEA;
 | 
file |
diff |
annotate
 | 
| Mon, 07 Oct 2019 11:35:43 +0200 | 
wenzelm | 
discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
 | 
file |
diff |
annotate
 | 
| Mon, 02 Sep 2019 11:46:27 +0200 | 
wenzelm | 
clarified signature: prefer operations without position;
 | 
file |
diff |
annotate
 | 
| Wed, 28 Aug 2019 22:59:49 +0200 | 
wenzelm | 
support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
 | 
file |
diff |
annotate
 | 
| Mon, 31 Dec 2018 20:08:32 +0100 | 
wenzelm | 
tuned;
 | 
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:27:13 +0200 | 
wenzelm | 
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
 | 
file |
diff |
annotate
 | 
| Fri, 06 Oct 2017 21:23:21 +0200 | 
wenzelm | 
even more robust syntax (amending 122df1fde073);
 | 
file |
diff |
annotate
 | 
| Fri, 06 Oct 2017 17:13:57 +0200 | 
wenzelm | 
clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;
 | 
file |
diff |
annotate
 | 
| Fri, 29 Sep 2017 22:41:19 +0200 | 
wenzelm | 
more accurate node_syntax: avoid overall_syntax for PIDE edits;
 | 
file |
diff |
annotate
 | 
| Fri, 29 Sep 2017 22:12:32 +0200 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Fri, 29 Sep 2017 20:49:42 +0200 | 
wenzelm | 
more informative loaded_theories: dependencies and syntax;
 | 
file |
diff |
annotate
 | 
| Mon, 03 Apr 2017 17:00:36 +0200 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Mon, 03 Apr 2017 12:41:06 +0200 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Sat, 01 Apr 2017 15:35:32 +0200 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Wed, 01 Mar 2017 15:16:06 +0100 | 
wenzelm | 
improved performance of remove, e.g. relevant for Theories_Dockable.purge;
 | 
file |
diff |
annotate
 | 
| Mon, 09 Jan 2017 20:26:59 +0100 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Sat, 07 Jan 2017 15:25:01 +0100 | 
wenzelm | 
obsolete;
 | 
file |
diff |
annotate
 | 
| Thu, 05 Jan 2017 12:23:25 +0100 | 
wenzelm | 
misc tuning and clarification;
 | 
file |
diff |
annotate
 | 
| Wed, 14 Sep 2016 12:51:40 +0200 | 
wenzelm | 
tuned;
 | 
file |
diff |
annotate
 | 
| Tue, 02 Aug 2016 18:45:34 +0200 | 
wenzelm | 
tuned signature -- prover-independence is presently theoretical;
 | 
file |
diff |
annotate
 | 
| Tue, 02 Aug 2016 17:35:18 +0200 | 
wenzelm | 
support 'abbrevs' within theory header;
 | 
file |
diff |
annotate
 | 
| Sun, 03 May 2015 00:01:10 +0200 | 
wenzelm | 
misc tuning, based on warnings by IntelliJ IDEA;
 | 
file |
diff |
annotate
 | 
| Fri, 24 Apr 2015 19:08:43 +0200 | 
wenzelm | 
tuned;
 | 
file |
diff |
annotate
 | 
| Tue, 24 Mar 2015 23:37:05 +0100 | 
wenzelm | 
proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;
 | 
file |
diff |
annotate
 | 
| Sun, 15 Mar 2015 20:35:47 +0100 | 
wenzelm | 
clarified span position;
 | 
file |
diff |
annotate
 | 
| Sun, 15 Mar 2015 19:48:49 +0100 | 
wenzelm | 
tuned;
 | 
file |
diff |
annotate
 | 
| Sun, 15 Mar 2015 19:39:31 +0100 | 
wenzelm | 
tuned;
 | 
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 19:51:36 +0100 | 
wenzelm | 
clarified positions of theory imports;
 | 
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
 | 
| Thu, 15 Jan 2015 20:36:26 +0100 | 
wenzelm | 
proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
 | 
file |
diff |
annotate
 | 
| Thu, 08 Jan 2015 20:56:39 +0100 | 
wenzelm | 
tuned;
 | 
file |
diff |
annotate
 | 
| Wed, 03 Dec 2014 22:34:28 +0100 | 
wenzelm | 
node-specific keywords, with session base syntax as default;
 | 
file |
diff |
annotate
 | 
| Tue, 02 Dec 2014 14:16:56 +0100 | 
wenzelm | 
node-specific syntax, with base_syntax as default;
 | 
file |
diff |
annotate
 | 
| Tue, 12 Aug 2014 00:17:02 +0200 | 
wenzelm | 
tuned signature;
 | 
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
 | 
| Mon, 11 Aug 2014 20:46:56 +0200 | 
wenzelm | 
clarified modules;
 | 
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 21:01:28 +0200 | 
wenzelm | 
more frugal edits;
 | 
file |
diff |
annotate
 | 
| Tue, 08 Apr 2014 20:03:00 +0200 | 
wenzelm | 
simplified Text.Chunk -- eliminated ooddities;
 | 
file |
diff |
annotate
 | 
| Thu, 03 Apr 2014 21:08:00 +0200 | 
wenzelm | 
clarified Version.syntax -- avoid guessing initial situation;
 | 
file |
diff |
annotate
 | 
| Thu, 03 Apr 2014 20:53:35 +0200 | 
wenzelm | 
more abstract Prover.Syntax, as proposed by Carst Tankink;
 | 
file |
diff |
annotate
 | 
| Wed, 02 Apr 2014 20:41:44 +0200 | 
wenzelm | 
tuned signature -- more explicit iterator terminology;
 | 
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
 | 
| Mon, 31 Mar 2014 15:28:14 +0200 | 
wenzelm | 
tuned signature -- more static typing;
 | 
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
 | 
| Sat, 29 Mar 2014 10:49:32 +0100 | 
wenzelm | 
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
 | 
file |
diff |
annotate
 | 
| Sat, 29 Mar 2014 10:17:09 +0100 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Sat, 29 Mar 2014 09:34:51 +0100 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 |