| Tue, 17 Nov 1998 14:09:00 +0100 | wenzelm | space; | file | diff | annotate |
| Mon, 16 Nov 1998 10:41:27 +0100 | wenzelm | Scan.read; | file | diff | annotate |
| Fri, 31 Jul 1998 11:33:30 +0200 | wenzelm | size / length: printable length; | file | diff | annotate |
| Thu, 02 Jul 1998 17:26:47 +0200 | wenzelm | Symbol.beginning; | file | diff | annotate |
| Mon, 25 May 1998 21:13:20 +0200 | wenzelm | added recover, source; | file | diff | annotate |
| Mon, 18 May 1998 17:57:47 +0200 | wenzelm | Symbol.stopper; | file | diff | annotate |
| Wed, 13 May 1998 12:21:45 +0200 | wenzelm | adapted to new Scan.fail_with / Scan.!!; | file | diff | annotate |
| Thu, 07 May 1998 18:05:08 +0200 | wenzelm | added 'space'; | file | diff | annotate |
| Tue, 10 Mar 1998 14:27:44 +0100 | wenzelm | adhoc fix of is_blank; | file | diff | annotate |
| Mon, 09 Mar 1998 16:05:34 +0100 | wenzelm | replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML; | file | diff | annotate |