Make auto-numbering optional (disabled by default)

index.html

@@ -132,6 +132,8 @@ By <a target=_blank href="mailto:inexorabletash@gmail.com">Joshua Bell</a>
 
   <button id="show_paper" title="Echo all output to a &quot;print-out&quot;, so you can copy/paste">&#x1F4C3; Show output</button>
   <button id="hide_paper" title="Hide the &quot;print-out&quot;">&#x1F6AB; Hide output</button>
+
+  <input type="checkbox" id="autonum">Automatic-Numbering
   </form>
 
 </div>
@@ -154,6 +156,8 @@ By <a target=_blank href="mailto:inexorabletash@gmail.com">Joshua Bell</a>
   <li><a target="_blank" href="http://www.quitebasic.com/">Quite BASIC</a> - a similar project aimed at teaching programming
 </ul>
 
+<output style="font-family: monospace; font-size: small"></output>
+
 <div id="paper-spacer"></div>
 <div id="paper"></div>
 

index.js

@@ -114,7 +114,12 @@ window.addEventListener('DOMContentLoaded', function() {
 
     try {
       var source = getSource()
-      source = AutomaticNumbering(source)
+
+      $('output').innerText = ''
+      if ($('#autonum').checked) {
+        source = AutomaticNumbering(source)
+        $('output').innerText = source
+      }
 
       program = basic.compile(source);
     } catch (e) {