From 3c8bd225a70a38198bec491c88cc985e4dd57cde Mon Sep 17 00:00:00 2001
From: Koen Lageveen <koen.lageveen@me.com>
Date: Fri, 25 Nov 2016 11:48:00 +0100
Subject: [PATCH] fix #13 makes anti-aliasing optional

---
 index.html | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/index.html b/index.html
index 9832049..039c3fa 100755
--- a/index.html
+++ b/index.html
@@ -158,6 +158,10 @@
     min-height: 100%;
     text-rendering: optimizeLegibility;
   }
+  .CodeMirror.no-smooth {
+    font-smooth: never;
+    -webkit-font-smoothing : none;
+  }
   .CodeMirror .cm-atom { font-style: italic; }
   .CodeMirror-gutters {
     background: transparent;
@@ -221,7 +225,10 @@
     </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">
+    </p>
+    <p>
+      <label for="aliasing">Anti-aliasing </label><input onchange="setAntialiasing()" type="checkbox" id="aliasing" checked>
     </p>
 
     <dix id="font-info"></dix>
@@ -326,6 +333,13 @@ function updateGutters(cm) {
     function setSize() {
       $(".CodeMirror").css({ fontSize: $("#size").val() + "px" });
     }
+    function setAntialiasing() {
+      if ($("#aliasing").is(":checked")) {
+        $(".CodeMirror").removeClass("no-smooth");
+      } else {
+        $(".CodeMirror").addClass("no-smooth");
+      }
+    }
 
     $(document).ready(function(){
 
@@ -349,7 +363,7 @@ function updateGutters(cm) {
           } else {
             yearString = " (" + v.year + ")";
           }
-          
+
           $("#font-info").append(
             "<p class=\"" + v.alias + "\"> " + v.name +
             " - " + "<a href=\""+ v.website + "\" rel=\"external\">" + v.author + "</a>" + yearString +