| Sat, 23 Jul 2011 16:37:17 +0200 |
wenzelm |
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
|
file |
diff |
annotate
|
| Tue, 12 Jul 2011 14:33:08 +0200 |
wenzelm |
more precise Symbol_Pos.quote_string;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 16:13:34 +0200 |
wenzelm |
discontinued special treatment of hard tabulators;
|
file |
diff |
annotate
|
| Sat, 30 Apr 2011 18:16:40 +0200 |
wenzelm |
more uniform variations of scan_string;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 21:21:11 +0100 |
wenzelm |
more scalable Symbol_Pos.explode;
|
file |
diff |
annotate
|
| Sat, 13 Nov 2010 19:47:23 +0100 |
wenzelm |
eliminated slightly odd pervasive Symbol_Pos.symbol;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:02:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 15:22:53 +0100 |
wenzelm |
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
|
file |
diff |
annotate
|
| Wed, 18 Mar 2009 21:55:38 +0100 |
wenzelm |
de-camelized Symbol_Pos;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Sun, 24 Aug 2008 17:23:42 +0200 |
wenzelm |
untabify: silently turn tab into space if column information is unavailable;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 11:55:05 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2008 20:57:24 +0200 |
wenzelm |
added untabify_content;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 00:09:29 +0200 |
wenzelm |
added content;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2008 19:21:40 +0200 |
wenzelm |
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2008 13:44:36 +0200 |
wenzelm |
Symbols with explicit position information.
|
file |
diff |
annotate
|