2011-07-23 ago defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2010-11-20 ago renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-08-30 ago tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-09-30 ago eliminated redundant bindings;
2009-01-21 ago removed Ids;
2008-08-07 ago tuned;
2008-08-07 ago datatype lexicon: alternative representation using nested Symtab.table;
2008-08-07 ago reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;
2008-08-04 ago abstract type stopper, may depend on final input;
2008-01-28 ago added ::: / @@@ scanner combinators;
2007-09-16 ago tuned message;
2007-07-28 ago added :|-- (dependent projection);
2007-07-10 ago infixr || (more efficient);
2007-07-10 ago tuned;
2007-07-10 ago nested source: explicit interactive flag for recover avoids duplicate errors;
2007-07-09 ago tuned signature;
2007-01-19 ago tuned signature of extend_lexicon;
2006-12-15 ago avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-04-26 ago tuned;
2006-03-21 ago added ~$$ (negative literal);
2006-03-18 ago made $$ and "this" monomorphic (string);
2006-01-14 ago Output.error_msg;
2005-07-13 ago tuned;
2005-06-21 ago tuned;
2005-05-18 ago tuned;
2005-04-07 ago added some, peek, trace'; tuned;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-16 ago tuned;
2004-06-12 ago added trace (inefficient for very long input);
2004-06-09 ago added this_string;
2004-05-29 ago Output.error;
2004-05-10 ago added Scan.list;
2004-04-29 ago added is_literal;
2004-04-26 ago tuned presentation;
2003-07-11 ago Restored old (tail recursive!) version of repeat.
2003-06-28 ago integrated optimizations by Sebastian Skalberg,
2003-01-29 ago Some tuning:
2001-08-31 ago Tuned function extend_lexicon.
2000-12-29 ago recover: result;
2000-06-25 ago added state: 'a * 'b -> 'a * ('a * 'b);
2000-05-05 ago GPLed;
2000-04-01 ago recover: observe stopper;
1999-07-16 ago tuned dest_lexicon;
1999-05-12 ago rearranged order of modules;
1999-01-13 ago fixed titles;
1999-01-13 ago files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;