When using the HTML display, the upper right portion shows a line for each level of nesting that corresponds to the element currently under the mouse. The vertical size of this header nesting varies based on the nesting level. Unfortunately, this can frequently cause the display to hop with no mouse movement. Consider:
def Outer =
block
part1 = Inner
part2 = Inner
def Inner =
block
tag1 = Name
tag2 = Name
def Name =
block
name = Many 8 $any
If I move my mouse to the first Inner, the header shows 2 lines: Outer + Inner. If I then move my mouse to the name field of the first Inner in the first Outer, the top right now changes to 3 lines: Outer + Inner + Name. However, that change to 3 lines means that my mouse is no longer over the name field which just got pushed down. So now the header has to change back to 2 lines: Outer + Inner. Howevever, now my mouse (without me moving it) is now over the name field again, so the header has to change back to 3 lines: Outer + Inner + Name, but that means that my mouse is no longer over the name field ... and the display continues to flicker back and forth.
Fixing the vertical size of the header region div and auto-scrolling to the bottom would be one way to fix this. There may be other ways.
When using the HTML display, the upper right portion shows a line for each level of nesting that corresponds to the element currently under the mouse. The vertical size of this header nesting varies based on the nesting level. Unfortunately, this can frequently cause the display to hop with no mouse movement. Consider:
If I move my mouse to the first Inner, the header shows 2 lines: Outer + Inner. If I then move my mouse to the
namefield of the firstInnerin the firstOuter, the top right now changes to 3 lines: Outer + Inner + Name. However, that change to 3 lines means that my mouse is no longer over thenamefield which just got pushed down. So now the header has to change back to 2 lines: Outer + Inner. Howevever, now my mouse (without me moving it) is now over thenamefield again, so the header has to change back to 3 lines: Outer + Inner + Name, but that means that my mouse is no longer over thenamefield ... and the display continues to flicker back and forth.Fixing the vertical size of the header region div and auto-scrolling to the bottom would be one way to fix this. There may be other ways.