Function insertBoolHere

lib/web/drags.js:1305–1312

()

};

var insertBoolHere = function () {
    var selection_start = cm.getCursor("from");
    cm.replaceRange(" 1 ", selection_start); // we pad with spaces, otherwise when we replace
    // this text we blow away our widget
    // as well
    var selection_end = cm.getCursor("to");
    return insertBool(selection_start, selection_end);
};

var insertBoolAtSelection = function () {
    var selection_start = cm.getCursor("from");