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
Select any piece of text and use Create new scratch file from selection intention to create a separate .ard-file outside of Arend project (this is a standard Intellij feature)
Currently every such scratch displays message that it is outside of sources folder.
A reasonable implementation, IMO is to link the created scratch to the project where it was created and use project's src directory as (implicit, non-configurable) src folder for the scratch.
Modify default behavior of this intention in such a manner that it would create \import-header in the destination scratch for all links mentioned in the migrated piece of text.
The text was updated successfully, but these errors were encountered:
Select any piece of text and use
Create new scratch file from selection
intention to create a separate .ard-file outside of Arend project (this is a standard Intellij feature)Currently every such scratch displays message that it is outside of sources folder.
The text was updated successfully, but these errors were encountered: