2011-04-05 ago discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-02-08 ago explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;
2010-11-03 ago discontinued obsolete function sys_error and exception SYS_ERROR;
2010-09-17 ago 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);
2010-09-17 ago eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
2010-09-10 ago avoid extra wrapping for interrupts;
2010-09-09 ago refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
2010-09-09 ago more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-08-30 ago tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
2010-08-30 ago more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
2010-06-09 ago explicit treatment of empty exception block, which could lead to confusing output (e.g. in the theory loader), or even prevent error output altogether;
2009-11-10 ago generalized Runtime.toplevel_error wrt. output function;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-06 ago moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);