[isabelle-dev] scala-2.11.0

[Makarius]

Here is a funny presentation on the Future of Programming from "1973"
http://worrydream.com/#!/TheFutureOfProgramming

I could have put that on the thread "Remaining uses of Proof General", 
because it touches recurrent problems of getting stuck with accidental 
situations over decades, and the importance to unlearn old customs. But it 
also fits here on the thread about scala-2.11.0 and actors.


The talk briefly contrasts old-fashioned "threads + locks" with the 
brand-new actor model:

   Carl Hewitt; Peter Bishop; Richard Steiger (1973). A Universal Modular
   Actor Formalism for Artificial Intelligence. IJCAI.

As already explained, Scala had an on-board implementation of actors over 
several years, but it is now deprecated.  The replacement is the huge Akka 
framework.  So I discontinued that in Isabelle/Scala, and replaced it by a 
plain "threads + locks" implementation of the more elementary concept of 
Consumer_Thread.

That is basically a plain function with asynchronous input queue, and 
simple means to apply it in synchronous mode (without result).  If a 
result is required it can be done with Future.promise, as seen here 
http://isabelle.in.tum.de/repos/isabelle/annotate/bc50d5e04e90/src/Pure/Tools/simplifier_trace.scala#l139 
for example.

The performance of the Consumer_Thread input queue (Mailbox) is much 
better than that of the old actors, and resource allocation is more 
predictable.  I have started using that a bit more often now, e.g. in the 
now asynchronous interpreter of the Scala console in Isabelle/jEdit 
http://isabelle.in.tum.de/repos/isabelle/annotate/69531d86d77e/src/Tools/jEdit/src/scala_console.scala#l137


 	Makarius