| Mon, 15 Aug 2011 20:38:16 +0200 |
tuned error message;
|
file | diff | annotate |
| Sat, 13 Aug 2011 21:06:01 +0200 |
clarified Toplevel.end_theory;
|
file | diff | annotate |
| Sat, 13 Aug 2011 20:49:41 +0200 |
simplified Toplevel.init_theory: discontinued special name argument;
|
file | diff | annotate |
| Sat, 13 Aug 2011 20:41:29 +0200 |
simplified Toplevel.init_theory: discontinued special master argument;
|
file | diff | annotate |
| Sat, 13 Aug 2011 20:20:36 +0200 |
provide node header via Scala layer;
|
file | diff | annotate |
| Tue, 05 Jul 2011 20:36:49 +0200 |
get theory from last executation state;
|
file | diff | annotate |
| Tue, 05 Jul 2011 19:45:59 +0200 |
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
|
file | diff | annotate |
| Tue, 05 Jul 2011 11:16:37 +0200 |
tuned signature;
|
file | diff | annotate |
| Sat, 16 Apr 2011 15:47:52 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Sat, 26 Mar 2011 21:45:29 +0100 |
present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
|
file | diff | annotate |
| Sun, 20 Mar 2011 21:28:11 +0100 |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file | diff | annotate |
| Fri, 04 Feb 2011 17:11:00 +0100 |
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
|
file | diff | annotate |
| Mon, 31 Jan 2011 23:02:53 +0100 |
tuned signature;
|
file | diff | annotate |
| Mon, 31 Jan 2011 22:57:01 +0100 |
support named tasks, for improved tracing;
|
file | diff | annotate |
| Fri, 25 Feb 2011 13:04:56 +0100 |
merged isabisac with Isabelle2011
|
file | diff | annotate |
| Thu, 13 Jan 2011 17:34:45 +0100 |
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
|
file | diff | annotate |
| Sat, 04 Dec 2010 21:26:55 +0100 |
formal notepad without any result;
|
file | diff | annotate |
| Mon, 25 Oct 2010 21:06:56 +0200 |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file | diff | annotate |
| Fri, 17 Sep 2010 22:17:57 +0200 |
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);
|
file | diff | annotate |
| Fri, 10 Sep 2010 23:11:58 +0200 |
avoid extra wrapping for interrupts;
|
file | diff | annotate |
| Thu, 09 Sep 2010 18:18:34 +0200 |
removed dead code;
|
file | diff | annotate |
| Thu, 09 Sep 2010 17:20:27 +0200 |
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
|
file | diff | annotate |
| Tue, 31 Aug 2010 23:46:49 +0200 |
moved Toplevel.run_command to Pure/PIDE/document.ML;
|
file | diff | annotate |
| Mon, 30 Aug 2010 16:49:41 +0200 |
Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
|
file | diff | annotate |
| Mon, 30 Aug 2010 15:19:39 +0200 |
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
|
file | diff | annotate |
| Wed, 25 Aug 2010 21:31:22 +0200 |
added some proof state markup, notably number of subgoals (e.g. for indentation);
|
file | diff | annotate |
| Thu, 12 Aug 2010 13:42:13 +0200 |
named target is optional; explicit Name_Target.reinit
|
file | diff | annotate |
| Thu, 12 Aug 2010 13:28:18 +0200 |
Named_Target.init: empty string represents theory target
|
file | diff | annotate |
| Thu, 12 Aug 2010 13:23:46 +0200 |
Named_Target.theory_init
|
file | diff | annotate |
| Wed, 11 Aug 2010 20:25:44 +0200 |
merged
|
file | diff | annotate |
| Wed, 11 Aug 2010 17:16:02 +0200 |
avoid arcane Local_Theory.reinit entirely
|
file | diff | annotate |
| Wed, 11 Aug 2010 18:17:53 +0200 |
merged
|
file | diff | annotate |
| Wed, 11 Aug 2010 18:11:07 +0200 |
removed obsolete Toplevel.enter_proof_body;
|
file | diff | annotate |
| Wed, 11 Aug 2010 14:45:38 +0200 |
renamed Theory_Target to the more appropriate Named_Target
|
file | diff | annotate |
| Sun, 08 Aug 2010 19:36:31 +0200 |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
file | diff | annotate |
| Tue, 27 Jul 2010 22:00:26 +0200 |
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
|
file | diff | annotate |
| Sun, 25 Jul 2010 14:41:48 +0200 |
simplified handling of theory begin/end wrt. toplevel and theory loader;
|
file | diff | annotate |
| Sat, 24 Jul 2010 21:40:48 +0200 |
tuned;
|
file | diff | annotate |
| Sat, 24 Jul 2010 21:22:21 +0200 |
moved basic thy file name operations from Thy_Load to Thy_Header;
|
file | diff | annotate |
| Sat, 24 Jul 2010 12:14:53 +0200 |
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
|
file | diff | annotate |
| Thu, 22 Jul 2010 20:36:41 +0200 |
tuned signature;
|
file | diff | annotate |
| Thu, 22 Jul 2010 14:59:27 +0200 |
eliminated some unreferenced identifiers;
|
file | diff | annotate |
| Thu, 22 Jul 2010 14:01:43 +0200 |
tuned;
|
file | diff | annotate |
| Wed, 21 Jul 2010 13:25:14 +0200 |
clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
|
file | diff | annotate |
| Tue, 20 Jul 2010 21:07:23 +0200 |
avoid duplicate printing of 'theory' state (cf. 173974e07dea);
|
file | diff | annotate |
| Tue, 20 Jul 2010 20:56:28 +0200 |
toplevel pp for Proof.state and Toplevel.state;
|
file | diff | annotate |
| Tue, 20 Jul 2010 18:33:19 +0200 |
Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;
|
file | diff | annotate |
| Tue, 20 Jul 2010 14:44:33 +0200 |
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
|
file | diff | annotate |
| Fri, 23 Jul 2010 11:17:26 +0200 |
1st update in decompose-isar
|
file | diff | annotate |
| Fri, 23 Jul 2010 10:34:42 +0200 |
start branch decompose-isar
|
file | diff | annotate |
| Mon, 05 Jul 2010 20:36:39 +0200 |
async_state: report within proper transaction context;
|
file | diff | annotate |
| Sun, 04 Jul 2010 21:01:22 +0200 |
general Future.report -- also for Toplevel.async_state;
|
file | diff | annotate |
| Sat, 03 Jul 2010 23:24:36 +0200 |
run_command: actually observe "print" flag;
|
file | diff | annotate |
| Sat, 03 Jul 2010 22:33:10 +0200 |
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
|
file | diff | annotate |
| Mon, 31 May 2010 21:06:57 +0200 |
modernized some structure names, keeping a few legacy aliases;
|
file | diff | annotate |
| Mon, 31 May 2010 16:45:48 +0200 |
Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;
|
file | diff | annotate |
| Sat, 15 May 2010 23:16:32 +0200 |
refer directly to structure Keyword and Parse;
|
file | diff | annotate |
| Mon, 26 Apr 2010 21:36:44 +0200 |
proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;
|
file | diff | annotate |
| Fri, 23 Apr 2010 21:00:28 +0200 |
added keyword category "schematic goal", which prevents any attempt to fork the proof;
|
file | diff | annotate |
| Thu, 18 Feb 2010 23:41:01 +0100 |
removed unused Theory_Target.begin;
|
file | diff | annotate |