make line padding adjustable (fixes #141)

terminus-terminal/src/components/terminalTab.component.ts

@@ -214,6 +214,13 @@ export class TerminalTabComponent extends BaseTabComponent {
                 return ret
             }
         }
+
+        const _measureCharacterSize = hterm.scrollPort_.measureCharacterSize.bind(hterm.scrollPort_)
+        hterm.scrollPort_.measureCharacterSize = () => {
+            let size = _measureCharacterSize()
+            size.height += this.config.store.terminal.linePadding
+            return size
+        }
     }
 
     attachIOHandlers (io: any) {

terminus-terminal/src/config.ts

@@ -4,6 +4,7 @@ export class TerminalConfigProvider extends ConfigProvider {
     defaults = {
         terminal: {
             fontSize: 14,
+            linePadding: 0,
             bell: 'off',
             bracketedPaste: false,
             background: 'theme',

terminus-terminal/src/hterm.userCSS.scss

@@ -10,6 +10,11 @@ x-screen {
     transition: 0.125s ease background;
 }
 
+x-row > span {
+    display: inline-block;
+    height: inherit;
+}
+
 @font-face {
     font-family: "monospace-fallback";
     src: url(fonts/Meslo.otf) format("opentype");