Inject requirejs in notebook and start using it.
Mainly because the behavior of Marked change when require is injected.
So only apply the modification needed for marked to behave.
closes#3391
For users who need to hide the scrollbars while zooming text in the meantime, you can add the following to your custom.css:
```css
.CodeMirror-scroll, .CodeMirror-wrap .CodeMirror-scroll {
overflow: scroll;
}
.CodeMirror-vscrollbar, .CodeMirror-scrollbar-filler, .CodeMirror-hscrollbar {
visibility: hidden;
}
```
switch default ws_url logic to js side
In some cases (proxies, #3305), the request object doesn't have the right information about the originating information. This changes the default behavior, so that ws_url is generally empty by default, which the javascript takes to mean 'the same as http'. This is simpler and should be more resilient than trying a guess on server-side.
also replaces unused websocket_host with websocket_url
Rather than specifying only the hostname, it makes much more sense to specify the whole protocol,host,port in a single go.
Use different treshold for (auto)scroll in output
Use different treshold for (auto)scroll in output
Allow, in particular to switch to scolling for longer input (or disable
it) by still keeping the possibility to manually toggle the output to
scroll.
cf jsdoc,
OutputArea.auto_scroll_threshold
and
OutputArea.minimum_scroll_threshold
OutputArea.auto_scroll_threshold < 0 will prevent auto_scroll from ever happening.
In some cases (proxies, #3305), the request object doesn't have the right information about the originating information. This changes the default behavior, so that `ws_url` is generally empty by default, which the javascript takes to mean 'the same as http'. This is simpler and should be more resilient than trying a guess on server-side.
always draw scrollbar margin, so that inappropriate scrollbars never overlap the last line.
To compensate for the extra space, the margin between the scrollbar and the last line is shrunk significantly.