Make terminal pretty

IPython/html/static/terminal/js/main.js

@@ -1,53 +1,53 b''
 // 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
     ){
     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() {
         height = window.innerHeight - header.offsetHeight;
-        width = window.innerWidth;
+        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();
     
     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]));
     };
 
 });

IPython/html/static/terminal/less/terminal.less

@@ -1,17 +1,26 b''
 .terminal {
   float: left;
   border: black solid 5px;
-  font-family: "DejaVu Sans Mono", "Liberation Mono", monospace;
+  font-family: monospace;
   font-size: 11px;
   color: white;
   background: black;
+  border-radius: 2px;
+  box-shadow: 0px 4px 11px 0px gray;
+  border: 0px;
+  padding: @code_padding;
+
+  &, dummy-screen {
+    line-height: @code_line_height;
+    font-size: @notebook_font_size;
+  }
 }
 
 .terminal-cursor {
   color: black;
   background: white;
 }
 
 #terminado-container {
-    margin: 8px;
+  padding-top: 20px;
 }

IPython/html/static/tree/css/override.css

@@ -1,7 +1,7 b''
 /*This file contains any manual css for this page that needs to override the global styles.
 This is only required when different pages style the same element differently. This is just
 a hack to deal with our current css styles and no new styling should be added in this file.*/
 
 #ipython-main-app {
-    margin: 28px auto 0px auto;
+    margin: 20px auto 0px auto;
 }

IPython/html/templates/terminal.html

@@ -1,57 +1,57 b''
 {% extends "page.html" %}
 
 {% block title %}{{page_title}}{% endblock %}
 
 {% block params %}
 
 data-base-url="{{base_url}}"
 data-ws-path="{{ws_path}}"
 
 {% endblock %}
 
 
 {% block site %}
 
-<div id="terminado-container"></div>
+<div id="terminado-container" class="container"></div>
 
 {% endblock %}
 
 {% block script %}
 
 <!-- Hack: this needs to be outside the display:none block, so we can measure
      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 -->
 <div style='position:absolute; left:-1000em'>
 <pre id="dummy-screen" style="border: solid 5px white;" class="terminal">0
 1
 2
 3
 4
 5
 6
 7
 8
 9
 0
 1
 2
 3
 4
 5
 6
 7
 8
 9
 0
 1
 2
 3
 <span id="dummy-screen-rows" style="">01234567890123456789012345678901234567890123456789012345678901234567890123456789</span>
 </pre>
 </div>
 
     {{super()}}
 
 <script src="{{ static_url("terminal/js/main.js") }}" type="text/javascript" charset="utf-8"></script>
 {% endblock %}