From 666f01179cccc100b568370f9d65bada72158464 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gast=C3=B3n=20Kleiman?= <gaston.kleiman@gmail.com>
Date: Sat, 19 Feb 2011 06:18:12 +0800
Subject: [PATCH] Add 'Use Soft Tabs' option to bookmarklet settings.

This is needed to edit Python code and Makefiles.
---
 build_support/boot_textarea.js | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/build_support/boot_textarea.js b/build_support/boot_textarea.js
index cec2d976..4d7e7f52 100644
--- a/build_support/boot_textarea.js
+++ b/build_support/boot_textarea.js
@@ -366,6 +366,10 @@ function setupApi(editor, editorDiv, settingDiv, ace, options) {
                     }
                 break;
 
+                case "useSoftTabs":
+                    session.setUseSoftTabs(toBool(value));
+                break;
+
                 case "showPrintMargin":
                     renderer.setShowPrintMargin(toBool(value));
                 break
@@ -402,7 +406,8 @@ function setupSettingPanel(settingDiv, settingOpener, api, options) {
         theme:           "Theme:",
         fontSize:        "Font Size:",
         softWrap:        "Soft Wrap:",
-        showPrintMargin: "Show Print Margin:"
+        showPrintMargin: "Show Print Margin:",
+        useSoftTabs:     "Use Soft Tabs:"
     }
 
     var optionValues = {
@@ -446,7 +451,8 @@ function setupSettingPanel(settingDiv, settingOpener, api, options) {
             80:     "80",
             free:   "Free"
         },
-        showPrintMargin: BOOL
+        showPrintMargin: BOOL,
+        useSoftTabs: BOOL
     }
 
     var table = [];
@@ -510,7 +516,8 @@ window.__ace_shadowed__.options = {
     gutter:     "false",
     fontSize:   "12px",
     softWrap:   "off",
-    showPrintMargin: "false"
+    showPrintMargin: "false",
+    useSoftTabs: "true"
 }
 
 });