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