src/Pure/General/scan.ML
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-08-07 wenzelm 2008-08-07 tuned;
2008-08-07 wenzelm 2008-08-07 datatype lexicon: alternative representation using nested Symtab.table;
2008-08-07 wenzelm 2008-08-07 reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;
2008-08-04 wenzelm 2008-08-04 abstract type stopper, may depend on final input;
2008-01-28 wenzelm 2008-01-28 added ::: / @@@ scanner combinators;
2007-09-16 wenzelm 2007-09-16 tuned message;
2007-07-28 wenzelm 2007-07-28 added :|-- (dependent projection); tuned;
2007-07-10 wenzelm 2007-07-10 infixr || (more efficient); tuned signature; removed unused trace'; moved source cascading from scan.ML to source.ML; tuned;
2007-07-10 wenzelm 2007-07-10 tuned;
2007-07-10 wenzelm 2007-07-10 nested source: explicit interactive flag for recover avoids duplicate errors;
2007-07-09 wenzelm 2007-07-09 tuned signature; nested source: error msg passed to recover;
2007-01-19 wenzelm 2007-01-19 tuned signature of extend_lexicon;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-04-26 wenzelm 2006-04-26 tuned;
2006-03-21 wenzelm 2006-03-21 added ~$$ (negative literal); combinators: avoid code duplication; tuned extend_lexicon;
2006-03-18 wenzelm 2006-03-18 made $$ and "this" monomorphic (string);
2006-01-14 wenzelm 2006-01-14 Output.error_msg;
2005-07-13 wenzelm 2005-07-13 tuned;
2005-06-21 wenzelm 2005-06-21 tuned;
2005-05-18 wenzelm 2005-05-18 tuned;
2005-04-07 wenzelm 2005-04-07 added some, peek, trace'; tuned;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-16 wenzelm 2004-06-16 tuned;
2004-06-12 wenzelm 2004-06-12 added trace (inefficient for very long input);
2004-06-09 wenzelm 2004-06-09 added this_string;
2004-05-29 wenzelm 2004-05-29 Output.error;
2004-05-10 wenzelm 2004-05-10 added Scan.list;
2004-04-29 wenzelm 2004-04-29 added is_literal;
2004-04-26 wenzelm 2004-04-26 tuned presentation;
2003-07-11 berghofe 2003-07-11 Restored old (tail recursive!) version of repeat.
2003-06-28 kleing 2003-06-28 integrated optimizations by Sebastian Skalberg, produces less garbage, is faster and clearer
2003-01-29 berghofe 2003-01-29 Some tuning: - finite now uses rev_append (tail recursive!) to append stopper, because @ needs to much stack space for large strings - repeat is now tail recursive
2001-08-31 berghofe 2001-08-31 Tuned function extend_lexicon.
2000-12-29 wenzelm 2000-12-29 recover: result;
2000-06-25 wenzelm 2000-06-25 added state: 'a * 'b -> 'a * ('a * 'b);
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-01 wenzelm 2000-04-01 recover: observe stopper;
1999-07-16 wenzelm 1999-07-16 tuned dest_lexicon;
1999-05-12 wenzelm 1999-05-12 rearranged order of modules;
1999-01-13 wenzelm 1999-01-13 fixed titles;
1999-01-13 wenzelm 1999-01-13 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;