Thu, 17 May 2012 15:23:00 +0200 |
wenzelm |
tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;
|
file |
diff |
annotate
|
Wed, 11 Apr 2012 15:02:48 +0200 |
wenzelm |
clarified proof_result: finish proof formally via head tr, not end_tr;
|
file |
diff |
annotate
|
Tue, 10 Apr 2012 22:53:41 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
Tue, 10 Apr 2012 21:31:05 +0200 |
wenzelm |
static relevance of proof via syntax keywords;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 19:10:52 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
Wed, 21 Mar 2012 23:26:35 +0100 |
wenzelm |
more explicit Toplevel.open_target/close_target;
|
file |
diff |
annotate
|
Fri, 16 Mar 2012 14:42:11 +0100 |
wenzelm |
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
Mon, 14 Nov 2011 16:52:19 +0100 |
wenzelm |
pass positions for named targets, for formal links in the document model;
|
file |
diff |
annotate
|
Fri, 19 Aug 2011 23:25:47 +0200 |
wenzelm |
maintain recent future proofs at transaction boundaries;
|
file |
diff |
annotate
|
Thu, 18 Aug 2011 17:53:32 +0200 |
wenzelm |
more careful treatment of exception serial numbers, with propagation to message channel;
|
file |
diff |
annotate
|
Mon, 15 Aug 2011 20:38:16 +0200 |
wenzelm |
tuned error message;
|
file |
diff |
annotate
|
Sat, 13 Aug 2011 21:06:01 +0200 |
wenzelm |
clarified Toplevel.end_theory;
|
file |
diff |
annotate
|
Sat, 13 Aug 2011 20:49:41 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special name argument;
|
file |
diff |
annotate
|
Sat, 13 Aug 2011 20:41:29 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special master argument;
|
file |
diff |
annotate
|
Sat, 13 Aug 2011 20:20:36 +0200 |
wenzelm |
provide node header via Scala layer;
|
file |
diff |
annotate
|
Tue, 05 Jul 2011 20:36:49 +0200 |
wenzelm |
get theory from last executation state;
|
file |
diff |
annotate
|
Tue, 05 Jul 2011 19:45:59 +0200 |
wenzelm |
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 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Sat, 26 Mar 2011 21:45:29 +0100 |
wenzelm |
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 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file |
diff |
annotate
|
Fri, 04 Feb 2011 17:11:00 +0100 |
wenzelm |
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
|
file |
diff |
annotate
|
Mon, 31 Jan 2011 23:02:53 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 31 Jan 2011 22:57:01 +0100 |
wenzelm |
support named tasks, for improved tracing;
|
file |
diff |
annotate
|
Thu, 13 Jan 2011 17:34:45 +0100 |
wenzelm |
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 |
wenzelm |
formal notepad without any result;
|
file |
diff |
annotate
|
Mon, 25 Oct 2010 21:06:56 +0200 |
wenzelm |
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 |
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);
|
file |
diff |
annotate
|
Fri, 10 Sep 2010 23:11:58 +0200 |
wenzelm |
avoid extra wrapping for interrupts;
|
file |
diff |
annotate
|
Thu, 09 Sep 2010 18:18:34 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
Thu, 09 Sep 2010 17:20:27 +0200 |
wenzelm |
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 |
wenzelm |
moved Toplevel.run_command to Pure/PIDE/document.ML;
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 16:49:41 +0200 |
wenzelm |
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 |
wenzelm |
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 21:31:22 +0200 |
wenzelm |
added some proof state markup, notably number of subgoals (e.g. for indentation);
|
file |
diff |
annotate
|
Thu, 12 Aug 2010 13:42:13 +0200 |
haftmann |
named target is optional; explicit Name_Target.reinit
|
file |
diff |
annotate
|
Thu, 12 Aug 2010 13:28:18 +0200 |
haftmann |
Named_Target.init: empty string represents theory target
|
file |
diff |
annotate
|
Thu, 12 Aug 2010 13:23:46 +0200 |
haftmann |
Named_Target.theory_init
|
file |
diff |
annotate
|
Wed, 11 Aug 2010 20:25:44 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
Wed, 11 Aug 2010 17:16:02 +0200 |
haftmann |
avoid arcane Local_Theory.reinit entirely
|
file |
diff |
annotate
|
Wed, 11 Aug 2010 18:17:53 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
Wed, 11 Aug 2010 14:45:38 +0200 |
haftmann |
renamed Theory_Target to the more appropriate Named_Target
|
file |
diff |
annotate
|
Wed, 11 Aug 2010 18:11:07 +0200 |
wenzelm |
removed obsolete Toplevel.enter_proof_body;
|
file |
diff |
annotate
|
Sun, 08 Aug 2010 19:36:31 +0200 |
wenzelm |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
file |
diff |
annotate
|
Tue, 27 Jul 2010 22:00:26 +0200 |
wenzelm |
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 |
wenzelm |
simplified handling of theory begin/end wrt. toplevel and theory loader;
|
file |
diff |
annotate
|
Sat, 24 Jul 2010 21:40:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 24 Jul 2010 21:22:21 +0200 |
wenzelm |
moved basic thy file name operations from Thy_Load to Thy_Header;
|
file |
diff |
annotate
|
Sat, 24 Jul 2010 12:14:53 +0200 |
wenzelm |
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 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 22 Jul 2010 14:59:27 +0200 |
wenzelm |
eliminated some unreferenced identifiers;
|
file |
diff |
annotate
|
Thu, 22 Jul 2010 14:01:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 21 Jul 2010 13:25:14 +0200 |
wenzelm |
clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
|
file |
diff |
annotate
|
Tue, 20 Jul 2010 21:07:23 +0200 |
wenzelm |
avoid duplicate printing of 'theory' state (cf. 173974e07dea);
|
file |
diff |
annotate
|
Tue, 20 Jul 2010 20:56:28 +0200 |
wenzelm |
toplevel pp for Proof.state and Toplevel.state;
|
file |
diff |
annotate
|
Tue, 20 Jul 2010 18:33:19 +0200 |
wenzelm |
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 |
wenzelm |
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
|
Mon, 05 Jul 2010 20:36:39 +0200 |
wenzelm |
async_state: report within proper transaction context;
|
file |
diff |
annotate
|
Sun, 04 Jul 2010 21:01:22 +0200 |
wenzelm |
general Future.report -- also for Toplevel.async_state;
|
file |
diff |
annotate
|