leanprover / verso

Lean documentation authoring tool
Apache License 2.0
125 stars 14 forks source link

Consistent use of CSS variables for themeing #216

Open david-christiansen opened 1 month ago

david-christiansen commented 1 month ago

All genres that output highlighted Lean code should use a consistent set of CSS variables to control all of the following:

  1. Font families, weights, colors, and styles (italic/upright) for each token that Verso emits
  2. Colors used for information, warning, and error indications
  3. Background colors for inline code, block code, hovers, "what you're pointing at indicators", and proof states

There should also be a guide as to what the "safe" properties are to set in local CSS (e.g. for controlling overflow, indentation, and the like for rendered code)

Right now it's a bit chaotic, leading to inconsistencies.