Fri, 25 Apr 2014 22:13:17 +0200 blanchet use Z3 4.3.2 to fix most FIXMEs
Fri, 25 Apr 2014 22:13:17 +0200 blanchet added Z3 4.3.2 (unstable) component
Fri, 25 Apr 2014 22:13:17 +0200 blanchet updated Z3 version number
Fri, 25 Apr 2014 22:13:17 +0200 blanchet use Z3 4.3.2 syntax
Fri, 25 Apr 2014 21:45:04 +0200 haftmann subscription as target-specific implementation device
Fri, 25 Apr 2014 17:54:54 +0200 wenzelm make SML/NJ happier;
Fri, 25 Apr 2014 14:39:11 +0200 wenzelm merged
Fri, 25 Apr 2014 14:18:13 +0200 wenzelm updated properties for scala.concurrent.ExecutionContext.Implicits.global (future task farm), similar to Isabelle/ML;
Fri, 25 Apr 2014 13:55:50 +0200 wenzelm simplified change_buffer (again, see 937826d702d5): no thread, just timer, rely on asynchronous commands_changed.post;
Fri, 25 Apr 2014 13:29:56 +0200 wenzelm replaced manager Actor by Consumer_Thread, which is lazy to defer its start to actual Handler init time;
Fri, 25 Apr 2014 12:59:33 +0200 wenzelm tuned whitespace;
Fri, 25 Apr 2014 12:56:24 +0200 wenzelm obsolete;
Fri, 25 Apr 2014 12:51:08 +0200 wenzelm clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
Fri, 25 Apr 2014 12:27:18 +0200 wenzelm tuned comments;
Fri, 25 Apr 2014 11:09:59 +0200 wenzelm more robust prover termination;
Fri, 25 Apr 2014 10:51:57 +0200 wenzelm more explicit checks;
Thu, 24 Apr 2014 23:21:00 +0200 wenzelm tuned signature;
Thu, 24 Apr 2014 23:13:17 +0200 wenzelm more uniform warning/error handling, potentially with propagation to send_wait caller;
Thu, 24 Apr 2014 23:02:10 +0200 wenzelm more careful shutdown (amending f2f53f7046f4);
Thu, 24 Apr 2014 22:41:03 +0200 wenzelm misc tuning;
Thu, 24 Apr 2014 22:20:36 +0200 wenzelm obsolete;
Thu, 24 Apr 2014 22:10:00 +0200 wenzelm converted main session manager to Consumer_Thread: messages need to be consumed immediately, postponed_changes replaces implicit actor mailbox scanning;
Thu, 24 Apr 2014 18:04:18 +0200 wenzelm simplified commands_changed_buffer (in contrast to a8331fb5c959): rely on better performance of Consumer_Thread/Mailbox and more direct Timer (like session_actor.receiver);
Thu, 24 Apr 2014 16:52:17 +0200 wenzelm simplified -- prefer Consumer_Thread over Actor;
Thu, 24 Apr 2014 16:47:47 +0200 wenzelm tuned imports;
Thu, 24 Apr 2014 16:19:11 +0200 wenzelm support for requests with explicit acknowledgment (and exception propagation);
Thu, 24 Apr 2014 15:19:11 +0200 wenzelm more robust thread: continue after failure;
Thu, 24 Apr 2014 15:02:13 +0200 wenzelm clarified command_input: Consumer_Thread;
Thu, 24 Apr 2014 14:59:46 +0200 wenzelm further robustification wrt. unclear ranges;
Thu, 24 Apr 2014 14:51:41 +0200 wenzelm allow more control of main loop;
Thu, 24 Apr 2014 13:54:45 +0200 wenzelm eliminated pointless output actors;
Thu, 24 Apr 2014 13:40:29 +0200 wenzelm more robust shutdown;
Thu, 24 Apr 2014 13:13:48 +0200 wenzelm consumer thread with unbounded queueing of requests (similar to Message_Channel in ML);
Thu, 24 Apr 2014 13:10:42 +0200 wenzelm proper signaling after each state update (NB: ML version does this uniformly via timed_access);
Thu, 24 Apr 2014 12:10:26 +0200 wenzelm added Mailbox, as in ML;
Thu, 24 Apr 2014 12:09:55 +0200 wenzelm synchronized access, similar to ML version;
Thu, 24 Apr 2014 11:01:14 +0200 wenzelm tuned signature, in accordance to ML version;
Thu, 24 Apr 2014 10:38:14 +0200 wenzelm eliminated redundant Volatile;
Thu, 24 Apr 2014 10:33:06 +0200 wenzelm retain canonical reverse order;
Thu, 24 Apr 2014 10:30:55 +0200 wenzelm more canonical list operations;
Thu, 24 Apr 2014 10:24:44 +0200 wenzelm tuned signature in accordance to ML version;
Thu, 24 Apr 2014 00:29:55 +0200 wenzelm canonical list operations, as in ML;
Thu, 24 Apr 2014 00:27:06 +0200 wenzelm more uniform synchronized variables;
Fri, 25 Apr 2014 12:09:15 +0200 blanchet more unfolding and more folding in size equations, to look more natural in the nested case
Fri, 25 Apr 2014 11:58:10 +0200 blanchet reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
Thu, 24 Apr 2014 21:00:00 +0200 blanchet really unfold
Thu, 24 Apr 2014 17:52:19 +0200 haftmann avoid non-standard simp default rule
Thu, 24 Apr 2014 10:33:17 +0200 haftmann now covered by AFP 3ddac3e572cf
Thu, 24 Apr 2014 00:23:38 +0200 blanchet avoid name shadowing
Thu, 24 Apr 2014 00:08:48 +0200 blanchet spelling
Wed, 23 Apr 2014 17:57:56 +0200 kuncar predicator simplification rules: support also partially specialized types e.g. 'a * nat
Wed, 23 Apr 2014 17:57:56 +0200 kuncar all BNF tests can be part of a normal session because they are much faster now
Wed, 23 Apr 2014 17:05:48 +0200 wenzelm merged
Wed, 23 Apr 2014 15:57:06 +0200 wenzelm tuned;
Wed, 23 Apr 2014 15:22:48 +0200 wenzelm modernized Future/Promise implementation, bypassing old actors;
Wed, 23 Apr 2014 14:16:08 +0200 wenzelm updated according to scala-2.11.0 recommendations;
Wed, 23 Apr 2014 13:28:32 +0200 wenzelm explicit Exn.error_message in accordance to Output.error_message in ML;
Wed, 23 Apr 2014 13:05:11 +0200 wenzelm detect nested interrupts;
Wed, 23 Apr 2014 12:55:57 +0200 wenzelm clarified message and return code, in accordance to ML version;
Wed, 23 Apr 2014 12:51:55 +0200 wenzelm interruptible dependencies, which can take a few seconds;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip