##// 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
main.js
54 lines | 1.8 KiB | application/javascript | JavascriptLexer
// Copyright (c) IPython Development Team.
// Distributed under the terms of the Modified BSD License.
require([
'jquery',
'termjs',
'base/js/utils',
'base/js/page',
'terminal/js/terminado',
'custom/custom',
], function(
$,
termjs,
utils,
page,
terminado
){
"use strict";
page = new page.Page();
// Test size: 25x80
var termRowHeight = function(){ return 1.00 * $("#dummy-screen")[0].offsetHeight / 25;};
// 1.02 here arrived at by trial and error to make the spacing look right
var termColWidth = function() { return 1.02 * $("#dummy-screen-rows")[0].offsetWidth / 80;};
var base_url = utils.get_body_data('baseUrl');
var ws_path = utils.get_body_data('wsPath');
var ws_url = location.protocol.replace('http', 'ws') + "//" + location.host
+ base_url + ws_path;
var header = $("#header")[0]
function calculate_size() {
var height = window.innerHeight - header.offsetHeight;
var width = $('#terminado-container').width();
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');
return {rows: rows, cols: cols};
}
page.show_header();
var 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]));
};
});