recompute dummy size dynamically + styling in css

Bussonnier Matthias 12 years ago committed by Thomas Kluyver
parent 1dcf9c325d
commit 1b200e5504

@ -0,0 +1,13 @@
.terminal {
float: left;
border: black solid 5px;
font-family: "DejaVu Sans Mono", "Liberation Mono", monospace;
font-size: 11px;
color: white;
background: black;
}
.terminal-cursor {
color: black;
background: white;
}

@ -26,4 +26,4 @@
// notebook
@import "../notebook/less/style.less";
@import "../notebook/less/terminal.less";

@ -10483,4 +10483,16 @@ span#autosave_status {
-ms-transform: rotate(45deg);
-o-transform: rotate(45deg);
}
.terminal {
float: left;
border: black solid 5px;
font-family: "DejaVu Sans Mono", "Liberation Mono", monospace;
font-size: 11px;
color: white;
background: black;
}
.terminal-cursor {
color: black;
background: white;
}
/*# sourceMappingURL=../style/style.min.css.map */

@ -17,9 +17,8 @@ require([
){
page = new page.Page();
// Test size: 25x80
var termRowHeight = 1.00 * $("#dummy-screen")[0].offsetHeight / 25;
var termColWidth = 1.02 * $("#dummy-screen-rows")[0].offsetWidth / 80;
$("#dummy-screen").hide();
var termRowHeight = function(){ return 1.00 * $("#dummy-screen")[0].offsetHeight / 25;};
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');
@ -30,10 +29,9 @@ require([
function calculate_size() {
height = window.innerHeight - header.offsetHeight;
width = window.innerWidth;
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:", termRowHeight, termColWidth, height, width,
rows, cols);
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};
}

@ -5,7 +5,7 @@ define ([], function() {
cols: size.cols,
rows: size.rows,
screenKeys: true,
useStyle: true
useStyle: false
});
ws.onopen = function(event) {
ws.send(JSON.stringify(["set_size", size.rows, size.cols,

@ -27,7 +27,8 @@ data-ws-path="{{ws_path}}"
its size in JS in setting up the page. It is still invisible. Putting in
the script block gets it outside the initially undisplayed region. -->
<!-- test size: 25x80 -->
<pre id="dummy-screen" style="visibility:hidden; border: white solid 5px; font-family: &quot;DejaVu Sans Mono&quot;, &quot;Liberation Mono&quot;, monospace; font-size: 11px;">0
<div style='position:absolute; left:-1000em'>
<pre id="dummy-screen" style="" class='terminal' style'border: solid 5px white'>0
1
2
3
@ -51,8 +52,9 @@ data-ws-path="{{ws_path}}"
1
2
3
<span id="dummy-screen-rows" style="visibility:hidden;">01234567890123456789012345678901234567890123456789012345678901234567890123456789</span>
<span id="dummy-screen-rows" style="">01234567890123456789012345678901234567890123456789012345678901234567890123456789</span>
</pre>
</div>
{{super()}}

Loading…
Cancel
Save