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

Add the plugin manager #7198

Merged
merged 3 commits into from
Dec 27, 2023
Merged

Add the plugin manager #7198

merged 3 commits into from
Dec 27, 2023

Conversation

jtpio
Copy link
Member

@jtpio jtpio commented Dec 21, 2023

Fixes #7097

  • Add @jupyterlab/pluginmanager-extension
  • Populate availablePlugins
  • Default to opening the widget in the left area
  • UI test?

@jtpio jtpio added this to the 7.1 milestone Dec 21, 2023
Copy link
Contributor

Binder 👈 Launch a Binder on branch jtpio/notebook/plugin-manager

@jtpio
Copy link
Member Author

jtpio commented Dec 22, 2023

Basic functionality seems to be working, with the plugin manager widget added to the left area and available on all notebook pages, since each notebook page has a different set of plugins:

notebook-pluginmanager.webm

@jtpio
Copy link
Member Author

jtpio commented Dec 22, 2023

With the current state, this would make the plugin manager widget a bit hidden and difficult to find. But maybe that's fine for now, since this can be considered a more advanced feature that would likely not be used by many Notebook users.

@jtpio jtpio marked this pull request as ready for review December 27, 2023 09:16
@jtpio
Copy link
Member Author

jtpio commented Dec 27, 2023

Getting this one so the functionality is available and can be iterated on in follow-up PRs.

@jtpio jtpio closed this Dec 27, 2023
@jtpio jtpio reopened this Dec 27, 2023
@jtpio jtpio merged commit 251e0e3 into jupyter:main Dec 27, 2023
61 checks passed
@jtpio jtpio deleted the plugin-manager branch December 27, 2023 09:33
@jtpio
Copy link
Member Author

jtpio commented Dec 27, 2023

Opened #7200 to track follow-up improvements.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Add the plugin manager extension
1 participant