From 21cdcb20b4703d9a61268eeb9d37cfb2142b1c9e Mon Sep 17 00:00:00 2001
From: Matt Pass <matt@mattpass.com>
Date: Sun, 17 Jun 2012 16:27:59 +0100
Subject: [PATCH] New tabWidth option

tabWidth option now shown in 'style' section
On change, this affects editor demo instance
---
 lib/settings-screen.php | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/lib/settings-screen.php b/lib/settings-screen.php
index 938537f..ff8619b 100644
--- a/lib/settings-screen.php
+++ b/lib/settings-screen.php
@@ -156,11 +156,19 @@ function findSequence(goal) {
 	}
 	return find(1,"1");
 }</textarea>
+<br>
+
+<span style="position: absolute; top: 520px">
+	tab width <span style="font-size: 10px; color: #888">chars</span><br>
+	<input type="text" name="tabWidth" id="tabWidth" style="width: 30px" onkeydown="showButton()" onkeyup="changeTabWidth()" value="<?php echo $tabWidth;?>">
+</span>
 
 <script>
 var editor = CodeMirror.fromTextArea(document.getElementById("code"), {
 	lineNumbers: true,
 	readOnly: "nocursor",
+	indentUnit: top.tabWidth,
+	tabSize: top.tabWidth,
 	theme: "<?php if ($theme=="default") {echo 'icecoder';} else {echo $theme;}; ?>"
 	});
 
@@ -171,6 +179,12 @@ function selectTheme() {
 	editor.setOption("theme", theme);
 }
 
+function changeTabWidth() {
+	var tabWidth = document.getElementById("tabWidth").value;
+	editor.setOption("indentUnit", tabWidth);
+	editor.setOption("tabSize", tabWidth);
+}
+
 var showButton = function() {
 	document.getElementById('updateButton').style.opacity = 1;
 }