src/Pure/General/symbol_pos.ML
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 ||);
Tue, 12 Jul 2011 14:33:08 +0200 wenzelm more precise Symbol_Pos.quote_string;
Fri, 08 Jul 2011 16:13:34 +0200 wenzelm discontinued special treatment of hard tabulators;
Sat, 30 Apr 2011 18:16:40 +0200 wenzelm more uniform variations of scan_string;
Wed, 29 Dec 2010 21:21:11 +0100 wenzelm more scalable Symbol_Pos.explode;
Sat, 13 Nov 2010 19:47:23 +0100 wenzelm eliminated slightly odd pervasive Symbol_Pos.symbol;
Mon, 17 May 2010 15:02:44 +0200 wenzelm tuned signature;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Thu, 19 Mar 2009 15:22:53 +0100 wenzelm moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
Wed, 18 Mar 2009 21:55:38 +0100 wenzelm de-camelized Symbol_Pos;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Sun, 24 Aug 2008 17:23:42 +0200 wenzelm untabify: silently turn tab into space if column information is unavailable;
Thu, 14 Aug 2008 11:55:05 +0200 wenzelm made SML/NJ happy;
Wed, 13 Aug 2008 20:57:24 +0200 wenzelm added untabify_content;
Sat, 09 Aug 2008 00:09:29 +0200 wenzelm added content;
Thu, 07 Aug 2008 19:21:40 +0200 wenzelm renamed SymbolPos.scan_position to SymbolPos.scan_pos;
Thu, 07 Aug 2008 13:44:36 +0200 wenzelm Symbols with explicit position information.
less more (0) tip