From b123cd8a939566bd05df60ea6f7d0f65593a9293 Mon Sep 17 00:00:00 2001
From: Koen Lageveen <koen.lageveen@me.com>
Date: Thu, 5 Jan 2017 22:21:34 +0100
Subject: [PATCH] add line spacing control

---
 index.html | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/index.html b/index.html
index 1277e2a..76b8ba8 100755
--- a/index.html
+++ b/index.html
@@ -135,8 +135,9 @@
     width: 9em;
     margin-left: .5ex;
   }
-  #size {
-    width: 3em;
+  #size,
+  #spacing {
+    width: 4em;
     margin-left: .5ex;
   }
   pre,
@@ -225,7 +226,11 @@
     </p>
     <p>
       <label for="size">Size</label>
-      <input onchange="setSize()" type="number" id="size" value="14">
+      <input onchange="setSize()" type="number" id="size" value="14" min="1" max="32" step="1">
+    </p>
+    <p>
+      <label for="spacing">Spacing</label>
+      <input onchange="setSpacing()" type="number" id="spacing" value="1.2" min="1" max="2" step="0.1">
     </p>
     <p>
       <label for="aliasing">Anti-aliasing </label><input onchange="setAntialiasing()" type="checkbox" id="aliasing" checked>
@@ -334,6 +339,9 @@ function updateGutters(cm) {
     function setSize() {
       $(".CodeMirror").css({ fontSize: $("#size").val() + "px" });
     }
+    function setSpacing() {
+      $(".CodeMirror").css({ lineHeight: $("#spacing").val() });
+    }
     function setAntialiasing() {
       if ($("#aliasing").is(":checked")) {
         $(".CodeMirror").removeClass("no-smooth");