You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Jun 26, 2024. It is now read-only.
Right now the info view always shows the error messages at the cursor position, but sometimes you want to monitor the error messages from somewhere else. It would be nice if you could tell the info view to track/focus/bikeshed one position and then continue to work somewhere else. You can already pause the info view, but then you unfortunately don't get any updates.
One example of that use is that you write a theorem and you try to tweak the tactics to make progress on it. You place your focus on that theorem, then you start changing the code of the tactic. You have one panel that gives you the error in that tactic and another that shows you what is going on at the focus. You don't have to keep going back and forth. It's a bit like having an #eval right after the code that you're writing
The text was updated successfully, but these errors were encountered:
It would help to do that to have the flag that you mentioned:
Probably the easiest way to support this concrete use case is to add a flag to the Lean 3 server so that it always loads the olean files, even if they're out of date.
Right now the info view always shows the error messages at the cursor position, but sometimes you want to monitor the error messages from somewhere else. It would be nice if you could tell the info view to track/focus/bikeshed one position and then continue to work somewhere else. You can already pause the info view, but then you unfortunately don't get any updates.
As requested by @cipher1024:
The text was updated successfully, but these errors were encountered: