search

leanprover / leanprover.github.io

www
https://lean-lang.org/
15 stars 24 forks source link

mouse-hover type information breaks on pane resize #61

Open picrin opened 7 years ago

picrin commented 7 years ago

The new version of the tutorial includes type information on mouse hover. This is a great feature, but there is a bug, which manifests itself when one resizes the horizontal pane bar:

paneresize

The issue is that the mouse hover information isn't available in the new position of the proof term, instead, it is available at a shifted location, at the original position of the term before pane resize.

The issue is present on all 3 browsers I've tested:

  1. Opera
  2. Firefox
  3. Chrome
Kha commented 7 years ago

Thank you for the report. We're using an Ace Editor API to translate screen coordinates to text positions, so that's not something we can easily fix ourselves (though it might have been fixed upstream in the mean time). Anyway, we're looking into replacing Ace with Monaco, which should hopefully fix this problem too.