src/Pure/Thy/thy_scan.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 |};