Show More
@@ -80,8 +80,15 b' require([' | |||
|
80 | 80 | // Make sure the codemirror editor is sized appropriatley. |
|
81 | 81 | var _handle_resize = function() { |
|
82 | 82 | var header = $('#header'); |
|
83 | var padding = header.outerHeight(true) - header.innerHeight(); | |
|
84 | $('div.CodeMirror').height(window.innerHeight - header.height() - 2*padding); | |
|
83 | ||
|
84 | // The header doesn't have a margin or padding above it. Calculate | |
|
85 | // the lower margin&padding by subtracting the innerHeight from the | |
|
86 | // outerHeight. | |
|
87 | var header_margin_bottom = header.outerHeight(true) - header.innerHeight(); | |
|
88 | ||
|
89 | // When scaling CodeMirror, subtract the header lower margin from the | |
|
90 | // height twice. Once for top padding and once for bottom padding. | |
|
91 | $('div.CodeMirror').height(window.innerHeight - header.height() - 2*header_margin_bottom); | |
|
85 | 92 | }; |
|
86 | 93 | window.onresize = _handle_resize; |
|
87 | 94 |
General Comments 0
You need to be logged in to leave comments.
Login now