Re: [isabelle] Calling Isabelle tools without exiting



On 04/10/17 10:15, Lars Hupel wrote:
> 
> what is the official way (from Isabelle/Scala) to invoke an Isabelle
> tool without exiting the JVM? For example, if I want to invoke a
> sequence of tools.

Most Isabelle command-line tools are indeed implemented in
Isabelle/Scala today, but the tool wrapper assumes that it is the only
(or last) thing that this JVM runs. Thus the JVM will finally exit,
after printing exceptions properly without "Java vomit". See also the
module Command_Line (both in Scala and ML).

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

Note that PATH within the Isabelle environment has $ISABELLE_HOME/bin
first, so "isabelle" above refers to the running Isabelle installation.

Further not that operations like File.bash_path and Bash.string help to
compose bash scripts reliably.


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.

E.g. for the above that is Build.build, which I often use in the
Isabelle/Scala console of Isabelle/jEdit, in the absence of proper IDE
support for the build process.


	Makarius




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