src/Pure/General/scan.ML
Mon, 23 Oct 2023 12:08:38 +0200 wenzelm clarified modules;
Tue, 01 Mar 2016 20:51:38 +0100 wenzelm clarified modules;
Sun, 18 Oct 2015 21:30:01 +0200 wenzelm tuned signature;
Sat, 17 Oct 2015 22:31:21 +0200 wenzelm tuned signature;
Mon, 29 Dec 2014 15:38:59 +0100 wenzelm more toplevel pretty printing;
Mon, 01 Dec 2014 13:49:47 +0100 wenzelm tuned;
Sat, 01 Nov 2014 19:33:51 +0100 wenzelm recover via scanner;
Fri, 31 Oct 2014 21:10:11 +0100 wenzelm discontinued obsolete tty and prompt;
Mon, 20 Jan 2014 19:47:31 +0100 wenzelm clarified scan_cartouche_depth, according to Scala version;
Thu, 09 Aug 2012 14:37:43 +0200 wenzelm refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
Sat, 23 Jul 2011 16:37:17 +0200 wenzelm defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
Mon, 30 Aug 2010 15:19:39 +0200 wenzelm tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Thu, 07 Aug 2008 21:13:01 +0200 wenzelm tuned;
Thu, 07 Aug 2008 21:07:55 +0200 wenzelm datatype lexicon: alternative representation using nested Symtab.table;
Thu, 07 Aug 2008 13:44:47 +0200 wenzelm reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;
Mon, 04 Aug 2008 21:24:15 +0200 wenzelm abstract type stopper, may depend on final input;
Mon, 28 Jan 2008 22:27:19 +0100 wenzelm added ::: / @@@ scanner combinators;
Sun, 16 Sep 2007 14:52:29 +0200 wenzelm tuned message;
Sat, 28 Jul 2007 20:40:31 +0200 wenzelm added :|-- (dependent projection);
Tue, 10 Jul 2007 16:45:01 +0200 wenzelm infixr || (more efficient);
Tue, 10 Jul 2007 00:43:51 +0200 wenzelm tuned;
Tue, 10 Jul 2007 00:17:52 +0200 wenzelm nested source: explicit interactive flag for recover avoids duplicate errors;
Mon, 09 Jul 2007 23:12:38 +0200 wenzelm tuned signature;
Fri, 19 Jan 2007 22:08:21 +0100 wenzelm tuned signature of extend_lexicon;
less more (0) -50 -30 tip