Stream: Beginner Questions

Topic: Editing a file without disabling navigation in other files

view this post on Zulip David Wang (Feb 02 2025 at 12:28):

Hello,
The navigator plugin seems to only work on checked files. Is there a way to edit a theory file, without losing navigation (<ctrl>+<hover> or <ctrl>+<click>) functionality in every theory file that depends on it? E.g. A.thy depends on B.thy. B takes a long time to check and I still want to navigate through A, while editing B.

view this post on Zulip Mathias Fleury (Feb 02 2025 at 12:43):

The HTML version of the documentation

view this post on Zulip David Wang (Feb 02 2025 at 12:43):

Mathias Fleury said:

The HTML version of the documentation

Thanks

view this post on Zulip Mathias Fleury (Feb 02 2025 at 12:44):

That is my main use case to actually regularly produce and update it

Last updated: Mar 09 2025 at 12:28 UTC