src/Pure/Isar/token.scala
Mon, 20 Mar 2017 20:43:26 +0100 wenzelm support to encode/decode command state;
Sat, 07 Jan 2017 20:01:05 +0100 wenzelm tuned signature;
Sat, 31 Dec 2016 21:00:43 +0100 wenzelm more precise markup;
Mon, 26 Dec 2016 13:21:08 +0100 wenzelm clarified header text;
Mon, 07 Nov 2016 19:09:10 +0100 wenzelm more uniform path syntax, as in ML (see 5a7c919a4ada);
Wed, 13 Jul 2016 19:04:49 +0200 wenzelm clarified indentation: 'begin' is treated like a separate command without indent;
Mon, 11 Jul 2016 20:37:28 +0200 wenzelm indentation of brackets;
Mon, 11 Jul 2016 18:18:24 +0200 wenzelm tunes signature;
Mon, 11 Jul 2016 16:36:29 +0200 wenzelm explicit kind "before_command";
Thu, 07 Jul 2016 21:34:56 +0200 wenzelm clarified signature;
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Fri, 08 Jan 2016 17:17:43 +0100 wenzelm tuned;
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;
Sat, 18 Apr 2015 23:43:30 +0200 wenzelm clarified keywords for quasi-command spans and Sidekick structure;
Thu, 09 Apr 2015 20:42:32 +0200 wenzelm clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
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;
Mon, 16 Mar 2015 13:32:31 +0100 wenzelm avoid duplicate header errors, more precise positions;
Sun, 15 Mar 2015 21:57:10 +0100 wenzelm proper command id for inlined errors, which is important for Command.State.accumulate;
Sun, 15 Mar 2015 20:35:47 +0100 wenzelm clarified span position;
Sun, 15 Mar 2015 14:46:01 +0100 wenzelm more command categories, as in ML;
Sat, 14 Mar 2015 20:08:03 +0100 wenzelm tuned signature;
Sat, 14 Mar 2015 19:51:36 +0100 wenzelm clarified positions of theory imports;
Tue, 10 Mar 2015 20:12:30 +0100 wenzelm more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
Tue, 09 Dec 2014 21:14:11 +0100 wenzelm tuned signature;
Wed, 03 Dec 2014 14:04:38 +0100 wenzelm tuned signature;
Wed, 03 Dec 2014 11:37:51 +0100 wenzelm clarified token kind;
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);
Sat, 01 Nov 2014 15:01:41 +0100 wenzelm command-line terminator ";" is no longer accepted;
Tue, 21 Oct 2014 20:44:17 +0200 wenzelm tuned;
Tue, 21 Oct 2014 20:18:37 +0200 wenzelm proper token kind;
Tue, 20 May 2014 14:25:28 +0200 wenzelm explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;
Mon, 19 May 2014 14:48:50 +0200 wenzelm clarified is_text in accordance to ML version (7e0178c84994), e.g. relevant for 'header' syntax in PIDE front-end;
Fri, 11 Apr 2014 09:36:38 +0200 wenzelm tuned message, to accommodate extra brackets produced by Scala parsers;
Tue, 08 Apr 2014 13:24:08 +0200 wenzelm more precise token positions;
Sun, 16 Feb 2014 15:38:08 +0100 wenzelm support ML antiquotations in Scala;
Sun, 16 Feb 2014 13:18:08 +0100 wenzelm tuned signature -- emphasize line-oriented aspect;
Sat, 15 Feb 2014 18:28:18 +0100 wenzelm more uniform ML keyword markup;
Fri, 14 Feb 2014 21:06:20 +0100 wenzelm lexical syntax for SML (in Scala);
Fri, 14 Feb 2014 16:25:30 +0100 wenzelm tuned signature (in accordance to ML version);
Fri, 14 Feb 2014 15:42:27 +0100 wenzelm tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
Sat, 25 Jan 2014 16:46:39 +0100 wenzelm semicolon is minor keyword (see also 29f1e53f9937);
Sat, 18 Jan 2014 19:31:32 +0100 wenzelm unused;
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
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;
Fri, 10 Aug 2012 13:33:07 +0200 wenzelm clarified undefined, unparsed, unfinished command spans;
Tue, 07 Aug 2012 22:25:17 +0200 wenzelm more structural parsing for minor modes;
Mon, 30 Jul 2012 15:31:00 +0200 wenzelm allow negative int values as well, according to real = int | float;
Mon, 30 Jul 2012 13:42:45 +0200 wenzelm tuned signature;
Fri, 20 Jul 2012 15:48:22 +0200 wenzelm basic support for stand-alone options with external string representation;
Thu, 19 Jul 2012 14:24:40 +0200 wenzelm support Session.Queue with ordering and dependencies;
Wed, 18 Jul 2012 14:07:31 +0200 wenzelm more informative errors;
Mon, 19 Mar 2012 14:59:31 +0100 wenzelm clarified command span classification: strict Command.is_command, permissive Command.name;
Thu, 15 Mar 2012 14:22:54 +0100 wenzelm clarified syntax of prospective keywords;
Thu, 30 Jun 2011 19:24:09 +0200 wenzelm more general theory header parsing;
Sat, 18 Jun 2011 11:45:07 +0200 wenzelm more uniform treatment of "keyword" vs. "operator";
Fri, 17 Jun 2011 00:10:39 +0200 wenzelm recovered markup for non-alphabetic keywords;
less more (0) -60 tip