Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improvements in IndexManager #1330

Merged
merged 1 commit into from
Jan 9, 2024
Merged

Improvements in IndexManager #1330

merged 1 commit into from
Jan 9, 2024

Conversation

spoenemann
Copy link
Contributor

  • Don't remove the reference to the AstNode
  • remove takes a single URI for consistency with other services
  • Renamed protected properties for more clarity

- Don't remove the reference to the AstNode
- `remove` takes a single URI for consistency with other services
@spoenemann spoenemann added this to the v3.0.0 milestone Jan 5, 2024
@spoenemann spoenemann requested a review from msujew January 5, 2024 11:29
@spoenemann
Copy link
Contributor Author

Some context about deleting the node property in AstNodeDescriptions:

  • We did that in the initial version of the IndexManager out of fear that such a reference could become outdated. But we're clearing the index anyway when a document needs to be reindexed, so it shouldn't be a problem in practice.
  • We also had in mind that one might want to unload a document from memory to reduce the overall memory consumption of a workspace. But we never tried that and so far we haven't seen the need for it, so we should leave that topic for later (seeing a real example where unloading is necessary). Enabling such unloading will require more work, anyway, because linking is currently synchronous, so we can't load documents during linking.
  • Serializing the index is also a topic, but that can be done with explicit IndexManager methods to be added in a future version.

@msujew msujew added the index Index/Workspace handling related label Jan 8, 2024
Copy link
Member

@msujew msujew left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great, looks good to me 👍

@spoenemann spoenemann merged commit fee533f into main Jan 9, 2024
5 checks passed
@spoenemann spoenemann deleted the index-manager-improvements branch January 9, 2024 08:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
index Index/Workspace handling related
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants