src/Pure/Thy/thy_scan.ML
2001-10-17 wenzelm 2001-10-17 tuned comments;
1999-05-17 wenzelm 1999-05-17 cleaned comments;
1999-02-03 wenzelm 1999-02-03 tokenize: get exploded args;
1998-11-17 wenzelm 1998-11-17 Symbol.space;
1998-07-02 wenzelm 1998-07-02 Symbol.beginning;
1998-05-18 wenzelm 1998-05-18 Symbol.stopper;
1998-05-13 wenzelm 1998-05-13 adapted to new Scan.fail_with / Scan.!!;
1998-03-09 wenzelm 1998-03-09 adapted to new scanner, baroque chars;
1997-10-10 wenzelm 1997-10-10 scan_longid moved to Syntax/lexicon.ML;
1997-01-29 wenzelm 1997-01-29 removed warning for unprintable chars in strings (functionality will be put into administrative script);
1996-12-13 wenzelm 1996-12-13 added warning for unprintable chars in strings;
1996-12-09 wenzelm 1996-12-09 removed escaping of 8bit chars;
1996-11-18 wenzelm 1996-11-18 improved string scanner: converts 8 bit chars to escape sequences;
1996-11-01 paulson 1996-11-01 Changes tabs found in .thy files to spaces
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1995-03-28 clasohm 1995-03-28 changed string scanner so that newlines ('\n') are allowed and ignored inside strings
1994-11-14 clasohm 1994-11-14 added check for newlines not enclosed by '\' inside strings
1994-05-19 wenzelm 1994-05-19 (replaces Thy/scan.ML) scanner now based on combinators of structure Scanner; improved handling of keywords; now supports long.ids, (* (* nested *) comments *), {| verbatim text |};