src/Pure/Isar/runtime.ML
2014-11-26 ago more informative failure of protocol commands, with exception trace;
2014-11-03 ago clarified legacy code;
2014-10-31 ago discontinued obsolete Output.urgent_message;
2014-08-15 ago explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
2014-07-31 ago more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
2014-07-24 ago more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
2014-03-27 ago clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-25 ago clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
2014-03-24 ago discontinued Toplevel.debug in favour of system option "exception_trace";
2013-09-18 ago improved printing of exception trace in Poly/ML 5.5.1;
2013-07-17 ago more robust exn_messages_ids;
2013-04-09 ago tuned message;
2013-04-08 ago improved printing of exception CTERM (see also d0f0f37ec346);
2013-04-08 ago prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
2013-02-26 ago tuned signature;
2013-02-22 ago identify exceptions more robustly, to allow SML/NJ report toplevel errors without crash;
2013-01-16 ago identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16 ago more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2012-12-13 ago smarter handling of tracing messages: prover process pauses and enters user dialog;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-28 ago smarter handling of tracing messages;
2012-08-29 ago renamed Position.str_of to Position.here;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-14 ago simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
2011-11-14 ago more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
2011-10-19 ago more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
2011-08-19 ago more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
2011-08-18 ago more precise treatment of exception nesting and serial numbers;
2011-08-18 ago more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-18 ago tune Par_Exn.make: balance merge;
2011-08-17 ago identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
2011-08-17 ago more systematic handling of parallel exceptions;
2011-07-11 ago tuned signature -- corresponding to Scala version;
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);