src/Pure/General/source.ML
Mon, 04 Aug 2008 21:24:17 +0200 wenzelm abstract type Scan.stopper;
Sun, 06 Jan 2008 15:57:52 +0100 wenzelm removed unused of_stream;
Fri, 07 Dec 2007 17:40:05 +0100 wenzelm output_prompt: CRITICAL;
Sun, 12 Aug 2007 18:53:04 +0200 wenzelm stream source: non-critical, assuming exclusive ownership;
Sun, 29 Jul 2007 22:41:55 +0200 wenzelm added of_list_limited (with limit argument);
Sun, 29 Jul 2007 17:28:55 +0200 wenzelm NAMED_CRITICAL;
Mon, 23 Jul 2007 16:45:01 +0200 wenzelm marked some CRITICAL sections;
Thu, 19 Jul 2007 23:49:04 +0200 wenzelm added of_string_limited (more efficient for partial scans);
Tue, 10 Jul 2007 16:45:03 +0200 wenzelm moved source cascading from scan.ML to source.ML;
Tue, 10 Jul 2007 00:17:52 +0200 wenzelm nested source: explicit interactive flag for recover avoids duplicate errors;
Mon, 09 Jul 2007 23:12:40 +0200 wenzelm nested source: error msg passed to recover;
Mon, 09 Jul 2007 11:44:22 +0200 wenzelm prompt: plain string, not output;
Thu, 31 May 2007 01:25:24 +0200 wenzelm TextIO.inputLine: use present SML B library version;
Wed, 27 Sep 2006 21:33:13 +0200 wenzelm removed obsolete of_instream_slurp -- now already included in tty;
Wed, 27 Sep 2006 21:13:13 +0200 wenzelm of_stream/tty: slurp input eagerly;
Wed, 20 Sep 2006 13:02:30 +0200 aspinall Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.
Thu, 27 Apr 2006 15:06:42 +0200 wenzelm renamed Source.mapfilter to Source.map_filter;
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Mon, 10 May 2004 19:26:11 +0200 wenzelm Source.of_list: no buffer limitation (now pointless due to tail-recursive Scan.repeat);
Fri, 29 Dec 2000 19:44:13 +0100 wenzelm recover: result;
Sun, 25 Jun 2000 23:46:52 +0200 wenzelm added exhausted: ('a, 'b) source -> ('a, 'a list) source;
Fri, 05 May 2000 22:02:46 +0200 wenzelm GPLed;
Thu, 13 Jan 2000 15:29:52 +0100 wenzelm tuned comment;
Fri, 21 May 1999 11:37:36 +0200 wenzelm added default_prompt;
Wed, 12 May 1999 16:52:28 +0200 wenzelm rearranged order of modules;
Wed, 03 Feb 1999 16:31:07 +0100 wenzelm of_file: Path.T, Position.T;
Wed, 13 Jan 1999 15:18:02 +0100 wenzelm fixed titles;
Wed, 13 Jan 1999 12:44:33 +0100 wenzelm files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
less more (0) tip