##// END OF EJS Templates
Merge pull request #6920 from SylvainCorlay/serialize_date...
Merge pull request #6920 from SylvainCorlay/serialize_date Dates and Strings are JavaScript objects, and _pack_models behaves incorrectly in these cases.

File last commit:

r18489:2bdaec39
r18833:25c9cfb8 merge
Show More
terminado.js
39 lines | 1.2 KiB | application/javascript | JavascriptLexer
Thomas Kluyver
Terminal basically working...
r18481 define ([], function() {
function make_terminal(element, size, ws_url) {
var ws = new WebSocket(ws_url);
var term = new Terminal({
cols: size.cols,
rows: size.rows,
screenKeys: true,
Bussonnier Matthias
recompute dummy size dynamically + styling in css
r18489 useStyle: false
Thomas Kluyver
Terminal basically working...
r18481 });
ws.onopen = function(event) {
ws.send(JSON.stringify(["set_size", size.rows, size.cols,
window.innerHeight, window.innerWidth]));
term.on('data', function(data) {
ws.send(JSON.stringify(['stdin', data]));
});
term.on('title', function(title) {
document.title = title;
});
term.open(element);
ws.onmessage = function(event) {
json_msg = JSON.parse(event.data);
switch(json_msg[0]) {
case "stdout":
term.write(json_msg[1]);
break;
case "disconnect":
term.write("\r\n\r\n[CLOSED]\r\n");
break;
}
};
};
return {socket: ws, term: term};
}
return {make_terminal: make_terminal};
});