Sat, 13 Nov 2010 21:46:24 +0100 always print state of proof commands (notably "qed" etc.);
wenzelm [Sat, 13 Nov 2010 21:46:24 +0100] rev 40532
always print state of proof commands (notably "qed" etc.);
Sat, 13 Nov 2010 21:01:03 +0100 simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
wenzelm [Sat, 13 Nov 2010 21:01:03 +0100] rev 40531
simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
Sat, 13 Nov 2010 20:49:02 +0100 tuned message;
wenzelm [Sat, 13 Nov 2010 20:49:02 +0100] rev 40530
tuned message;
Sat, 13 Nov 2010 20:20:05 +0100 proper escape in regex;
wenzelm [Sat, 13 Nov 2010 20:20:05 +0100] rev 40529
proper escape in regex;
Sat, 13 Nov 2010 20:13:35 +0100 report malformed symbols;
wenzelm [Sat, 13 Nov 2010 20:13:35 +0100] rev 40528
report malformed symbols;
Sat, 13 Nov 2010 20:06:52 +0100 qualified Symbol_Pos.symbol;
wenzelm [Sat, 13 Nov 2010 20:06:52 +0100] rev 40527
qualified Symbol_Pos.symbol;
Sat, 13 Nov 2010 19:55:45 +0100 total Symbol.source;
wenzelm [Sat, 13 Nov 2010 19:55:45 +0100] rev 40526
total Symbol.source;
Sat, 13 Nov 2010 19:47:23 +0100 eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm [Sat, 13 Nov 2010 19:47:23 +0100] rev 40525
eliminated slightly odd pervasive Symbol_Pos.symbol;
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);
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip