Gandi-IDE / gandi-plugins

Gandi Plugins is a component library containing a suite of feature-enhancing plugins for Gandi-IDE.
GNU Lesser General Public License v3.0
10 stars 12 forks source link

Suggestions for Plugin Extension Manager #65

Open yuen619 opened 4 months ago

yuen619 commented 4 months ago

I found that the extension in the plugin extension manager ExtensionBox can be checked, so why not support batch selection and deletion? @fath11 image Then if the ExtensionBox is displayed and the extension is installed later, we need to reopen the ExtensionBox to see it. Can you optimize it?

fath11 commented 4 months ago

batch selection and deletion are already a thing. when you check multiple extensions, the delete button for those selected extensions will only appear on one of them and if you click it, it will delete all selected extensions.

as for the second issue, i forgot that it was there so i didnt fix it in my latest PR ;-;

yuen619 commented 4 months ago

Please handle the situation where the selected language extension in the editor does not correspond to i10n, and if the extension information cannot be obtained, an error message will appear. Add a try catch... may solve the problem