Fix tooltip display in Google Chrome

This commit is contained in:
Arne Keller 2021-07-27 13:08:38 +02:00
parent c9e8fc7568
commit 6df7f0f443

View File

@ -81,7 +81,8 @@ class MathjaxProofTree extends MathjaxAdapter {
margin: 0 !important;\ margin: 0 !important;\
}\ }\
.typicalc-type, g[semantics='bspr_prooflabel:left'] {\ .typicalc-type, g[semantics='bspr_prooflabel:left'] {\
stroke: transparent; stroke-width: 600px; pointer-events: all;\ /* cross-browser-compatibility: Chrome does not support the stroke trick, but instead bounding-box (which is not supported by Firefox..) */\
stroke: transparent; stroke-width: 600px; pointer-events: all; pointer-events: bounding-box;\
}\ }\
#typicalc-definition-abs, #typicalc-definition-abs-let, #typicalc-definition-app,\ #typicalc-definition-abs, #typicalc-definition-abs-let, #typicalc-definition-app,\
#typicalc-definition-const, #typicalc-definition-var, #typicalc-definition-var-let, #typicalc-definition-let {\ #typicalc-definition-const, #typicalc-definition-var, #typicalc-definition-var-let, #typicalc-definition-let {\