src/Pure/General/symbol_pos.ML
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Thu, 23 Aug 2012 17:46:03 +0200 wenzelm tuned messages: end-of-input rarely means physical end-of-file from the past;
Sat, 11 Aug 2012 17:43:00 +0200 wenzelm tuned markup;
Fri, 10 Aug 2012 22:25:45 +0200 wenzelm proper error prefixes;
Thu, 09 Aug 2012 14:37:43 +0200 wenzelm refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
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