Sat, 13 Nov 2010 19:55:45 +0100total Symbol.source;
wenzelm [Sat, 13 Nov 2010 19:55:45 +0100] rev 40772
total Symbol.source;

Sat, 13 Nov 2010 19:47:23 +0100eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm [Sat, 13 Nov 2010 19:47:23 +0100] rev 40771
eliminated slightly odd pervasive Symbol_Pos.symbol;

Sat, 13 Nov 2010 19:27:41 +0100treat Unicode "replacement character" (i.e. decoding error) is malformed;
wenzelm [Sat, 13 Nov 2010 19:27:41 +0100] rev 40770
treat Unicode "replacement character" (i.e. decoding error) is malformed;

Sat, 13 Nov 2010 19:21:53 +0100simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm [Sat, 13 Nov 2010 19:21:53 +0100] rev 40769
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 +0100tuned;
wenzelm [Sat, 13 Nov 2010 16:46:00 +0100] rev 40768
tuned;

Sat, 13 Nov 2010 12:32:21 +0100back 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 40767
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;

Sat, 13 Nov 2010 11:41:02 +0100await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
wenzelm [Sat, 13 Nov 2010 11:41:02 +0100] rev 40766
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;

Sat, 13 Nov 2010 00:24:41 +0100updated README;
wenzelm [Sat, 13 Nov 2010 00:24:41 +0100] rev 40765
updated README;

Fri, 12 Nov 2010 21:37:01 +0100defensive defaults for more robust experience for new users;
wenzelm [Fri, 12 Nov 2010 21:37:01 +0100] rev 40764
defensive defaults for more robust experience for new users;

Fri, 12 Nov 2010 17:44:03 +0100merged
wenzelm [Fri, 12 Nov 2010 17:44:03 +0100] rev 40763
merged