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

Highlight all occurrences when mouse hovers a symbol in generated HTML #4535

Merged
merged 8 commits into from Mar 25, 2020

Conversation

ice1000
Copy link
Member

@ice1000 ice1000 commented Mar 24, 2020

See https://twitter.com/i/status/1241631880388194304

This idea is stolen from Haddock.

Tests are on the way.

@ice1000 ice1000 self-assigned this Mar 24, 2020
hint-man[bot]
hint-man bot approved these changes Mar 24, 2020
Copy link
Contributor

@hint-man hint-man bot left a comment

There is no place for me here... I will choose the truth I like.

@ice1000
Copy link
Member Author

ice1000 commented Mar 24, 2020

Rebased on master

@ice1000 ice1000 requested a review from vlopezj Mar 24, 2020
src/full/Agda/Interaction/Highlighting/HTML.hs Outdated Show resolved Hide resolved
src/full/Agda/Interaction/Highlighting/HTML.hs Outdated Show resolved Hide resolved
@@ -0,0 +1,28 @@
var highlight = function (on) {
Copy link
Contributor

@vlopezj vlopezj Mar 24, 2020

Choose a reason for hiding this comment

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

Add copyright notice from Haddock project. Check that the file indeed comes from there.

Copy link
Member Author

@ice1000 ice1000 Mar 24, 2020

Choose a reason for hiding this comment

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

I modified it a little, not sure how does that affect the copyright though.

Copy link
Member Author

@ice1000 ice1000 Mar 24, 2020

Choose a reason for hiding this comment

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

Added the copyright line and a link to the license

@vlopezj
Copy link
Contributor

vlopezj commented Mar 24, 2020

Thanks for the pull request. I don't know how useful this could be for me personally, but if Haddock has it, then we should have it too 👍.
I haven't tested it on my computer, but the code looks OK. I wrote some minor things you should fix.

I also see you changed a lot of the spacing in the CommandLineOptions and defaultOptions. I think it's better to leave it as it was (even if it's looks ugly) instead of adding more changes to the project history. If it's something minor and the code is related to the rest of the pull request, then it's OK to do cosmetic fixes (like the one you did in the "--html-highlight" documentation).

@nad
Copy link
Contributor

nad commented Mar 24, 2020

More highlighting is not necessarily better. Could you explain the rationale for this feature? How should it be used?

I can imagine that it might be nice to see every instance of a given bound variable. However, in the linked example, when you hover over the pattern variable b the corresponding variable in the body of the function is not highlighted.

I don't see the point of seeing every instance of (say) highlighted at the same time. When you scroll a page and the mouse pointer is over it various names might light up, and I can imagine that this would be distracting.

I also wondered about the performance of this feature, and apparently "this feature may cause browser performance problem".

@ice1000
Copy link
Member Author

ice1000 commented Mar 24, 2020

Could you explain the rationale for this feature?

This can be helpful for understanding complicated scoping, such as variable bindings, module-related stuffs and overloaded projections/constructors.

I can imagine that it might be nice to see every instance of a given bound variable. However, in the linked example, when you hover over the pattern variable b the corresponding variable in the body of the function is not highlighted.

Then it's a bug of the href generator.

I don't see the point of seeing every instance of (say) ∘ highlighted at the same time. When you scroll a page and the mouse pointer is over it various names might light up, and I can imagine that this would be distracting.

We can also say "this is how you discover new features".

I also wondered about the performance of this feature, and apparently "this feature may cause browser performance problem".

Again in the document, this feature is disabled by default, so I don't think we're bringing burden.

@ice1000
Copy link
Member Author

ice1000 commented Mar 24, 2020

I also see you changed a lot of the spacing in the CommandLineOptions and defaultOptions. I think it's better to leave it as it was (even if it's looks ugly) instead of adding more changes to the project history. If it's something minor and the code is related to the rest of the pull request, then it's OK to do cosmetic fixes (like the one you did in the "--html-highlight" documentation).

This is because I added a really long option and I don't know how to shorten it. So I need to add a line which doesn't align the others. I feel like there will be someone doing this anyway, so I just did it by the way. Now all of these options are aligned in a very safe position that is less likely to be changed in the future, so I'm gonna keep it for now. I am not strong on this though, feel free to "ask me" to remove them. I'll revert the changes.

@ice1000 ice1000 requested a review from vlopezj Mar 24, 2020
@ice1000
Copy link
Member Author

ice1000 commented Mar 24, 2020

CI passes

@ice1000 ice1000 merged commit f5ddad5 into agda:master Mar 25, 2020
10 checks passed
@ice1000 ice1000 deleted the ! branch Mar 25, 2020
@ice1000
Copy link
Member Author

ice1000 commented Mar 25, 2020

Since all comments are addressed, I'm gonna take this in. I'm still open to further changes, just reply to this thread.

@andreasabel
Copy link
Member

andreasabel commented Mar 27, 2020

Ideally, this feature would not switched by the generator of a html page, but the viewer.

However, I suppose, this would require a more sophisticated Agda viewer implemented in JS, with an options menu, and cookies to store the choice...

@nad
Copy link
Contributor

nad commented Mar 27, 2020

Since all comments are addressed, I'm gonna take this in.

I disagree with your claim.

Again in the document, this feature is disabled by default, so I don't think we're bringing burden.

As I wrote above I don't see the point of this feature. Perhaps there is no runtime cost to users who do not use it, but there could still be a maintenance cost for developers.

This can be helpful for understanding complicated scoping, such as variable bindings, module-related stuffs and overloaded projections/constructors.

Can you give a specific example of how you intend to use the feature?

@ice1000
Copy link
Member Author

ice1000 commented Mar 27, 2020

I disagree with your claim.

I was talking about the review comments, sorry for the ambiguity.

Perhaps there is no runtime cost to users who do not use it, but there could still be a maintenance cost for developers.

I can take care of future changes related to this feature.

I'd like to call this feature "show usages", because it shows usages (in the current web page) for definitions.
You can't show usages (in any sense) before.

@ice1000
Copy link
Member Author

ice1000 commented Mar 27, 2020

It also helps distinguishing similar names. If unfortunately your computer cannot display some pure-unicode symbols and you don't want to click on each "cannot be displayed" symbols to see their definitions, this feature may help you.

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

Successfully merging this pull request may close these issues.

None yet

4 participants