src/Pure/Thy/thy_syntax.scala
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;
Fri, 29 Sep 2017 22:41:19 +0200 wenzelm more accurate node_syntax: avoid overall_syntax for PIDE edits;
Fri, 29 Sep 2017 22:12:32 +0200 wenzelm tuned signature;
Fri, 29 Sep 2017 20:49:42 +0200 wenzelm more informative loaded_theories: dependencies and syntax;
Mon, 03 Apr 2017 17:00:36 +0200 wenzelm tuned signature;
Mon, 03 Apr 2017 12:41:06 +0200 wenzelm tuned signature;
Sat, 01 Apr 2017 15:35:32 +0200 wenzelm tuned signature;
Wed, 01 Mar 2017 15:16:06 +0100 wenzelm improved performance of remove, e.g. relevant for Theories_Dockable.purge;
Mon, 09 Jan 2017 20:26:59 +0100 wenzelm tuned signature;
Sat, 07 Jan 2017 15:25:01 +0100 wenzelm obsolete;
Thu, 05 Jan 2017 12:23:25 +0100 wenzelm misc tuning and clarification;
Wed, 14 Sep 2016 12:51:40 +0200 wenzelm tuned;
Tue, 02 Aug 2016 18:45:34 +0200 wenzelm tuned signature -- prover-independence is presently theoretical;
Tue, 02 Aug 2016 17:35:18 +0200 wenzelm support 'abbrevs' within theory header;
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Fri, 24 Apr 2015 19:08:43 +0200 wenzelm tuned;
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;
Sun, 15 Mar 2015 20:35:47 +0100 wenzelm clarified span position;
Sun, 15 Mar 2015 19:48:49 +0100 wenzelm tuned;
Sun, 15 Mar 2015 19:39:31 +0100 wenzelm tuned;
Sun, 15 Mar 2015 19:21:15 +0100 wenzelm hybrid use of command blobs: inlined errors and auxiliary files;
Sun, 15 Mar 2015 12:42:30 +0100 wenzelm tuned;
Sat, 14 Mar 2015 19:51:36 +0100 wenzelm clarified positions of theory imports;
Fri, 13 Mar 2015 12:58:49 +0100 wenzelm simplified Command.resolve_files in ML, using blobs_index from Scala;
Thu, 12 Mar 2015 20:34:08 +0100 wenzelm clarified command content;
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);
Thu, 08 Jan 2015 20:56:39 +0100 wenzelm tuned;
Wed, 03 Dec 2014 22:34:28 +0100 wenzelm node-specific keywords, with session base syntax as default;
Tue, 02 Dec 2014 14:16:56 +0100 wenzelm node-specific syntax, with base_syntax as default;
Tue, 12 Aug 2014 00:17:02 +0200 wenzelm tuned signature;
Tue, 12 Aug 2014 00:08:32 +0200 wenzelm separate module Command_Span: mostly syntactic representation;
Mon, 11 Aug 2014 22:59:38 +0200 wenzelm tuned signature;
Mon, 11 Aug 2014 22:43:26 +0200 wenzelm tuned output, in accordance to transaction name in ML;
Mon, 11 Aug 2014 22:29:48 +0200 wenzelm more explicit type Span in Scala, according to ML version;
Mon, 11 Aug 2014 20:46:56 +0200 wenzelm clarified modules;
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);
Wed, 23 Jul 2014 21:01:28 +0200 wenzelm more frugal edits;
Tue, 08 Apr 2014 20:03:00 +0200 wenzelm simplified Text.Chunk -- eliminated ooddities;
Thu, 03 Apr 2014 21:08:00 +0200 wenzelm clarified Version.syntax -- avoid guessing initial situation;
Thu, 03 Apr 2014 20:53:35 +0200 wenzelm more abstract Prover.Syntax, as proposed by Carst Tankink;
Wed, 02 Apr 2014 20:41:44 +0200 wenzelm tuned signature -- more explicit iterator terminology;
Wed, 02 Apr 2014 20:22:12 +0200 wenzelm more explicit iterator terminology, in accordance to Scala 2.8 library;
Mon, 31 Mar 2014 15:28:14 +0200 wenzelm tuned signature -- more static typing;
Mon, 31 Mar 2014 15:05:24 +0200 wenzelm store blob content within document node: aux. files that were once open are made persistent;
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);
Sat, 29 Mar 2014 10:17:09 +0100 wenzelm tuned signature;
Sat, 29 Mar 2014 09:34:51 +0100 wenzelm tuned signature;
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
Thu, 27 Feb 2014 14:51:14 +0100 wenzelm reparse only for actually changed blobs;
Thu, 27 Feb 2014 14:07:04 +0100 wenzelm more formal Document.Blobs;
Thu, 27 Feb 2014 10:58:43 +0100 wenzelm tuned;
Wed, 12 Feb 2014 11:28:17 +0100 wenzelm maintain blob edits within history, which is important for Snapshot.convert/revert;
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);
Sat, 25 Jan 2014 15:29:40 +0100 wenzelm propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
Wed, 22 Jan 2014 21:33:50 +0100 wenzelm clarified approximative syntax of thy_load commands: first name after command keyword, after cleaning wrt. tags and cmts;
Fri, 22 Nov 2013 21:13:44 +0100 wenzelm clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
Tue, 19 Nov 2013 22:12:54 +0100 wenzelm more explicit indication of missing files;
Tue, 19 Nov 2013 20:53:43 +0100 wenzelm clarified Document.Blobs environment vs. actual edits of auxiliary files;
Tue, 19 Nov 2013 19:33:27 +0100 wenzelm maintain blobs within document state: digest + text in ML, digest-only in Scala;
Tue, 19 Nov 2013 13:54:02 +0100 wenzelm always reparse nodes with thy_load commands, to update inlined files;
less more (0) -100 -60 tip