src/Pure/Isar/runtime.ML
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2016-04-02 wenzelm 2016-04-02 tuned signature;
2016-04-02 wenzelm 2016-04-02 careful export of type-dependent functions, without losing their special status;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2016-03-03 wenzelm 2016-03-03 clarified modules; tuned signature;
2016-03-02 wenzelm 2016-03-02 support for ML_exception_debugger;
2015-12-20 wenzelm 2015-12-20 tuned signature;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-01 wenzelm 2015-09-01 thread context for exceptions from forks, e.g. relevant when printing errors; tuned signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-26 wenzelm 2014-11-26 even more exception traces for Document.update, which goes through additional execution wrappers;
2014-11-26 wenzelm 2014-11-26 more informative failure of protocol commands, with exception trace; eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);
2014-11-03 wenzelm 2014-11-03 clarified legacy code;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-08-15 wenzelm 2014-08-15 explicit system message for protocol failure -- show on Syslog panel instead of Raw Output; more robust crash recovery: warning could crash again;
2014-07-31 wenzelm 2014-07-31 more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
2014-07-24 wenzelm 2014-07-24 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 wenzelm 2014-03-27 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-25 wenzelm 2014-03-25 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 wenzelm 2014-03-24 discontinued Toplevel.debug in favour of system option "exception_trace";
2013-09-18 wenzelm 2013-09-18 improved printing of exception trace in Poly/ML 5.5.1;
2013-07-17 wenzelm 2013-07-17 more robust exn_messages_ids; more robust failure of exn_messages_ids;
2013-04-09 wenzelm 2013-04-09 tuned message;
2013-04-08 wenzelm 2013-04-08 improved printing of exception CTERM (see also d0f0f37ec346);
2013-04-08 wenzelm 2013-04-08 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 wenzelm 2013-02-26 tuned signature;
2013-02-22 wenzelm 2013-02-22 identify exceptions more robustly, to allow SML/NJ report toplevel errors without crash;
2013-01-16 wenzelm 2013-01-16 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16 wenzelm 2013-01-16 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2012-12-13 wenzelm 2012-12-13 smarter handling of tracing messages: prover process pauses and enters user dialog;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-28 wenzelm 2012-09-28 smarter handling of tracing messages;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-14 wenzelm 2011-11-14 simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
2011-11-14 wenzelm 2011-11-14 more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
2011-10-19 wenzelm 2011-10-19 more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
2011-08-19 wenzelm 2011-08-19 more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
2011-08-18 wenzelm 2011-08-18 more precise treatment of exception nesting and serial numbers;
2011-08-18 wenzelm 2011-08-18 more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-18 wenzelm 2011-08-18 tune Par_Exn.make: balance merge; clarified Par_Exn.dest: later exceptions first;
2011-08-17 wenzelm 2011-08-17 identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
2011-08-17 wenzelm 2011-08-17 more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;
2011-07-11 wenzelm 2011-07-11 tuned signature -- corresponding to Scala version;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-02-08 wenzelm 2011-02-08 explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;
2010-11-03 wenzelm 2010-11-03 discontinued obsolete function sys_error and exception SYS_ERROR;
2010-09-17 wenzelm 2010-09-17 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 wenzelm 2010-09-17 eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
2010-09-10 wenzelm 2010-09-10 avoid extra wrapping for interrupts;
2010-09-09 wenzelm 2010-09-09 refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
2010-09-09 wenzelm 2010-09-09 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-08-30 wenzelm 2010-08-30 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
2010-08-30 wenzelm 2010-08-30 more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
2010-06-09 wenzelm 2010-06-09 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 wenzelm 2009-11-10 generalized Runtime.toplevel_error wrt. output function;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;