src/Pure/Isar/token.scala
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;
Sat, 30 Oct 2010 15:26:40 +0200 wenzelm support for floating-point tokens in outer syntax (coinciding with inner syntax version);
Thu, 12 Aug 2010 17:55:23 +0200 wenzelm more basic notion of unparsed input;
Mon, 17 May 2010 14:23:54 +0200 wenzelm renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
less more (0) tip