src/Pure/Isar/outer_syntax.scala
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;
Sat, 04 Nov 2017 18:57:49 +0100 wenzelm tuned signature;
Sat, 04 Nov 2017 17:11:21 +0100 wenzelm clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
Wed, 01 Nov 2017 21:02:16 +0100 wenzelm init only once (see also c0f776b661fa);
Wed, 01 Nov 2017 20:46:23 +0100 wenzelm proper merge (amending fb46c031c841);
Sat, 07 Oct 2017 13:13:46 +0200 wenzelm clarified empty merge;
Fri, 29 Sep 2017 20:49:42 +0200 wenzelm more informative loaded_theories: dependencies and syntax;
Tue, 04 Apr 2017 22:56:28 +0200 wenzelm more explicit types;
Tue, 04 Apr 2017 22:53:01 +0200 wenzelm proper name according to meaning;
Tue, 20 Dec 2016 10:45:20 +0100 wenzelm tuned;
Wed, 14 Sep 2016 12:56:57 +0200 wenzelm maintain abbrevs in canonical reverse order;
Wed, 14 Sep 2016 12:12:44 +0200 wenzelm tuned;
Thu, 04 Aug 2016 11:17:11 +0200 wenzelm clarified modules;
Thu, 04 Aug 2016 10:55:51 +0200 wenzelm clarified modules;
Wed, 03 Aug 2016 11:45:09 +0200 wenzelm include 'begin' and 'end' structure in text folds;
Tue, 02 Aug 2016 21:04:52 +0200 wenzelm implicit keyword completion only for actual words (amending 73939a9b70a3);
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;
Wed, 20 Jul 2016 16:02:00 +0200 wenzelm completion templates for commands involving "begin ... end" blocks;
Wed, 13 Jul 2016 19:36:47 +0200 wenzelm tuned;
Tue, 12 Jul 2016 14:51:39 +0200 wenzelm clarified;
Tue, 12 Jul 2016 14:13:42 +0200 wenzelm clarified;
Tue, 12 Jul 2016 13:26:39 +0200 wenzelm closing 'qed' or '}' is outside of fold;
Mon, 11 Jul 2016 16:36:29 +0200 wenzelm explicit kind "before_command";
Sun, 10 Jul 2016 11:18:35 +0200 wenzelm tuned signature: more uniform Keyword.spec;
Thu, 07 Jul 2016 21:34:56 +0200 wenzelm clarified signature;
Sun, 28 Feb 2016 17:37:20 +0100 wenzelm discontinued old 'header';
Sun, 24 Jan 2016 20:37:40 +0100 wenzelm proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;
Sat, 17 Oct 2015 21:15:10 +0200 wenzelm added 'paragraph', 'subparagraph';
Wed, 08 Jul 2015 15:37:32 +0200 wenzelm clarified text folds: proof ... qed counts as extra block;
Wed, 08 Jul 2015 12:09:44 +0200 wenzelm tuned;
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Mon, 06 Apr 2015 22:11:01 +0200 wenzelm support for 'restricted' modifier: only qualified accesses outside the local scope;
Sat, 04 Apr 2015 21:21:40 +0200 wenzelm more general notion of command span: command keyword not necessarily at start;
Tue, 17 Mar 2015 15:21:41 +0100 wenzelm misc tuning and simplification;
Sun, 15 Mar 2015 19:21:15 +0100 wenzelm hybrid use of command blobs: inlined errors and auxiliary files;
Sun, 15 Mar 2015 12:49:20 +0100 wenzelm more command categories, as in ML;
Thu, 12 Mar 2015 20:34:08 +0100 wenzelm clarified command content;
Thu, 08 Jan 2015 20:56:39 +0100 wenzelm tuned;
Tue, 09 Dec 2014 21:14:11 +0100 wenzelm tuned signature;
Wed, 03 Dec 2014 14:04:38 +0100 wenzelm tuned signature;
Tue, 02 Dec 2014 14:16:56 +0100 wenzelm node-specific syntax, with base_syntax as default;
Mon, 01 Dec 2014 15:21:49 +0100 wenzelm more merge operations;
Fri, 07 Nov 2014 23:35:13 +0100 wenzelm tuned outline;
Wed, 05 Nov 2014 21:59:21 +0100 wenzelm more uniform header_keywords in ML/Scala;
Wed, 05 Nov 2014 17:37:25 +0100 wenzelm clarified representation of type Keywords;
Wed, 05 Nov 2014 16:57:12 +0100 wenzelm explicit type Keyword.Keywords;
Wed, 05 Nov 2014 15:32:11 +0100 wenzelm clarified minor/major lexicon (like ML version);
Sun, 02 Nov 2014 15:27:37 +0100 wenzelm uniform heading commands work in any context, even in theory header;
Fri, 31 Oct 2014 21:48:40 +0100 wenzelm discontinued obsolete control command category;
Tue, 21 Oct 2014 20:44:17 +0200 wenzelm tuned;
Tue, 21 Oct 2014 15:21:44 +0200 wenzelm support for structure matching;
Tue, 21 Oct 2014 13:56:42 +0200 wenzelm tuned rendering;
Tue, 21 Oct 2014 10:53:24 +0200 wenzelm clarified tree root;
Sun, 19 Oct 2014 11:20:03 +0200 wenzelm tuned signature and modules;
Sat, 18 Oct 2014 22:41:36 +0200 wenzelm more folds;
Sat, 18 Oct 2014 20:56:16 +0200 wenzelm clarified Line_Structure wrt. command span;
Sat, 18 Oct 2014 10:32:19 +0200 wenzelm tuned signature;
Thu, 16 Oct 2014 21:24:42 +0200 wenzelm more explicit Line_Nesting;
Thu, 16 Oct 2014 12:24:19 +0200 wenzelm tuned comments;
less more (0) -100 -60 tip