| Sat, 15 Aug 2015 19:42:35 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 14 Jan 2015 16:27:19 +0100 |
wenzelm |
clarified build_theories: proper protocol handler;
|
file |
diff |
annotate
|
| Wed, 14 Jan 2015 14:28:52 +0100 |
wenzelm |
clarified build_theories;
|
file |
diff |
annotate
|
| Tue, 13 Jan 2015 21:46:09 +0100 |
wenzelm |
some support for PIDE batch session;
|
file |
diff |
annotate
|
| Mon, 22 Dec 2014 20:40:37 +0100 |
wenzelm |
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
|
file |
diff |
annotate
|
| Mon, 22 Dec 2014 18:10:54 +0100 |
wenzelm |
proper Synchronized.var;
|
file |
diff |
annotate
|
| Mon, 22 Dec 2014 17:17:00 +0100 |
wenzelm |
removed remains from Proof General;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:37:22 +0100 |
wenzelm |
provide explicit theory (amending 621c052789b4);
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 21:35:11 +0100 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 21:20:06 +0100 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 20:18:27 +0200 |
wenzelm |
tuned signature according to Scala version -- prefer explicit argument;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 21:02:45 +0200 |
wenzelm |
more official Thy_Info.script_thy;
|
file |
diff |
annotate
|
| 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
|