Sat, 13 Nov 2010 19:27:41 +0100 treat Unicode "replacement character" (i.e. decoding error) is malformed;
wenzelm [Sat, 13 Nov 2010 19:27:41 +0100] rev 40524
treat Unicode "replacement character" (i.e. decoding error) is malformed;
Sat, 13 Nov 2010 19:21:53 +0100 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm [Sat, 13 Nov 2010 19:21:53 +0100] rev 40523
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing; refined treatment of malformed surrogates (Scala);
Sat, 13 Nov 2010 16:46:00 +0100 tuned;
wenzelm [Sat, 13 Nov 2010 16:46:00 +0100] rev 40522
tuned;
Sat, 13 Nov 2010 12:32:21 +0100 back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
wenzelm [Sat, 13 Nov 2010 12:32:21 +0100] rev 40521
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip