WordPress.org

Plugin Directory

Changeset 575331


Ignore:
Timestamp:
07/20/12 23:01:15 (21 months ago)
Author:
bpetty
Message:

New editor is now mostly working, still needs style and browser compatibility fixes.

Location:
better-file-editor/branches/development
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • better-file-editor/branches/development/better-file-editor.php

    r575032 r575331  
    66Version: 2.0 
    77Author: Bryan Petty <bryan@ibaku.net> 
     8Author URI: http://profiles.wordpress.org/bpetty/ 
    89License: GPLv2 or later 
    910License URI: http://www.gnu.org/licenses/gpl-2.0.html 
     
    2425            <script src="<?php echo plugins_url( 'js/wp-ace.js' , __FILE__ ); ?>"></script> 
    2526            <script type="text/javascript" charset="utf-8"> 
    26                 require("wp-ace"); 
     27                jQuery(document).ready(function() { 
     28                    require("wp-ace"); 
     29                }); 
    2730            </script> 
     31            <style type="text/css"> 
     32                #template div { 
     33                    margin-right: 0px; 
     34                } 
     35                #template #editor { 
     36                    margin-right: 210px; 
     37                } 
     38                #wp-ace-editor { 
     39                    position: relative; 
     40                    height: 560px; 
     41                    font-size: 12px; 
     42                } 
     43                .ace_editor { 
     44                    font-family: Consolas, Menlo, "Liberation Mono", Courier, monospace !important; 
     45                } 
     46            </style> 
    2847        <?php 
    2948    } 
  • better-file-editor/branches/development/js/wp-ace.js

    r575267 r575331  
     1/* 
     2Plugin Name: Better File Editor 
     3Author: Bryan Petty <bryan@ibaku.net> 
     4License: GPLv2 or later 
     5License URI: http://www.gnu.org/licenses/gpl-2.0.html 
     6*/ 
     7 
    18/* ***** BEGIN LICENSE BLOCK ***** 
    29 * Version: MPL 1.1/GPL 2.0/LGPL 2.1 
     
    4047 
    4148define('wp-ace', function(require, exports, module) { 
    42   "never use strict"; 
     49 
     50"never use strict"; 
    4351 
    4452require("ace/lib/fixoldbrowsers"); 
     
    6371var modes = []; 
    6472function getModeFromPath(path) { 
    65     var mode = modesByName.text; 
    66     for (var i = 0; i < modes.length; i++) { 
    67         if (modes[i].supportsFile(path)) { 
    68             mode = modes[i]; 
    69             break; 
    70         } 
    71     } 
    72     return mode; 
     73    var mode = modesByName.text; 
     74    for (var i = 0; i < modes.length; i++) { 
     75        if (modes[i].supportsFile(path)) { 
     76            mode = modes[i]; 
     77            break; 
     78        } 
     79    } 
     80    return mode; 
    7381}; 
    7482 
    7583var Mode = function(name, desc, extensions) { 
    76     this.name = name; 
    77     this.desc = desc; 
    78     this.mode = "ace/mode/" + name; 
    79     this.extRe = new RegExp("^.*\\.(" + extensions + ")$", "g"); 
     84    this.name = name; 
     85    this.desc = desc; 
     86    this.mode = "ace/mode/" + name; 
     87    this.extRe = new RegExp("^.*\\.(" + extensions + ")$", "g"); 
    8088}; 
    8189 
    8290Mode.prototype.supportsFile = function(filename) { 
    83     return filename.match(this.extRe); 
     91    return filename.match(this.extRe); 
    8492}; 
    8593 
    8694var modesByName = { 
    87     c9search:   ["C9Search"     , "c9search_results"], 
    88     coffee:     ["CoffeeScript" , "coffee|^Cakefile"], 
    89     coldfusion: ["ColdFusion"   , "cfm"], 
    90     csharp:     ["C#"           , "cs"], 
    91     css:        ["CSS"          , "css"], 
    92     diff:       ["Diff"         , "diff|patch"], 
    93     golang:     ["Go"           , "go"], 
    94     groovy:     ["Groovy"       , "groovy"], 
    95     haxe:       ["haXe"         , "hx"], 
    96     html:       ["HTML"         , "htm|html|xhtml"], 
    97     c_cpp:      ["C/C++"        , "c|cc|cpp|cxx|h|hh|hpp"], 
    98     clojure:    ["Clojure"      , "clj"], 
    99     java:       ["Java"         , "java"], 
    100     javascript: ["JavaScript"   , "js"], 
    101     json:       ["JSON"         , "json"], 
    102     jsx:        ["JSX"          , "jsx"], 
    103     latex:      ["LaTeX"        , "latex|tex|ltx|bib"], 
    104     less:       ["LESS"         , "less"], 
    105     liquid:     ["Liquid"       , "liquid"], 
    106     lua:        ["Lua"          , "lua"], 
    107     luapage:    ["LuaPage"      , "lp"], // http://keplerproject.github.com/cgilua/manual.html#templates 
    108     markdown:   ["Markdown"     , "md|markdown"], 
    109     ocaml:      ["OCaml"        , "ml|mli"], 
    110     perl:       ["Perl"         , "pl|pm"], 
    111     pgsql:      ["pgSQL"        , "pgsql"], 
    112     php:        ["PHP"          , "php|phtml"], 
    113     powershell: ["Powershell"   , "ps1"], 
    114     python:     ["Python"       , "py"], 
    115     ruby:       ["Ruby"         , "ru|gemspec|rake|rb"], 
    116     scad:       ["OpenSCAD"     , "scad"], 
    117     scala:      ["Scala"        , "scala"], 
    118     scss:       ["SCSS"         , "scss|sass"], 
    119     sh:         ["SH"           , "sh|bash|bat"], 
    120     sql:        ["SQL"          , "sql"], 
    121     svg:        ["SVG"          , "svg"], 
    122     text:       ["Text"         , "txt"], 
    123     textile:    ["Textile"      , "textile"], 
    124     xml:        ["XML"          , "xml|rdf|rss|wsdl|xslt|atom|mathml|mml|xul|xbl"], 
    125     xquery:     ["XQuery"       , "xq"], 
    126     yaml:       ["YAML"         , "yaml"] 
     95    c9search:   ["C9Search"     , "c9search_results"], 
     96    coffee:     ["CoffeeScript" , "coffee|^Cakefile"], 
     97    coldfusion: ["ColdFusion"   , "cfm"], 
     98    csharp:     ["C#"           , "cs"], 
     99    css:        ["CSS"          , "css"], 
     100    diff:       ["Diff"         , "diff|patch"], 
     101    golang:     ["Go"           , "go"], 
     102    groovy:     ["Groovy"       , "groovy"], 
     103    haxe:       ["haXe"         , "hx"], 
     104    html:       ["HTML"         , "htm|html|xhtml"], 
     105    c_cpp:      ["C/C++"        , "c|cc|cpp|cxx|h|hh|hpp"], 
     106    clojure:    ["Clojure"      , "clj"], 
     107    java:       ["Java"         , "java"], 
     108    javascript: ["JavaScript"   , "js"], 
     109    json:       ["JSON"         , "json"], 
     110    jsx:        ["JSX"          , "jsx"], 
     111    latex:      ["LaTeX"        , "latex|tex|ltx|bib"], 
     112    less:       ["LESS"         , "less"], 
     113    liquid:     ["Liquid"       , "liquid"], 
     114    lua:        ["Lua"          , "lua"], 
     115    luapage:    ["LuaPage"      , "lp"], // http://keplerproject.github.com/cgilua/manual.html#templates 
     116    markdown:   ["Markdown"     , "md|markdown"], 
     117    ocaml:      ["OCaml"        , "ml|mli"], 
     118    perl:       ["Perl"         , "pl|pm"], 
     119    pgsql:      ["pgSQL"        , "pgsql"], 
     120    php:        ["PHP"          , "php|phtml"], 
     121    powershell: ["Powershell"   , "ps1"], 
     122    python:     ["Python"       , "py"], 
     123    ruby:       ["Ruby"         , "ru|gemspec|rake|rb"], 
     124    scad:       ["OpenSCAD"     , "scad"], 
     125    scala:      ["Scala"        , "scala"], 
     126    scss:       ["SCSS"         , "scss|sass"], 
     127    sh:         ["SH"           , "sh|bash|bat"], 
     128    sql:        ["SQL"          , "sql"], 
     129    svg:        ["SVG"          , "svg"], 
     130    text:       ["Text"         , "txt"], 
     131    textile:    ["Textile"      , "textile"], 
     132    xml:        ["XML"          , "xml|rdf|rss|wsdl|xslt|atom|mathml|mml|xul|xbl"], 
     133    xquery:     ["XQuery"       , "xq"], 
     134    yaml:       ["YAML"         , "yaml"] 
    127135}; 
    128136 
    129137for (var name in modesByName) { 
    130     var mode = modesByName[name]; 
    131     mode = new Mode(name, mode[0], mode[1]) 
    132     modesByName[name] = mode; 
    133     modes.push(mode); 
     138    var mode = modesByName[name]; 
     139    mode = new Mode(name, mode[0], mode[1]) 
     140    modesByName[name] = mode; 
     141    modes.push(mode); 
    134142} 
    135143 
     
    137145/*********** create editor ***************************/ 
    138146 
    139 var controls = document.getElementById("wp-ace-editor-controls"); 
     147jQuery('#newcontent').parent().attr('id', 'editor'); 
     148 
     149jQuery('#newcontent').after('\ 
     150<div id="wp-ace-editor-controls">\ 
     151    <ul>\ 
     152        <li>\ 
     153            <select id="editor_theme" size="1">\ 
     154                <option value="ace/theme/chrome">Chrome</option>\ 
     155                <option value="ace/theme/clouds">Clouds</option>\ 
     156                <option value="ace/theme/clouds_midnight">Clouds Midnight</option>\ 
     157                <option value="ace/theme/cobalt">Cobalt</option>\ 
     158                <option value="ace/theme/crimson_editor">Crimson Editor</option>\ 
     159                <option value="ace/theme/dawn">Dawn</option>\ 
     160                <option value="ace/theme/dreamweaver">Dreamweaver</option>\ 
     161                <option value="ace/theme/eclipse">Eclipse</option>\ 
     162                <option value="ace/theme/idle_fingers">idleFingers</option>\ 
     163                <option value="ace/theme/kr_theme">krTheme</option>\ 
     164                <option value="ace/theme/merbivore">Merbivore</option>\ 
     165                <option value="ace/theme/merbivore_soft">Merbivore Soft</option>\ 
     166                <option value="ace/theme/mono_industrial">Mono Industrial</option>\ 
     167                <option value="ace/theme/monokai">Monokai</option>\ 
     168                <option value="ace/theme/pastel_on_dark">Pastel on dark</option>\ 
     169                <option value="ace/theme/solarized_dark">Solarized Dark</option>\ 
     170                <option value="ace/theme/solarized_light">Solarized Light</option>\ 
     171                <option value="ace/theme/textmate" selected="selected">TextMate</option>\ 
     172                <option value="ace/theme/twilight">Twilight</option>\ 
     173                <option value="ace/theme/tomorrow">Tomorrow</option>\ 
     174                <option value="ace/theme/tomorrow_night">Tomorrow Night</option>\ 
     175                <option value="ace/theme/tomorrow_night_blue">Tomorrow Night Blue</option>\ 
     176                <option value="ace/theme/tomorrow_night_bright">Tomorrow Night Bright</option>\ 
     177                <option value="ace/theme/tomorrow_night_eighties">Tomorrow Night 80s</option>\ 
     178                <option value="ace/theme/vibrant_ink">Vibrant Ink</option>\ 
     179            </select>\ 
     180        </li>\ 
     181        <li>\ 
     182            <select id="fontsize" size="1">\ 
     183                <option value="10px">10px</option>\ 
     184                <option value="11px">11px</option>\ 
     185                <option value="12px" selected="selected">12px</option>\ 
     186                <option value="14px">14px</option>\ 
     187                <option value="16px">16px</option>\ 
     188                <option value="20px">20px</option>\ 
     189                <option value="24px">24px</option>\ 
     190            </select>\ 
     191        </li>\ 
     192        <li>\ 
     193            <input type="checkbox" name="show_hidden" id="show_hidden">Visible Whitespace</input>\ 
     194        </li>\ 
     195        <li>\ 
     196            <input type="checkbox" id="show_gutter" checked>Show Gutter</input>\ 
     197        </li>\ 
     198        <li>\ 
     199            <input type="checkbox" id="show_print_margin" checked>Show Ruler</input>\ 
     200        </li>\ 
     201    </ul>\ 
     202</div>\ 
     203<div id="wp-ace-editor"></div>\ 
     204'); 
     205 
    140206var container = document.getElementById("wp-ace-editor"); 
    141207var textarea = document.getElementById("newcontent"); 
    142 controls.style.display = 'block'; 
    143 container.style.display = 'block'; 
    144208textarea.style.display = 'none'; 
    145209 
     
    149213env.editor = split.getEditor(0); 
    150214split.on("focus", function(editor) { 
    151     env.editor = editor; 
    152     updateUIEditorOptions(); 
     215    env.editor = editor; 
     216    updateUIEditorOptions(); 
    153217}); 
    154218env.split = split; 
     
    172236 
    173237env.editor.commands.addCommands([{ 
    174     name: "gotoline", 
    175     bindKey: {win: "Ctrl-L", mac: "Command-L"}, 
    176     exec: function(editor, line) { 
    177         if (typeof needle == "object") { 
    178             var arg = this.name + " " + editor.getCursorPosition().row; 
    179             editor.cmdLine.setValue(arg, 1) 
    180             editor.cmdLine.focus() 
    181             return 
    182         } 
    183         line = parseInt(line, 10); 
    184         if (!isNaN(line)) 
    185             editor.gotoLine(line); 
    186     }, 
    187     readOnly: true 
     238    name: "gotoline", 
     239    bindKey: {win: "Ctrl-L", mac: "Command-L"}, 
     240    exec: function(editor, line) { 
     241        if (typeof needle == "object") { 
     242            var arg = this.name + " " + editor.getCursorPosition().row; 
     243            editor.cmdLine.setValue(arg, 1) 
     244            editor.cmdLine.focus() 
     245            return 
     246        } 
     247        line = parseInt(line, 10); 
     248        if (!isNaN(line)) 
     249            editor.gotoLine(line); 
     250    }, 
     251    readOnly: true 
    188252}, { 
    189     name: "find", 
    190     bindKey: {win: "Ctrl-F", mac: "Command-F"}, 
    191     exec: function(editor, needle) { 
    192         if (typeof needle == "object") { 
    193             var arg = this.name + " " + editor.getCopyText() 
    194             editor.cmdLine.setValue(arg, 1) 
    195             editor.cmdLine.focus() 
    196             return 
    197         } 
    198         editor.find(needle); 
    199     }, 
    200     readOnly: true 
     253    name: "find", 
     254    bindKey: {win: "Ctrl-F", mac: "Command-F"}, 
     255    exec: function(editor, needle) { 
     256        if (typeof needle == "object") { 
     257            var arg = this.name + " " + editor.getCopyText() 
     258            editor.cmdLine.setValue(arg, 1) 
     259            editor.cmdLine.focus() 
     260            return 
     261        } 
     262        editor.find(needle); 
     263    }, 
     264    readOnly: true 
    201265}, { 
    202     name: "focusCommandLine", 
    203     bindKey: "shift-esc", 
    204     exec: function(editor, needle) { editor.cmdLine.focus(); }, 
    205     readOnly: true 
     266    name: "focusCommandLine", 
     267    bindKey: "shift-esc", 
     268    exec: function(editor, needle) { editor.cmdLine.focus(); }, 
     269    readOnly: true 
    206270}]) 
    207271 
    208272cmdLine.commands.bindKeys({ 
    209     "Shift-Return|Ctrl-Return|Alt-Return": function(cmdLine) { cmdLine.insert("\n")}, 
    210     "Esc|Shift-Esc": function(cmdLine){ cmdLine.editor.focus(); }, 
    211     "Return": function(cmdLine){ 
    212         var command = cmdLine.getValue().split(/\s+/); 
    213         var editor = cmdLine.editor; 
    214         editor.commands.exec(command[0], editor, command[1]); 
    215         editor.focus(); 
    216     }, 
     273    "Shift-Return|Ctrl-Return|Alt-Return": function(cmdLine) { cmdLine.insert("\n")}, 
     274    "Esc|Shift-Esc": function(cmdLine){ cmdLine.editor.focus(); }, 
     275    "Return": function(cmdLine){ 
     276        var command = cmdLine.getValue().split(/\s+/); 
     277        var editor = cmdLine.editor; 
     278        editor.commands.exec(command[0], editor, command[1]); 
     279        editor.focus(); 
     280    }, 
    217281}) 
    218282 
     
    225289var commands = env.editor.commands; 
    226290commands.addCommand({ 
    227     name: "save", 
    228     bindKey: {win: "Ctrl-S", mac: "Command-S"}, 
    229     exec: function() {alert("Fake Save File");} 
     291    name: "save", 
     292    bindKey: {win: "Ctrl-S", mac: "Command-S"}, 
     293    exec: function() {alert("Fake Save File");} 
    230294}); 
    231295 
     
    257321 
    258322/*********** options pane ***************************/ 
    259 var wrapModeEl = document.getElementById("soft_wrap"); 
    260323var themeEl = document.getElementById("editor_theme"); 
    261324var showHiddenEl = document.getElementById("show_hidden"); 
     
    266329 
    267330function updateUIEditorOptions() { 
    268     var editor = env.editor; 
    269     var session = editor.session; 
    270  
    271     saveOption(wrapModeEl, session.getUseWrapMode() ? session.getWrapLimitRange().min || "free" : "off"); 
    272  
    273     saveOption(themeEl, editor.getTheme()); 
    274     saveOption(showHiddenEl, editor.getShowInvisibles()); 
    275     saveOption(showGutterEl, editor.renderer.getShowGutter()); 
    276     saveOption(showPrintMarginEl, editor.renderer.getShowPrintMargin()); 
     331    var editor = env.editor; 
     332    var session = editor.session; 
     333 
     334    saveOption(themeEl, editor.getTheme()); 
     335    saveOption(showHiddenEl, editor.getShowInvisibles()); 
     336    saveOption(showGutterEl, editor.renderer.getShowGutter()); 
     337    saveOption(showPrintMarginEl, editor.renderer.getShowPrintMargin()); 
    277338} 
    278339 
    279340function saveOption(el, val) { 
    280     if (!el.onchange && !el.onclick) 
    281         return; 
    282  
    283     if ("checked" in el) { 
    284         if (val !== undefined) 
    285             el.checked = val; 
    286  
    287         localStorage && localStorage.setItem(el.id, el.checked ? 1 : 0); 
    288     } 
    289     else { 
    290         if (val !== undefined) 
    291             el.value = val; 
    292  
    293         localStorage && localStorage.setItem(el.id, el.value); 
    294     } 
     341    if (!el.onchange && !el.onclick) 
     342        return; 
     343 
     344    if ("checked" in el) { 
     345        if (val !== undefined) 
     346            el.checked = val; 
     347 
     348        localStorage && localStorage.setItem(el.id, el.checked ? 1 : 0); 
     349    } 
     350    else { 
     351        if (val !== undefined) 
     352            el.value = val; 
     353 
     354        localStorage && localStorage.setItem(el.id, el.value); 
     355    } 
    295356} 
    296357 
    297358event.addListener(themeEl, "mouseover", function(e){ 
    298     this.desiredValue = e.target.value; 
    299     if (!this.$timer) 
    300         this.$timer = setTimeout(this.updateTheme); 
     359    this.desiredValue = e.target.value; 
     360    if (!this.$timer) 
     361        this.$timer = setTimeout(this.updateTheme); 
    301362}) 
    302363 
    303364event.addListener(themeEl, "mouseout", function(e){ 
    304     this.desiredValue = null; 
    305     if (!this.$timer) 
    306         this.$timer = setTimeout(this.updateTheme, 20); 
     365    this.desiredValue = null; 
     366    if (!this.$timer) 
     367        this.$timer = setTimeout(this.updateTheme, 20); 
    307368}) 
    308369 
    309370themeEl.updateTheme = function(){ 
    310     env.split.setTheme(themeEl.desiredValue || themeEl.selectedValue); 
    311     themeEl.$timer = null; 
     371    env.split.setTheme(themeEl.desiredValue || themeEl.selectedValue); 
     372    themeEl.$timer = null; 
    312373} 
    313374 
    314375bindDropdown("editor_theme", function(value) { 
    315     if (!value) 
    316         return; 
    317     env.editor.setTheme(value); 
    318     themeEl.selectedValue = value; 
     376    if (!value) 
     377        return; 
     378    env.editor.setTheme(value); 
     379    themeEl.selectedValue = value; 
    319380}); 
    320381 
    321382bindDropdown("fontsize", function(value) { 
    322     env.split.setFontSize(value); 
     383    env.split.setFontSize(value); 
    323384}); 
    324385 
    325 bindDropdown("soft_wrap", function(value) { 
    326     var session = env.editor.getSession(); 
    327     var renderer = env.editor.renderer; 
    328     switch (value) { 
    329         case "off": 
    330             session.setUseWrapMode(false); 
    331             renderer.setPrintMarginColumn(80); 
    332             break; 
    333         case "40": 
    334             session.setUseWrapMode(true); 
    335             session.setWrapLimitRange(40, 40); 
    336             renderer.setPrintMarginColumn(40); 
    337             break; 
    338         case "80": 
    339             session.setUseWrapMode(true); 
    340             session.setWrapLimitRange(80, 80); 
    341             renderer.setPrintMarginColumn(80); 
    342             break; 
    343         case "free": 
    344             session.setUseWrapMode(true); 
    345             session.setWrapLimitRange(null, null); 
    346             renderer.setPrintMarginColumn(80); 
    347             break; 
    348     } 
     386bindCheckbox("show_hidden", function(checked) { 
     387    env.editor.setShowInvisibles(checked); 
    349388}); 
    350389 
    351 bindCheckbox("show_hidden", function(checked) { 
    352     env.editor.setShowInvisibles(checked); 
     390bindCheckbox("show_gutter", function(checked) { 
     391    env.editor.renderer.setShowGutter(checked); 
    353392}); 
    354393 
    355 bindCheckbox("show_gutter", function(checked) { 
    356     env.editor.renderer.setShowGutter(checked); 
     394bindCheckbox("show_print_margin", function(checked) { 
     395    env.editor.renderer.setShowPrintMargin(checked); 
    357396}); 
    358397 
    359 bindCheckbox("show_print_margin", function(checked) { 
    360     env.editor.renderer.setShowPrintMargin(checked); 
    361 }); 
    362  
    363 bindCheckbox("fade_fold_widgets", function(checked) { 
    364     env.editor.setFadeFoldWidgets(checked); 
    365 }); 
    366  
    367 var secondSession = null; 
    368 bindDropdown("split", function(value) { 
    369     var sp = env.split; 
    370     if (value == "none") { 
    371         if (sp.getSplits() == 2) { 
    372             secondSession = sp.getEditor(1).session; 
    373         } 
    374         sp.setSplits(1); 
    375     } else { 
    376         var newEditor = (sp.getSplits() == 1); 
    377         if (value == "below") { 
    378             sp.setOrientation(sp.BELOW); 
    379         } else { 
    380             sp.setOrientation(sp.BESIDE); 
    381         } 
    382         sp.setSplits(2); 
    383  
    384         if (newEditor) { 
    385             var session = secondSession || sp.getEditor(0).session; 
    386             var newSession = sp.setSession(session, 1); 
    387             newSession.name = session.name; 
    388         } 
    389     } 
    390 }); 
    391  
    392398function bindCheckbox(id, callback) { 
    393     var el = document.getElementById(id); 
    394     if (localStorage && localStorage.getItem(id)) 
    395         el.checked = localStorage.getItem(id) == "1"; 
    396  
    397     var onCheck = function() { 
    398         callback(!!el.checked); 
    399         saveOption(el); 
    400     }; 
    401     el.onclick = onCheck; 
    402     onCheck(); 
     399    var el = document.getElementById(id); 
     400    if (localStorage && localStorage.getItem(id)) 
     401        el.checked = localStorage.getItem(id) == "1"; 
     402 
     403    var onCheck = function() { 
     404        callback(!!el.checked); 
     405        saveOption(el); 
     406    }; 
     407    el.onclick = onCheck; 
     408    onCheck(); 
    403409} 
    404410 
    405411function bindDropdown(id, callback) { 
    406     var el = document.getElementById(id); 
    407     if (localStorage && localStorage.getItem(id)) 
    408         el.value = localStorage.getItem(id); 
    409  
    410     var onChange = function() { 
    411         callback(el.value); 
    412         saveOption(el); 
    413     }; 
    414  
    415     el.onchange = onChange; 
    416     onChange(); 
     412    var el = document.getElementById(id); 
     413    if (localStorage && localStorage.getItem(id)) 
     414        el.value = localStorage.getItem(id); 
     415 
     416    var onChange = function() { 
     417        callback(el.value); 
     418        saveOption(el); 
     419    }; 
     420 
     421    el.onchange = onChange; 
     422    onChange(); 
    417423} 
    418424 
    419425function fillDropdown(list, el) { 
    420     list.forEach(function(item) { 
    421         var option = document.createElement("option"); 
    422         option.setAttribute("value", item.name); 
    423         option.innerHTML = item.desc; 
    424         el.appendChild(option); 
    425     }); 
     426    list.forEach(function(item) { 
     427        var option = document.createElement("option"); 
     428        option.setAttribute("value", item.name); 
     429        option.innerHTML = item.desc; 
     430        el.appendChild(option); 
     431    }); 
    426432} 
    427433 
     
    433439 
    434440function singleLineEditor(el) { 
    435     var renderer = new Renderer(el); 
    436     renderer.scrollBar.element.style.display = "none"; 
    437     renderer.scrollBar.width = 0; 
    438     renderer.content.style.height = "auto"; 
    439  
    440     renderer.screenToTextCoordinates = function(x, y) { 
    441         var pos = this.pixelToScreenCoordinates(x, y); 
    442         return this.session.screenToDocumentPosition( 
    443             Math.min(this.session.getScreenLength() - 1, Math.max(pos.row, 0)), 
    444             Math.max(pos.column, 0) 
    445         ); 
    446     }; 
    447     // todo size change event 
    448     renderer.$computeLayerConfig = function() { 
    449         var longestLine = this.$getLongestLine(); 
    450         var firstRow = 0; 
    451         var lastRow = this.session.getLength(); 
    452         var height = this.session.getScreenLength() * this.lineHeight; 
    453  
    454         this.scrollTop = 0; 
    455         var config = this.layerConfig; 
    456         config.width = longestLine; 
    457         config.padding = this.$padding; 
    458         config.firstRow = 0; 
    459         config.firstRowScreen = 0; 
    460         config.lastRow = lastRow; 
    461         config.lineHeight = this.lineHeight; 
    462         config.characterWidth = this.characterWidth; 
    463         config.minHeight = height; 
    464         config.maxHeight = height; 
    465         config.offset = 0; 
    466         config.height = height; 
    467  
    468         this.$gutterLayer.element.style.marginTop = 0 + "px"; 
    469         this.content.style.marginTop = 0 + "px"; 
    470         this.content.style.width = longestLine + 2 * this.$padding + "px"; 
    471         this.content.style.height = height + "px"; 
    472         this.scroller.style.height = height + "px"; 
    473         this.container.style.height = height + "px"; 
    474     }; 
    475     renderer.isScrollableBy=function(){return false}; 
    476  
    477     var editor = new Editor(renderer); 
    478     new MultiSelect(editor); 
    479     editor.session.setUndoManager(new UndoManager()); 
    480  
    481     editor.setHighlightActiveLine(false); 
    482     editor.setShowPrintMargin(false); 
    483     editor.renderer.setShowGutter(false); 
    484     // editor.renderer.setHighlightGutterLine(false); 
    485     return editor; 
     441    var renderer = new Renderer(el); 
     442    renderer.scrollBar.element.style.display = "none"; 
     443    renderer.scrollBar.width = 0; 
     444    renderer.content.style.height = "auto"; 
     445 
     446    renderer.screenToTextCoordinates = function(x, y) { 
     447        var pos = this.pixelToScreenCoordinates(x, y); 
     448        return this.session.screenToDocumentPosition( 
     449            Math.min(this.session.getScreenLength() - 1, Math.max(pos.row, 0)), 
     450            Math.max(pos.column, 0) 
     451        ); 
     452    }; 
     453    // todo size change event 
     454    renderer.$computeLayerConfig = function() { 
     455        var longestLine = this.$getLongestLine(); 
     456        var firstRow = 0; 
     457        var lastRow = this.session.getLength(); 
     458        var height = this.session.getScreenLength() * this.lineHeight; 
     459 
     460        this.scrollTop = 0; 
     461        var config = this.layerConfig; 
     462        config.width = longestLine; 
     463        config.padding = this.$padding; 
     464        config.firstRow = 0; 
     465        config.firstRowScreen = 0; 
     466        config.lastRow = lastRow; 
     467        config.lineHeight = this.lineHeight; 
     468        config.characterWidth = this.characterWidth; 
     469        config.minHeight = height; 
     470        config.maxHeight = height; 
     471        config.offset = 0; 
     472        config.height = height; 
     473 
     474        this.$gutterLayer.element.style.marginTop = 0 + "px"; 
     475        this.content.style.marginTop = 0 + "px"; 
     476        this.content.style.width = longestLine + 2 * this.$padding + "px"; 
     477        this.content.style.height = height + "px"; 
     478        this.scroller.style.height = height + "px"; 
     479        this.container.style.height = height + "px"; 
     480    }; 
     481    renderer.isScrollableBy=function(){return false}; 
     482 
     483    var editor = new Editor(renderer); 
     484    new MultiSelect(editor); 
     485    editor.session.setUndoManager(new UndoManager()); 
     486 
     487    editor.setHighlightActiveLine(false); 
     488    editor.setShowPrintMargin(false); 
     489    editor.renderer.setShowGutter(false); 
     490    // editor.renderer.setHighlightGutterLine(false); 
     491    return editor; 
    486492}; 
    487493 
     
    556562 
    557563  var Split = function(container, theme, splits) { 
    558       this.BELOW = 1; 
    559       this.BESIDE = 0; 
    560  
    561       this.$container = container; 
    562       this.$theme = theme; 
    563       this.$splits = 0; 
    564       this.$editorCSS = ""; 
    565       this.$editors = []; 
    566       this.$orientation = this.BESIDE; 
    567  
    568       this.setSplits(splits || 1); 
    569       this.$cEditor = this.$editors[0]; 
    570  
    571  
    572       this.on("focus", function(editor) { 
    573         this.$cEditor = editor; 
    574       }.bind(this)); 
    575     }; 
     564      this.BELOW = 1; 
     565      this.BESIDE = 0; 
     566 
     567      this.$container = container; 
     568      this.$theme = theme; 
     569      this.$splits = 0; 
     570      this.$editorCSS = ""; 
     571      this.$editors = []; 
     572      this.$orientation = this.BESIDE; 
     573 
     574      this.setSplits(splits || 1); 
     575      this.$cEditor = this.$editors[0]; 
     576 
     577 
     578      this.on("focus", function(editor) { 
     579        this.$cEditor = editor; 
     580      }.bind(this)); 
     581    }; 
    576582 
    577583  (function() { 
    578584 
    579     oop.implement(this, EventEmitter); 
    580  
    581     this.$createEditor = function() { 
    582       var el = document.createElement("div"); 
    583       el.className = this.$editorCSS; 
    584       el.style.cssText = "position: absolute; top:0px; bottom:0px"; 
    585       this.$container.appendChild(el); 
    586       var editor = new Editor(new Renderer(el, this.$theme)); 
    587  
    588       editor.on("focus", function() { 
    589         this._emit("focus", editor); 
    590       }.bind(this)); 
    591  
    592       this.$editors.push(editor); 
    593       editor.setFontSize(this.$fontSize); 
    594       return editor; 
    595     }; 
    596  
    597     /** internal, hide 
    598     * Split.setSplits(splits) -> Void 
    599     * - splits (Number): The new number of splits 
    600     * 
    601     *  
    602     * 
    603     **/ 
    604     this.setSplits = function(splits) { 
    605       var editor; 
    606       if (splits < 1) { 
    607         throw "The number of splits have to be > 0!"; 
    608       } 
    609  
    610       if (splits == this.$splits) { 
    611         return; 
    612       } else if (splits > this.$splits) { 
    613         while (this.$splits < this.$editors.length && this.$splits < splits) { 
    614           editor = this.$editors[this.$splits]; 
    615           this.$container.appendChild(editor.container); 
    616           editor.setFontSize(this.$fontSize); 
    617           this.$splits++; 
    618         } 
    619         while (this.$splits < splits) { 
    620           this.$createEditor(); 
    621           this.$splits++; 
    622         } 
    623       } else { 
    624         while (this.$splits > splits) { 
    625           editor = this.$editors[this.$splits - 1]; 
    626           this.$container.removeChild(editor.container); 
    627           this.$splits--; 
    628         } 
    629       } 
    630       this.resize(); 
    631     }; 
    632  
    633     /** 
    634     * Split.getSplits() -> Number 
    635     * 
    636     * Returns the number of splits. 
    637     * 
    638     **/ 
    639     this.getSplits = function() { 
    640       return this.$splits; 
    641     }; 
    642  
    643     /** 
    644     * Split.getEditor(idx) -> Editor 
    645     * -idx (Number): The index of the editor you want 
    646     * 
    647     * Returns the editor identified by the index `idx`. 
    648     * 
    649     **/ 
    650     this.getEditor = function(idx) { 
    651       return this.$editors[idx]; 
    652     }; 
    653  
    654     /** 
    655     * Split.getCurrentEditor() -> Editor 
    656     * 
    657     * Returns the current editor. 
    658     * 
    659     **/ 
    660     this.getCurrentEditor = function() { 
    661       return this.$cEditor; 
    662     }; 
    663  
    664     /** related to: Editor.focus 
    665     * Split.focus() -> Void 
    666     * 
    667     * Focuses the current editor. 
    668     * 
    669     **/ 
    670     this.focus = function() { 
    671       this.$cEditor.focus(); 
    672     }; 
    673  
    674     /** related to: Editor.blur 
    675     * Split.blur() -> Void 
    676     * 
    677     * Blurs the current editor. 
    678     * 
    679     **/ 
    680     this.blur = function() { 
    681       this.$cEditor.blur(); 
    682     }; 
    683  
    684     /** related to: Editor.setTheme 
    685     * Split.setTheme(theme) -> Void 
    686     * - theme (String): The name of the theme to set 
    687     *  
    688     * Sets a theme for each of the available editors. 
    689     **/ 
    690     this.setTheme = function(theme) { 
    691       this.$editors.forEach(function(editor) { 
    692         editor.setTheme(theme); 
    693       }); 
    694     }; 
    695  
    696     /** internal, hide 
    697     * Split.setKeyboardHandler(keybinding) -> Void 
    698     * - keybinding (String): 
    699     *  
    700     * 
    701     **/ 
    702     this.setKeyboardHandler = function(keybinding) { 
    703       this.$editors.forEach(function(editor) { 
    704         editor.setKeyboardHandler(keybinding); 
    705       }); 
    706     }; 
    707  
    708     /** internal, hide 
    709     * Split.forEach(callback, scope) -> Void 
    710     * - callback (Function): A callback function to execute 
    711     * - scope (String):  
    712     *  
    713     * Executes `callback` on all of the available editors.  
    714     * 
    715     **/ 
    716     this.forEach = function(callback, scope) { 
    717       this.$editors.forEach(callback, scope); 
    718     }; 
    719  
    720     /** related to: Editor.setFontSize 
    721     * Split.setFontSize(size) -> Void 
    722     * - size (Number): The new font size 
    723     *  
    724     * Sets the font size, in pixels, for all the available editors. 
    725     * 
    726     **/ 
    727     this.$fontSize = ""; 
    728     this.setFontSize = function(size) { 
    729       this.$fontSize = size; 
    730       this.forEach(function(editor) { 
    731         editor.setFontSize(size); 
    732       }); 
    733     }; 
    734  
    735     this.$cloneSession = function(session) { 
    736       var s = new EditSession(session.getDocument(), session.getMode()); 
    737  
    738       var undoManager = session.getUndoManager(); 
    739       if (undoManager) { 
    740         var undoManagerProxy = new UndoManagerProxy(undoManager, s); 
    741         s.setUndoManager(undoManagerProxy); 
    742       } 
    743  
    744       // Overwrite the default $informUndoManager function such that new delas 
    745       // aren't added to the undo manager from the new and the old session. 
    746       s.$informUndoManager = lang.deferredCall(function() { 
    747         s.$deltas = []; 
    748       }); 
    749  
    750       // Copy over 'settings' from the session. 
    751       s.setTabSize(session.getTabSize()); 
    752       s.setUseSoftTabs(session.getUseSoftTabs()); 
    753       s.setOverwrite(session.getOverwrite()); 
    754       s.setBreakpoints(session.getBreakpoints()); 
    755       s.setUseWrapMode(session.getUseWrapMode()); 
    756       s.setUseWorker(session.getUseWorker()); 
    757       s.setWrapLimitRange(session.$wrapLimitRange.min, session.$wrapLimitRange.max); 
    758       s.$foldData = session.$cloneFoldData(); 
    759  
    760       return s; 
    761     }; 
    762  
    763     /** related to: Editor.setSession 
    764     * Split.setSession(session, idx) -> Void 
    765     * - session (EditSession): The new edit session 
    766     * - idx (Number): The editor's index you're interested in 
    767     *  
    768     * Sets a new [[EditSession `EditSession`]] for the indicated editor. 
    769     * 
    770     **/ 
    771     this.setSession = function(session, idx) { 
    772       var editor; 
    773       if (idx == null) { 
    774         editor = this.$cEditor; 
    775       } else { 
    776         editor = this.$editors[idx]; 
    777       } 
    778  
    779       // Check if the session is used already by any of the editors in the 
    780       // split. If it is, we have to clone the session as two editors using 
    781       // the same session can cause terrible side effects (e.g. UndoQueue goes 
    782       // wrong). This also gives the user of Split the possibility to treat 
    783       // each session on each split editor different. 
    784       var isUsed = this.$editors.some(function(editor) { 
    785         return editor.session === session; 
    786       }); 
    787  
    788       if (isUsed) { 
    789         session = this.$cloneSession(session); 
    790       } 
    791       editor.setSession(session); 
    792  
    793       // Return the session set on the editor. This might be a cloned one. 
    794       return session; 
    795     }; 
    796  
    797     /** internal, hide 
    798     * Split.getOrientation() -> Number 
    799     *  
    800     * Returns the orientation. 
    801     * 
    802     **/ 
    803     this.getOrientation = function() { 
    804       return this.$orientation; 
    805     }; 
    806  
    807     /** internal, hide 
    808     * Split.setOrientation(oriantation) -> Void 
    809     * - oriantation (Number): 
    810     * 
    811     * Sets the orientation. 
    812     * 
    813     **/ 
    814     this.setOrientation = function(orientation) { 
    815       if (this.$orientation == orientation) { 
    816         return; 
    817       } 
    818       this.$orientation = orientation; 
    819       this.resize(); 
    820     }; 
    821  
    822     /**  internal 
    823     * Split.resize() -> Void 
    824     * 
    825     * 
    826     * 
    827     **/ 
    828     this.resize = function() { 
    829       var width = this.$container.clientWidth; 
    830       var height = this.$container.clientHeight; 
    831       var editor; 
    832  
    833       if (this.$orientation == this.BESIDE) { 
    834         var editorWidth = width / this.$splits; 
    835         for (var i = 0; i < this.$splits; i++) { 
    836           editor = this.$editors[i]; 
    837           editor.container.style.width = editorWidth + "px"; 
    838           editor.container.style.top = "0px"; 
    839           editor.container.style.left = i * editorWidth + "px"; 
    840           editor.container.style.height = height + "px"; 
    841           editor.resize(); 
    842         } 
    843       } else { 
    844         var editorHeight = height / this.$splits; 
    845         for (var i = 0; i < this.$splits; i++) { 
    846           editor = this.$editors[i]; 
    847           editor.container.style.width = width + "px"; 
    848           editor.container.style.top = i * editorHeight + "px"; 
    849           editor.container.style.left = "0px"; 
    850           editor.container.style.height = editorHeight + "px"; 
    851           editor.resize(); 
    852         } 
    853       } 
    854     }; 
     585    oop.implement(this, EventEmitter); 
     586 
     587    this.$createEditor = function() { 
     588      var el = document.createElement("div"); 
     589      el.className = this.$editorCSS; 
     590      el.style.cssText = "position: absolute; top:0px; bottom:0px"; 
     591      this.$container.appendChild(el); 
     592      var editor = new Editor(new Renderer(el, this.$theme)); 
     593 
     594      editor.on("focus", function() { 
     595        this._emit("focus", editor); 
     596      }.bind(this)); 
     597 
     598      this.$editors.push(editor); 
     599      editor.setFontSize(this.$fontSize); 
     600      return editor; 
     601    }; 
     602 
     603    /** internal, hide 
     604    * Split.setSplits(splits) -> Void 
     605    * - splits (Number): The new number of splits 
     606    * 
     607    *  
     608    * 
     609    **/ 
     610    this.setSplits = function(splits) { 
     611      var editor; 
     612      if (splits < 1) { 
     613        throw "The number of splits have to be > 0!"; 
     614      } 
     615 
     616      if (splits == this.$splits) { 
     617        return; 
     618      } else if (splits > this.$splits) { 
     619        while (this.$splits < this.$editors.length && this.$splits < splits) { 
     620          editor = this.$editors[this.$splits]; 
     621          this.$container.appendChild(editor.container); 
     622          editor.setFontSize(this.$fontSize); 
     623          this.$splits++; 
     624        } 
     625        while (this.$splits < splits) { 
     626          this.$createEditor(); 
     627          this.$splits++; 
     628        } 
     629      } else { 
     630        while (this.$splits > splits) { 
     631          editor = this.$editors[this.$splits - 1]; 
     632          this.$container.removeChild(editor.container); 
     633          this.$splits--; 
     634        } 
     635      } 
     636      this.resize(); 
     637    }; 
     638 
     639    /** 
     640    * Split.getSplits() -> Number 
     641    * 
     642    * Returns the number of splits. 
     643    * 
     644    **/ 
     645    this.getSplits = function() { 
     646      return this.$splits; 
     647    }; 
     648 
     649    /** 
     650    * Split.getEditor(idx) -> Editor 
     651    * -idx (Number): The index of the editor you want 
     652    * 
     653    * Returns the editor identified by the index `idx`. 
     654    * 
     655    **/ 
     656    this.getEditor = function(idx) { 
     657      return this.$editors[idx]; 
     658    }; 
     659 
     660    /** 
     661    * Split.getCurrentEditor() -> Editor 
     662    * 
     663    * Returns the current editor. 
     664    * 
     665    **/ 
     666    this.getCurrentEditor = function() { 
     667      return this.$cEditor; 
     668    }; 
     669 
     670    /** related to: Editor.focus 
     671    * Split.focus() -> Void 
     672    * 
     673    * Focuses the current editor. 
     674    * 
     675    **/ 
     676    this.focus = function() { 
     677      this.$cEditor.focus(); 
     678    }; 
     679 
     680    /** related to: Editor.blur 
     681    * Split.blur() -> Void 
     682    * 
     683    * Blurs the current editor. 
     684    * 
     685    **/ 
     686    this.blur = function() { 
     687      this.$cEditor.blur(); 
     688    }; 
     689 
     690    /** related to: Editor.setTheme 
     691    * Split.setTheme(theme) -> Void 
     692    * - theme (String): The name of the theme to set 
     693    *  
     694    * Sets a theme for each of the available editors. 
     695    **/ 
     696    this.setTheme = function(theme) { 
     697      this.$editors.forEach(function(editor) { 
     698        editor.setTheme(theme); 
     699      }); 
     700    }; 
     701 
     702    /** internal, hide 
     703    * Split.setKeyboardHandler(keybinding) -> Void 
     704    * - keybinding (String): 
     705    *  
     706    * 
     707    **/ 
     708    this.setKeyboardHandler = function(keybinding) { 
     709      this.$editors.forEach(function(editor) { 
     710        editor.setKeyboardHandler(keybinding); 
     711      }); 
     712    }; 
     713 
     714    /** internal, hide 
     715    * Split.forEach(callback, scope) -> Void 
     716    * - callback (Function): A callback function to execute 
     717    * - scope (String):  
     718    *  
     719    * Executes `callback` on all of the available editors.  
     720    * 
     721    **/ 
     722    this.forEach = function(callback, scope) { 
     723      this.$editors.forEach(callback, scope); 
     724    }; 
     725 
     726    /** related to: Editor.setFontSize 
     727    * Split.setFontSize(size) -> Void 
     728    * - size (Number): The new font size 
     729    *  
     730    * Sets the font size, in pixels, for all the available editors. 
     731    * 
     732    **/ 
     733    this.$fontSize = ""; 
     734    this.setFontSize = function(size) { 
     735      this.$fontSize = size; 
     736      this.forEach(function(editor) { 
     737        editor.setFontSize(size); 
     738      }); 
     739    }; 
     740 
     741    this.$cloneSession = function(session) { 
     742      var s = new EditSession(session.getDocument(), session.getMode()); 
     743 
     744      var undoManager = session.getUndoManager(); 
     745      if (undoManager) { 
     746        var undoManagerProxy = new UndoManagerProxy(undoManager, s); 
     747        s.setUndoManager(undoManagerProxy); 
     748      } 
     749 
     750      // Overwrite the default $informUndoManager function such that new delas 
     751      // aren't added to the undo manager from the new and the old session. 
     752      s.$informUndoManager = lang.deferredCall(function() { 
     753        s.$deltas = []; 
     754      }); 
     755 
     756      // Copy over 'settings' from the session. 
     757      s.setTabSize(session.getTabSize()); 
     758      s.setUseSoftTabs(session.getUseSoftTabs()); 
     759      s.setOverwrite(session.getOverwrite()); 
     760      s.setBreakpoints(session.getBreakpoints()); 
     761      s.setUseWrapMode(session.getUseWrapMode()); 
     762      s.setUseWorker(session.getUseWorker()); 
     763      s.setWrapLimitRange(session.$wrapLimitRange.min, session.$wrapLimitRange.max); 
     764      s.$foldData = session.$cloneFoldData(); 
     765 
     766      return s; 
     767    }; 
     768 
     769    /** related to: Editor.setSession 
     770    * Split.setSession(session, idx) -> Void 
     771    * - session (EditSession): The new edit session 
     772    * - idx (Number): The editor's index you're interested in 
     773    *  
     774    * Sets a new [[EditSession `EditSession`]] for the indicated editor. 
     775    * 
     776    **/ 
     777    this.setSession = function(session, idx) { 
     778      var editor; 
     779      if (idx == null) { 
     780        editor = this.$cEditor; 
     781      } else { 
     782        editor = this.$editors[idx]; 
     783      } 
     784 
     785      // Check if the session is used already by any of the editors in the 
     786      // split. If it is, we have to clone the session as two editors using 
     787      // the same session can cause terrible side effects (e.g. UndoQueue goes 
     788      // wrong). This also gives the user of Split the possibility to treat 
     789      // each session on each split editor different. 
     790      var isUsed = this.$editors.some(function(editor) { 
     791        return editor.session === session; 
     792      }); 
     793 
     794      if (isUsed) { 
     795        session = this.$cloneSession(session); 
     796      } 
     797      editor.setSession(session); 
     798 
     799      // Return the session set on the editor. This might be a cloned one. 
     800      return session; 
     801    }; 
     802 
     803    /** internal, hide 
     804    * Split.getOrientation() -> Number 
     805    *  
     806    * Returns the orientation. 
     807    * 
     808    **/ 
     809    this.getOrientation = function() { 
     810      return this.$orientation; 
     811    }; 
     812 
     813    /** internal, hide 
     814    * Split.setOrientation(oriantation) -> Void 
     815    * - oriantation (Number): 
     816    * 
     817    * Sets the orientation. 
     818    * 
     819    **/ 
     820    this.setOrientation = function(orientation) { 
     821      if (this.$orientation == orientation) { 
     822        return; 
     823      } 
     824      this.$orientation = orientation; 
     825      this.resize(); 
     826    }; 
     827 
     828    /**  internal 
     829    * Split.resize() -> Void 
     830    * 
     831    * 
     832    * 
     833    **/ 
     834    this.resize = function() { 
     835      var width = this.$container.clientWidth; 
     836      var height = this.$container.clientHeight; 
     837      var editor; 
     838 
     839      if (this.$orientation == this.BESIDE) { 
     840        var editorWidth = width / this.$splits; 
     841        for (var i = 0; i < this.$splits; i++) { 
     842          editor = this.$editors[i]; 
     843          editor.container.style.width = editorWidth + "px"; 
     844          editor.container.style.top = "0px"; 
     845          editor.container.style.left = i * editorWidth + "px"; 
     846          editor.container.style.height = height + "px"; 
     847          editor.resize(); 
     848        } 
     849      } else { 
     850        var editorHeight = height / this.$splits; 
     851        for (var i = 0; i < this.$splits; i++) { 
     852          editor = this.$editors[i]; 
     853          editor.container.style.width = width + "px"; 
     854          editor.container.style.top = i * editorHeight + "px"; 
     855          editor.container.style.left = "0px"; 
     856          editor.container.style.height = editorHeight + "px"; 
     857          editor.resize(); 
     858        } 
     859      } 
     860    }; 
    855861 
    856862  }).call(Split.prototype); 
     
    863869   **/ 
    864870  function UndoManagerProxy(undoManager, session) { 
    865     this.$u = undoManager; 
    866     this.$doc = session; 
     871    this.$u = undoManager; 
     872    this.$doc = session; 
    867873  } 
    868874 
    869875  (function() { 
    870     this.execute = function(options) { 
    871       this.$u.execute(options); 
    872     }; 
    873  
    874     this.undo = function() { 
    875       var selectionRange = this.$u.undo(true); 
    876       if (selectionRange) { 
    877         this.$doc.selection.setSelectionRange(selectionRange); 
    878       } 
    879     }; 
    880  
    881     this.redo = function() { 
    882       var selectionRange = this.$u.redo(true); 
    883       if (selectionRange) { 
    884         this.$doc.selection.setSelectionRange(selectionRange); 
    885       } 
    886     }; 
    887  
    888     this.reset = function() { 
    889       this.$u.reset(); 
    890     }; 
    891  
    892     this.hasUndo = function() { 
    893       return this.$u.hasUndo(); 
    894     }; 
    895  
    896     this.hasRedo = function() { 
    897       return this.$u.hasRedo(); 
    898     }; 
     876    this.execute = function(options) { 
     877      this.$u.execute(options); 
     878    }; 
     879 
     880    this.undo = function() { 
     881      var selectionRange = this.$u.undo(true); 
     882      if (selectionRange) { 
     883        this.$doc.selection.setSelectionRange(selectionRange); 
     884      } 
     885    }; 
     886 
     887    this.redo = function() { 
     888      var selectionRange = this.$u.redo(true); 
     889      if (selectionRange) { 
     890        this.$doc.selection.setSelectionRange(selectionRange); 
     891      } 
     892    }; 
     893 
     894    this.reset = function() { 
     895      this.$u.reset(); 
     896    }; 
     897 
     898    this.hasUndo = function() { 
     899      return this.$u.hasUndo(); 
     900    }; 
     901 
     902    this.hasRedo = function() { 
     903      return this.$u.hasRedo(); 
     904    }; 
    899905  }).call(UndoManagerProxy.prototype); 
    900906 
Note: See TracChangeset for help on using the changeset viewer.