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
Thanks for the request @domaspoliakas! Thinking about and playing around with this a bit we hit on a snag right away that you can't really save a scratch buffer which means you can't get the didSave notification sent to the server to both get diagnostics and results of the worksheet. You can try to hack around this but it might be messy.
Another idea would be to just create either a tmp file or like a .metals/scratch.worksheet.sc. Then a quick worksheet command could always just open that up if it exists or create a new one.
Describe the feature
Worksheets that use a scratch buffer instead of being saved on disk.
Potential ways to implement?
From discord:
Additional context
N/A
Search terms
Worksheets worksheet scratch buffer disk
The text was updated successfully, but these errors were encountered: