[isabelle-dev] scala-2.11.0

[Makarius]

On Mon, 5 May 2014, Gottfried Barrow wrote:

> Cutting this short(er), part of my reject of Scala was because external 
> calls to the JVM are slow, which is important for "REPL use", but I 
> figured out it's not of ultimate importance, which led to me installing 
> and using JRuby in my own distribution folder.

Here I guess you mean something like the isabelle_scala_script wrapper, 
which is indeed very slow on startup for two reasons:

   (1) startup of a full JVM,
   (2) long and painful warmup of the Scala compiler.

Then it only runs once on a small script.  After the long prelude it is 
actually fast, although that is too late.


In normal operation of the PIDE infrastructure, Isabelle/ML vs. 
Isabelle/Scala process are your two feet for walking rather quickly, but 
with wearing two differently coloured socks.


Here is a quick invocation of JVM functionality from inside Isabelle/ML:

ML {*
   Invoke_Scala.method "java.lang.System.getProperty" "java.home"
*}

This has very low overhead, although there is some latency due to the PIDE 
protocol.

That gives you a String => String function invocation interface from ML to 
Scala.  It is an easy exercise to use the YXML and XML.Encode / XML.Decode 
modules to pass structured data back an forth.

It is a reasonably easy exercise, to invoke the Scala compiler on some 
source script on the spot, e.g. see the scala_console.scala in the 
Isabelle/jEdit source directory.

It is probably more than an exercise to invoke the Scala compiler in a way 
that it produces nice IDE markup for the source text.


 	Makarius