leanprover-community / lean4web

The Lean 4 web editor
https://live.lean-lang.org/
Apache License 2.0
52 stars 14 forks source link

Comment highlighting #16

Open joneugster opened 6 months ago

joneugster commented 6 months ago

Example, where the comment highlighting is off: demo

/- ## Wichtig:
- Bei der Verwendung von `calc` müssen alle `_` gleich weit eingerückt sein, sonst gibt es
  verwirrende Fehlermeldungen.
- Sehen Sie die Fehlermeldung `fail to show termination for ...`? Das weist darauf hin, dass
  Induktion verwendet wurde, die Argumente aber nicht strukturell kleiner sind. Eventuell wurden
  in Kombination mit `rw` auch Argumente nicht explizit angegeben? -/

For me, only the last line is marked green (i.e. the colour of comments in the theme)