##// END OF EJS Templates
adjust appearance of cell toolbar select...
adjust appearance of cell toolbar select undo some of the bootstrap mixin sizing, which should help the appearance on Firefox on Linux.

File last commit:

r20023:982ae339 merge
r20413:38ea398e
Show More
main.js
63 lines | 2.1 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',
'services/config',
'terminal/js/terminado',
'custom/custom',
], function(
$,
termjs,
utils,
page,
configmod,
terminado
){
"use strict";
page = new page.Page();
var common_config = new configmod.ConfigSection('common',
{base_url: utils.get_body_data('baseUrl')});
common_config.load();
// 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();
utils.load_extensions_from_config(common_config);
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]));
};
});