Skip to content

Conversation

fredrik-bakke
Copy link
Collaborator

@fredrik-bakke fredrik-bakke commented Apr 25, 2025

Summary

  • Add dotted underlines under links that are adjacent making it possible to tell them apart, e.g.:
    image
    image
    The styling does not apply to code, or concept paragraph symbols, and it only applies to links with another link directly adjacent to it.
  • Don't display underline on hover in code. New:
    image
    vs old:
    image
  • Add external link indicator, e.g., the symbol after the first link below image

@fredrik-bakke fredrik-bakke added enhancement New feature or request website labels Apr 25, 2025
Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

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

I don't think adding the dotted underlines with JavaScript is a good move. It adds overhead on every page load, linear in the number of links (which is most of the content), and the resulting separation is still pretty easy to miss IMO. The more scalable solution would be to try and phrase things in such a way that you don't get runs of links (like the original |transitive| |well-founded relation| got reworded into |relation| that is |transitive| and |well-founded|).

@fredrik-bakke
Copy link
Collaborator Author

I don't think adding the dotted underlines with JavaScript is a good move. It adds overhead on every page load, linear in the number of links (which is most of the content), and the resulting separation is still pretty easy to miss IMO. The more scalable solution would be to try and phrase things in such a way that you don't get runs of links (like the original |transitive| |well-founded relation| got reworded into |relation| that is |transitive| and |well-founded|).

I have to disagree that it's not an improvement, but let's not fight about this now. The issue is very minor anyways, and I've reverted the relevant changes.

Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

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

Sorry, this one slipped through the cracks

fredrik-bakke and others added 4 commits August 18, 2025 22:23
There's really only Firefox 115 ESR which doesn't support :has, and it
itself is only supported on Windows 8 and macOS Mojave, until March 2026
Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

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

I'm happy with these changes, but let me know if you manage to reproduce the external link indicators showing up in your Firefox. Otherwise feel free to merge it

@fredrik-bakke
Copy link
Collaborator Author

I'm happy with these changes, but let me know if you manage to reproduce the external link indicators showing up in your Firefox. Otherwise feel free to merge it

I'll test it right now

@fredrik-bakke
Copy link
Collaborator Author

I'll test it right now

Nope, they're gone!

@fredrik-bakke fredrik-bakke merged commit 4a07386 into UniMath:master Oct 3, 2025
3 checks passed
@fredrik-bakke fredrik-bakke deleted the link-style branch October 3, 2025 14:59
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Oct 3, 2025
## Summary

- [X] ~Add dotted underlines under links that are adjacent making it
possible to tell them apart, e.g.:

![image](https://github.com/user-attachments/assets/1a8c3c99-acaa-4bda-9f7f-da9890f09423)

![image](https://github.com/user-attachments/assets/07f83e2d-0031-419f-994e-5997d87ddcc4)
The styling does not apply to code, or concept paragraph symbols, and it
only applies to links with another link directly adjacent to it.~
- [X] Don't display underline on hover in code. New: 

![image](https://github.com/user-attachments/assets/890b0200-4073-4e13-9260-af4cb3a8a6c6)
  vs old: 

![image](https://github.com/user-attachments/assets/c90227d7-4461-4b4d-9fa0-883d3c086b73)
- [X] Add external link indicator, e.g., the symbol after the first link
below <img width="506" height="257" alt="image"
src="https://github.com/user-attachments/assets/6a19d2ca-c99e-44a8-be30-245fc1159589"
/>

---------

Co-authored-by: VojtechStep <vojtechstepancik@outlook.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request website

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants