Stream: General

Topic: Editing Pure


view this post on Zulip Lukas Stevens (Nov 26 2019 at 15:22):

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?

view this post on Zulip Josh Chen (Nov 26 2019 at 15:32):

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.

view this post on Zulip Mathias Fleury (Dec 06 2019 at 08:27):

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: Aug 15 2022 at 02:13 UTC