Add config option to control whether tooltips are displayed for linter decorations #6

Closed

timdown wants to merge 5 commits from lint-decoration-tooltip-config-option into main

timdown commented

2022-04-25 16:55:48 +02:00

(Migrated from github.com)

In some circumstances, it would be useful to suppress tooltips for linter decorations within the editor content and rely instead on tooltips for gutter markers. This adds a configuration option to do that.

marijnh (Migrated from github.com) reviewed

2022-04-26 08:21:26 +02:00

src/lint.ts

Is there a reason to use a separate facet here, rather than including this option in lintSource (possibly renaming it to lintConfig)?

Is there a reason to use a separate facet here, rather than including this option in `lintSource` (possibly renaming it to `lintConfig`)?

timdown (Migrated from github.com) reviewed

2022-04-26 10:53:46 +02:00

src/lint.ts

I think it would be fine to combine this one option into lintSource if you'd prefer that, and looking at it now, I agree that it doesn't seem correct to have delay in both facets.

For context, there are two things we're trying to achieve:

we'd like to suppress all tooltips for all linter markers in the editor content but keep the gutter tooltips
for errors, we want markers in both the gutter and editor content but for warnings we just want gutter markers.

We can achieve the first with this showTooltips option and we can achieve the second simply but somewhat hackily by styling warning markers in the content to be invisible.

I extracted this PR from a larger set of new config options I was experimenting with that enable and disable decorations both at the severity level and independently in the gutter and editor content, which seems to me like a different concern to a list of sources of diagnostics.

I think it would be fine to combine this one option into `lintSource` if you'd prefer that, and looking at it now, I agree that it doesn't seem correct to have `delay` in both facets. For context, there are two things we're trying to achieve: 1. we'd like to suppress all tooltips for all linter markers in the editor content but keep the gutter tooltips 2. for errors, we want markers in both the gutter and editor content but for warnings we just want gutter markers. We can achieve the first with this `showTooltips` option and we can achieve the second simply but somewhat hackily by styling warning markers in the content to be invisible. I extracted this PR from a larger set of new config options I was experimenting with that enable and disable decorations both at the severity level and independently in the gutter and editor content, which seems to me like a different concern to a list of sources of diagnostics.

marijnh (Migrated from github.com) reviewed

2022-04-26 16:54:20 +02:00

src/lint.ts

How about allowing showTooltips to be either a boolean or a (tooltip: Tooltip, type: "gutter" | "code") => boolean predicate? Hiding these with CSS seems a bit wasteful.

How about allowing `showTooltips` to be either a boolean or a `(tooltip: Tooltip, type: "gutter" | "code") => boolean` predicate? Hiding these with CSS seems a bit wasteful.

marijnh (Migrated from github.com) reviewed

2022-04-26 18:04:44 +02:00

src/lint.ts

(Or actually the boolean part wouldn't make much sense, just a predicate would work well I suppose.)

timdown (Migrated from github.com) reviewed

2022-04-27 12:14:08 +02:00

src/lint.ts

That would work for us for tooltips. I think having the array of Diagnostics available to the predicate would also be helpful: it would allow hiding of the tooltip based on the severity of the diagnostics. It could go further by instead having a diagnostics filter function; I can imagine we might decide we'd want to filter out warnings from the tooltip if there the were errors as well. Something like (diagnostics: Diagnostic[], type: "gutter" | "code") => Diagnostic[], called tooltipDiagnosticFilter maybe?

A similar showMarkers predicate for markers would be ideal and remove the need to hide warning markers via CSS.

That would work for us for tooltips. I think having the array of `Diagnostic`s available to the predicate would also be helpful: it would allow hiding of the tooltip based on the severity of the diagnostics. It could go further by instead having a diagnostics filter function; I can imagine we might decide we'd want to filter out warnings from the tooltip if there the were errors as well. Something like `(diagnostics: Diagnostic[], type: "gutter" | "code") => Diagnostic[]`, called `tooltipDiagnosticFilter` maybe? A similar `showMarkers` predicate for markers would be ideal and remove the need to hide warning markers via CSS.

marijnh (Migrated from github.com) reviewed

2022-04-27 13:04:19 +02:00

src/lint.ts

Oh, right, my Tooltip argument there was nonsense, we want to pass diagnostics, not tooltips. Your type sounds good.

Oh, right, my `Tooltip` argument there was nonsense, we want to pass diagnostics, not tooltips. Your type sounds good.

timdown (Migrated from github.com) reviewed

2022-04-29 12:56:08 +02:00

src/lint.ts

I've implemented tooltipDiagnosticFilter and markerDiagnosticFilter config options. I've also merged the lint source and config facets, but I'm really not convinced by how I've implemented that part. I wasn't sure what the best way to combine values would be, given that sources should be additive and configs should be merged.

One other contextual thing I've forgotten to mention that is that the "we" above is Overleaf, who I now work for.

I've implemented `tooltipDiagnosticFilter` and `markerDiagnosticFilter` config options. I've also merged the lint source and config facets, but I'm really not convinced by how I've implemented that part. I wasn't sure what the best way to combine values would be, given that sources should be additive and configs should be merged. One other contextual thing I've forgotten to mention that is that the "we" above is Overleaf, who I now work for.

marijnh commented

2022-04-29 16:32:59 +02:00

(Migrated from github.com)

Reading the patch, I realized it might be clearer to pass separate filters options the config to linter and the config to lintGutter, and do away with the second argument to the filters. Also, I'd prefer shorter option names like markerFilter and tooltipFilter.

Reading the patch, I realized it might be clearer to pass separate filters options the config to `linter` and the config to `lintGutter`, and do away with the second argument to the filters. Also, I'd prefer shorter option names like `markerFilter` and `tooltipFilter`.

timdown commented

2022-04-29 18:09:48 +02:00

(Migrated from github.com)

Done. I agree that having separate filter options in the gutter config seems better.

marijnh commented

2022-05-02 08:29:06 +02:00

(Migrated from github.com)

Thanks! I've merged this as 79aee39555

Thanks! I've merged this as 79aee39555d851f473a9d3995ecd94fe7ca93dc8

Pull request closed

This pull request cannot be reopened because the branch was deleted.

No reviewers

No labels

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

codemirror/lint!6

No description provided.

Rows
Columns