makarius at sketis.net
Mon May 5 17:48:23 CEST 2014
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:
Invoke_Scala.method "java.lang.System.getProperty" "java.home"
This has very low overhead, although there is some latency due to the PIDE
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.
More information about the isabelle-dev