// ----------------- JPEG
// resize the window...
// window.document.documentElement.scrollHeight
- var scroll_height = (int) _this.view.get_dom_document().document_element.scroll_height;
+ var scroll_height = (int) _this.view.el.get_dom_document().document_element.scroll_height;
if (scroll_height> 1024) {
- _this.scrolled_window.set_size_request(1200, Int.min(scroll_height, 6000));
+ _this.scrolled_window.el.set_size_request(1200, Int.min(scroll_height, 6000));
print("Resize to %d\n", scroll_height);
}