##// END OF EJS Templates
setting an option to null sets the default in CodeMirror...
setting an option to null sets the default in CodeMirror matching the unset behavior in config

File last commit:

r18492:24e963dc
r19311:9c060bc5
Show More
main.js
53 lines | 1.8 KiB | application/javascript | JavascriptLexer
Thomas Kluyver
Basic infrastructure for terminal page
r18480 // Copyright (c) IPython Development Team.
// Distributed under the terms of the Modified BSD License.
require([
'jquery',
'termjs',
Thomas Kluyver
Terminal basically working...
r18481 'base/js/utils',
'base/js/page',
'terminal/js/terminado',
Thomas Kluyver
Basic infrastructure for terminal page
r18480 'custom/custom',
], function(
$,
Thomas Kluyver
Terminal basically working...
r18481 termjs,
utils,
page,
terminado
){
page = new page.Page();
// Test size: 25x80
Bussonnier Matthias
recompute dummy size dynamically + styling in css
r18489 var termRowHeight = function(){ return 1.00 * $("#dummy-screen")[0].offsetHeight / 25;};
Thomas Kluyver
Add comment explaining 1.02 factor
r18492 // 1.02 here arrived at by trial and error to make the spacing look right
Bussonnier Matthias
recompute dummy size dynamically + styling in css
r18489 var termColWidth = function() { return 1.02 * $("#dummy-screen-rows")[0].offsetWidth / 80;};
Thomas Kluyver
Terminal basically working...
r18481
var base_url = utils.get_body_data('baseUrl');
Thomas Kluyver
Multiple terminals and conditional initialisation
r18482 var ws_path = utils.get_body_data('wsPath');
Thomas Kluyver
Terminal basically working...
r18481 var ws_url = location.protocol.replace('http', 'ws') + "//" + location.host
Thomas Kluyver
Multiple terminals and conditional initialisation
r18482 + base_url + ws_path;
Thomas Kluyver
Terminal basically working...
r18481
var header = $("#header")[0]
function calculate_size() {
height = window.innerHeight - header.offsetHeight;
width = window.innerWidth;
Bussonnier Matthias
recompute dummy size dynamically + styling in css
r18489 var rows = Math.min(1000, Math.max(20, Math.floor(height/termRowHeight())-1));
var cols = Math.min(1000, Math.max(40, Math.floor(width/termColWidth())-1));
console.log("resize to :", rows , 'rows by ', cols, 'columns');
Thomas Kluyver
Terminal basically working...
r18481 return {rows: rows, cols: cols};
}
page.show_header();
size = calculate_size();
var terminal = terminado.make_terminal($("#terminado-container")[0], size, ws_url);
page.show_site();
window.onresize = function() {
var geom = calculate_size();
terminal.term.resize(geom.cols, geom.rows);
terminal.socket.send(JSON.stringify(["set_size", geom.rows, geom.cols,
window.innerHeight, window.innerWidth]));
};
Thomas Kluyver
Basic infrastructure for terminal page
r18480
});