Jason Hu (May 04 2026 at 15:38): Jason Hu (May 04 2026 at 15:38):Hi all,
whenever I go to Isabelle level, it seems that go to definition clicks might just stop working in jedit. For example, if I click datatype, the chances are, go to definition has stopped working. How do I browse isabelle/ML code more smoothly? What is your trick?
Fabian Huch (May 04 2026 at 15:46):load ROOT.ML to create a session of Pure within Pure.
Jason Hu (May 04 2026 at 18:13):could you elaborate what exactly you would do?
Kevin Kappelmann (May 04 2026 at 18:46):Hi Jason, I think Fabian wants you to open $ISABELLE_HOME/src/Pure/ROOT.ML in jedit. This enables "go to definition" in ML sources that are preloaded by Isabelle/Pure.
Is this what you are looking for?
Jason Hu (May 04 2026 at 19:32):thank you. it works to some degree but I am not able to jump to all definitions. for example, i am in the middle of doing some case analysis in isabelle and would like to understand how Induct_Tacs.case_tac works, at that point, I've lost the jump to deifnitions again. I opened its ROOT file but it still doesn't work. what's the next I should do?
Kevin Kappelmann (May 05 2026 at 12:19):If Pure/ROOT.ML is opened and loaded and it does not work, I don't know.
Fabian Huch (May 05 2026 at 13:25):Induct_Tacs is not in Pure
Fabian Huch (May 05 2026 at 13:27):You need to interactively load the session you are interested in
Fabian Huch (May 05 2026 at 13:28):Which is not possible for Pure, hence the Pure in Pure via ROOT.ML
Jason Hu (May 05 2026 at 20:42):Pure/ROOT.ML does allow me to view the Pure folder. how do I load Induct_Tacs? my ML code has been using it. but it still doesn't browse it?
Last updated: May 15 2026 at 17:41 UTC