I can start Isabelle with Pure as a prebuilt logic using `isabelle jedit -l Pure`

. Can I also start Isabelle without prebuilding Pure, i.e. such that only the ML Bootstrapping is prebuilt, in order to edit Pure itself and get working goto definitions?

If you open the file "src/Pure/ROOT.ML" (available in the Isabelle/jEdit Documentation panel) an editable copy of Pure will be loaded for your session, and you'll be able to CTRL-click etc.

I can start Isabelle with Pure as a prebuilt logic using

`isabelle jedit -l Pure`

. Can I also start Isabelle without prebuilding Pure, i.e. such that only the ML Bootstrapping is prebuilt, in order to edit Pure itself and get working goto definitions?

isabelle jedit -R Pure?

(I am aware that the question was asked a few weeks ago, but I believe the other answer is not the optimal way to do it)

Last updated: Dec 07 2023 at 08:19 UTC