##// END OF EJS Templates
fix end_space size...
fix end_space size closes #7409 Mostly a symptome of too many nested div that do different things. don't try to both have an end space inside and outside the 'document' area. And don't try to also get the things to be 100viewport height by hacking around and make them smaller;

File last commit:

r19739:7c74a0d3
r19872:b3fa9de5
Show More
terminado.js
40 lines | 1.3 KiB | application/javascript | JavascriptLexer
Thomas Kluyver
Terminal basically working...
r18481 define ([], function() {
Matthias Bussonnier
Some code cleanup in javascript and python...
r19739 "use strict";
Thomas Kluyver
Terminal basically working...
r18481 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) {
Matthias Bussonnier
Some code cleanup in javascript and python...
r19739 var json_msg = JSON.parse(event.data);
Thomas Kluyver
Terminal basically working...
r18481 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};
});