Fri, 17 Sep 2010 22:42:07 +0200 ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
wenzelm [Fri, 17 Sep 2010 22:42:07 +0200] rev 39514
ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
Fri, 17 Sep 2010 22:17:57 +0200 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm [Fri, 17 Sep 2010 22:17:57 +0200] rev 39513
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
Fri, 17 Sep 2010 21:50:44 +0200 Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm [Fri, 17 Sep 2010 21:50:44 +0200] rev 39512
Isabelle_Markup.overview_color: indicate error / warning messages;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip