search

andriusvelykis / isabelle-eclipse

Eclipse integration for Isabelle proof assistant.
http://andriusvelykis.github.io/isabelle-eclipse
Eclipse Public License 1.0
12 stars 4 forks source link

Isabelle/Scala invocation not supported in theory/ML files #6

Open andriusvelykis opened 12 years ago

andriusvelykis commented 12 years ago

Using Invoke_Scala.method in Isabelle theory/ML files does not work correctly - the referenced classes are not found.

This happens when custom JARs are installed into Isabelle ext directory and then referenced from the ML code. The classes from these JARs are not found in the JVM.

The issue is with Eclipse's OSGI class-loading. The JARs are used as java extensions, and thus must be included at application startup. Because of plug-in architecture and dynamic selection of Isabelle distribution, these JARs cannot be loaded in such way.

Need to find a solution with dynamic loading of these JARs.

Workaround

As a workaround, include the directory into the classpath of your Eclipse IDE (via eclipse.ini file).

andriusvelykis commented 11 years ago

Possibly some success can be had in using Equinox Adaptor Hooks.

An example here uses Equinox Adaptor Hooks to add DynamicImport-Package declarations and thus update runtime classpath of loaded bundles. See section Providing Additional Runtime Classes to Instrumented Bundles.

Investigate.