src/Pure/Syntax/scan.ML
Thu, 18 Jun 1998 11:20:54 +0200 wenzelm replaced warning by error_msg;
Tue, 26 May 1998 12:29:27 +0200 wenzelm made SML/NJ happy;
Mon, 25 May 1998 21:12:46 +0200 wenzelm added catch: ('a -> 'b) -> 'a -> 'b;
Wed, 20 May 1998 18:57:16 +0200 wenzelm source vs. source';
Mon, 18 May 1998 17:57:16 +0200 wenzelm improved finite scans: more abstract stopper;
Wed, 13 May 1998 19:06:14 +0200 wenzelm added :-- (dependent pair);
Wed, 13 May 1998 12:20:28 +0200 wenzelm added fail_with and adapted !!;
Thu, 07 May 1998 18:34:48 +0200 wenzelm improved source: state-based;
Tue, 24 Mar 1998 16:57:40 +0100 wenzelm added try, single, many;
Mon, 09 Mar 1998 16:12:19 +0100 wenzelm Generic scanners (for potentially infinite input) -- replaces Scanner;
less more (0) tip