| Mon, 31 Mar 2014 10:28:08 +0200 |
wenzelm |
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 17:39:03 +0100 |
wenzelm |
clarifed module name;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 11:13:25 +0100 |
wenzelm |
tuned errors -- in accordance to Scala version;
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 14:39:44 +0100 |
wenzelm |
more integrity checks of theory names vs. full node names;
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 22:35:38 +0100 |
wenzelm |
more integrity checks of theory names vs. full node names -- at least for the scope of a single use_thys (or "theories" section in ROOT);
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 13:23:23 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Fri, 22 Nov 2013 20:36:57 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Sat, 16 Nov 2013 22:17:45 +0100 |
wenzelm |
prefer explicit "document" flag -- eliminated stateful Present.no_document;
|
file |
diff |
annotate
|
| Sat, 16 Nov 2013 13:12:02 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 06 Nov 2013 20:58:11 +0100 |
wenzelm |
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 11:29:01 +0200 |
wenzelm |
Execution.fork formally requires registered Execution.running;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2013 20:32:26 +0200 |
wenzelm |
maintain goal forks as part of global execution;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2013 17:04:22 +0200 |
wenzelm |
simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 15:59:02 +0200 |
wenzelm |
clarified protocol_message undefinedness;
|
file |
diff |
annotate
|
| Wed, 13 Mar 2013 21:25:08 +0100 |
wenzelm |
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
|
file |
diff |
annotate
|
| Mon, 04 Mar 2013 11:36:16 +0100 |
wenzelm |
join all proofs before scheduling present phase (ordered according to weight);
|
file |
diff |
annotate
|
| Mon, 04 Mar 2013 10:02:58 +0100 |
wenzelm |
more explicit datatype result;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 16:27:44 +0100 |
wenzelm |
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 12:45:19 +0100 |
wenzelm |
discontinued obsolete 'uses' within theory header;
|
file |
diff |
annotate
|
| Tue, 26 Feb 2013 19:44:26 +0100 |
wenzelm |
fork diagnostic commands (theory loader and PIDE interaction);
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 15:22:22 +0100 |
wenzelm |
more tight representation of command timing;
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 12:58:32 +0100 |
wenzelm |
support for prescient timing information within command transactions;
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 19:45:32 +0100 |
wenzelm |
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 15:00:48 +0100 |
wenzelm |
immediate theory progress for build_dialog;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 19:18:49 +0200 |
wenzelm |
some support for registering forked proofs within Proof.state, using its bottom context;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 16:39:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 22:10:27 +0200 |
wenzelm |
more accurate defining position of theory;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 12:33:42 +0200 |
wenzelm |
simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
|
file |
diff |
annotate
|