Show More
@@ -2,6 +2,7 | |||
|
2 | 2 | // Distributed under the terms of the Modified BSD License. |
|
3 | 3 | |
|
4 | 4 | require([ |
|
5 | 'jquery', | |
|
5 | 6 | 'base/js/namespace', |
|
6 | 7 | 'base/js/utils', |
|
7 | 8 | 'base/js/page', |
@@ -14,6 +15,7 require([ | |||
|
14 | 15 | 'edit/js/notificationarea', |
|
15 | 16 | 'custom/custom', |
|
16 | 17 | ], function( |
|
18 | $, | |
|
17 | 19 | IPython, |
|
18 | 20 | utils, |
|
19 | 21 | page, |
@@ -75,4 +77,21 require([ | |||
|
75 | 77 | } |
|
76 | 78 | }; |
|
77 | 79 | |
|
80 | // Make sure the codemirror editor is sized appropriatley. | |
|
81 | var _handle_resize = function() { | |
|
82 | var header = $('#header'); | |
|
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); | |
|
92 | }; | |
|
93 | window.onresize = _handle_resize; | |
|
94 | ||
|
95 | // On document ready, resize codemirror. | |
|
96 | $(document).ready(_handle_resize); | |
|
78 | 97 | }); |
General Comments 0
You need to be logged in to leave comments.
Login now