src/Pure/Isar/runtime.ML
Tue, 09 Apr 2013 12:29:36 +0200 wenzelm tuned message;
Mon, 08 Apr 2013 21:01:59 +0200 wenzelm improved printing of exception CTERM (see also d0f0f37ec346);
Mon, 08 Apr 2013 17:10:49 +0200 wenzelm prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
Tue, 26 Feb 2013 19:58:27 +0100 wenzelm tuned signature;
Fri, 22 Feb 2013 17:02:00 +0100 wenzelm identify exceptions more robustly, to allow SML/NJ report toplevel errors without crash;
Wed, 16 Jan 2013 20:41:29 +0100 wenzelm identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
Wed, 16 Jan 2013 16:26:36 +0100 wenzelm more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
Thu, 13 Dec 2012 19:53:55 +0100 wenzelm smarter handling of tracing messages: prover process pauses and enters user dialog;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Fri, 28 Sep 2012 16:51:58 +0200 wenzelm smarter handling of tracing messages;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Mon, 14 Nov 2011 16:24:50 +0100 wenzelm simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
Mon, 14 Nov 2011 16:16:49 +0100 wenzelm more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
Wed, 19 Oct 2011 16:45:46 +0200 wenzelm more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
Fri, 19 Aug 2011 12:51:14 +0200 wenzelm more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
Thu, 18 Aug 2011 18:07:40 +0200 wenzelm more precise treatment of exception nesting and serial numbers;
Thu, 18 Aug 2011 17:53:32 +0200 wenzelm more careful treatment of exception serial numbers, with propagation to message channel;
Thu, 18 Aug 2011 15:15:43 +0200 wenzelm tune Par_Exn.make: balance merge;
Wed, 17 Aug 2011 23:37:23 +0200 wenzelm identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
Wed, 17 Aug 2011 22:14:22 +0200 wenzelm more systematic handling of parallel exceptions;
Mon, 11 Jul 2011 22:55:47 +0200 wenzelm tuned signature -- corresponding to Scala version;
Tue, 05 Apr 2011 14:25:18 +0200 wenzelm discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
Tue, 08 Feb 2011 16:11:52 +0100 wenzelm explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;
Wed, 03 Nov 2010 11:33:51 +0100 wenzelm discontinued obsolete function sys_error and exception SYS_ERROR;
Fri, 17 Sep 2010 22:17:57 +0200 wenzelm 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 15:51:11 +0200 wenzelm eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
Fri, 10 Sep 2010 23:11:58 +0200 wenzelm avoid extra wrapping for interrupts;
Thu, 09 Sep 2010 18:21:06 +0200 wenzelm refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
Thu, 09 Sep 2010 17:20:27 +0200 wenzelm more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
Mon, 30 Aug 2010 15:19:39 +0200 wenzelm tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
Mon, 30 Aug 2010 15:09:20 +0200 wenzelm more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
Wed, 09 Jun 2010 16:23:00 +0200 wenzelm explicit treatment of empty exception block, which could lead to confusing output (e.g. in the theory loader), or even prevent error output altogether;
Tue, 10 Nov 2009 23:15:20 +0100 wenzelm generalized Runtime.toplevel_error wrt. output function;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Sat, 06 Jun 2009 21:11:22 +0200 wenzelm moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
less more (0) tip