Re: [isabelle] Calling Isabelle tools without exiting

> So multiple invocations of the tool wrapper require a separate process
> each time. This can be done in Isabelle/Scala by the
> Isabelle_System.bash operation, e.g. like this:
>   Isabelle_System.bash("isabelle build").check

Thanks, I have used that now.

> Another possibility (often better) is to invoke the underlying Scala
> operations within the running JVM process. Every Isabelle tool should
> have such an entry as a regular function, with typed interface and
> normal exception behavior.

In this particular case it is about invoking a "dynamic" Scala script
from the AFP, so there's no Scala entry point visible statically.

With the ever-increasing importance of Isabelle/Scala as a systems
language (and thus, for the AFP), we should consider a more robust and
less ad-hoc way of adding Scala tools to the classpath from within


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.