##// END OF EJS Templates
Code for the less magic was unnecessarily reading the entire input file twice. Redundant read removed.
Code for the less magic was unnecessarily reading the entire input file twice. Redundant read removed.

File last commit:

r18489:2bdaec39
r19624:8d378a70
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};
});