Search code examples
isabellejedit

Exploring ML files in Isabelle

I was wondering if in Isabelle ML files there is a way to activate the feature that normal theory files have, i.e, you can press Ctrl+click with mouse in a definition and get the desired definition.

However, this does not seem to work for ML files. Is there any option I can activate to navigate from a function to its definition?

Solution

  • One way to enable the feature that you seek would be to include the ML file in a *.thy file with the command ML_file and have both of them open in jEdit. Of course, there may exist better alternatives.