src/Pure/Isar/runtime.ML
Wed, 11 Oct 2023 11:59:24 +0200 wenzelm proper Exn.capture / Isabelle_Thread.try_catch;
Thu, 21 Sep 2023 18:14:28 +0200 wenzelm clarified modules;
Wed, 09 Jun 2021 10:52:37 +0200 wenzelm proper profiling within command execution: messages require PIDE id;
Fri, 23 Aug 2019 13:20:13 +0200 wenzelm clarified signature: prefer total operations;
Sat, 17 Aug 2019 13:39:28 +0200 wenzelm more robust, notably for open_proof of unnamed derivation;
Sat, 27 May 2017 13:20:35 +0200 wenzelm clarified build errors;
Wed, 06 Apr 2016 16:33:33 +0200 wenzelm clarified modules;
Tue, 05 Apr 2016 20:51:37 +0200 wenzelm clarified modules -- simplified bootstrap;
Sat, 02 Apr 2016 21:55:32 +0200 wenzelm tuned signature;
Sat, 02 Apr 2016 21:10:07 +0200 wenzelm careful export of type-dependent functions, without losing their special status;
Sat, 05 Mar 2016 17:01:45 +0100 wenzelm tuned signature -- clarified modules;
Sat, 05 Mar 2016 13:51:21 +0100 wenzelm tuned signature -- clarified modules;
Thu, 03 Mar 2016 15:23:02 +0100 wenzelm clarified modules;
Wed, 02 Mar 2016 19:43:31 +0100 wenzelm support for ML_exception_debugger;
Sun, 20 Dec 2015 13:11:47 +0100 wenzelm tuned signature;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Tue, 01 Sep 2015 23:10:23 +0200 wenzelm thread context for exceptions from forks, e.g. relevant when printing errors;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Wed, 26 Nov 2014 15:44:32 +0100 wenzelm even more exception traces for Document.update, which goes through additional execution wrappers;
Wed, 26 Nov 2014 14:35:55 +0100 wenzelm more informative failure of protocol commands, with exception trace;
Mon, 03 Nov 2014 15:08:15 +0100 wenzelm clarified legacy code;
Fri, 31 Oct 2014 11:36:41 +0100 wenzelm discontinued obsolete Output.urgent_message;
Fri, 15 Aug 2014 13:39:59 +0200 wenzelm explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
Thu, 31 Jul 2014 20:09:30 +0200 wenzelm more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
Thu, 24 Jul 2014 23:17:26 +0200 wenzelm more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
Thu, 27 Mar 2014 17:12:40 +0100 wenzelm clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
Tue, 25 Mar 2014 16:54:38 +0100 wenzelm 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);
Mon, 24 Mar 2014 12:00:17 +0100 wenzelm discontinued Toplevel.debug in favour of system option "exception_trace";
Wed, 18 Sep 2013 13:18:51 +0200 wenzelm improved printing of exception trace in Poly/ML 5.5.1;
Wed, 17 Jul 2013 17:16:51 +0200 wenzelm more robust exn_messages_ids;
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;
less more (0) -60 tip