(widget)
| 2339 | } |
| 2340 | |
| 2341 | function widgetHeight(widget) { |
| 2342 | if (widget.height != null) { return widget.height } |
| 2343 | var cm = widget.doc.cm; |
| 2344 | if (!cm) { return 0 } |
| 2345 | if (!contains(document.body, widget.node)) { |
| 2346 | var parentStyle = "position: relative;"; |
| 2347 | if (widget.coverGutter) |
| 2348 | { parentStyle += "margin-left: -" + cm.display.gutters.offsetWidth + "px;"; } |
| 2349 | if (widget.noHScroll) |
| 2350 | { parentStyle += "width: " + cm.display.wrapper.clientWidth + "px;"; } |
| 2351 | removeChildrenAndAdd(cm.display.measure, elt("div", [widget.node], null, parentStyle)); |
| 2352 | } |
| 2353 | return widget.height = widget.node.parentNode.offsetHeight |
| 2354 | } |
| 2355 | |
| 2356 | // Return true when the given mouse event happened in a widget |
| 2357 | function eventInWidget(display, e) { |
no test coverage detected