Ticket #3008: sage-3008.patch

File sage-3008.patch, 2.6 KB (added by was, 13 years ago)
  • sage/server/notebook/js.py

    # HG changeset patch
    # User William Stein <wstein@gmail.com>
    # Date 1210461159 25200
    # Node ID 397c8fa28b534d261ef9343e5ed7343fa0d63a60
    # Parent  86cd4f04b3fda1c297f73c57d807ee03cdd83662
    Fix trac #3008 -- Fix delete first cell bug. Also:
      2. Make deleting/merging cells via control-backspace feel slightly snappier
      3. Improve the documentation in js.py for the join_cell function.
    
    diff -r 86cd4f04b3fd -r 397c8fa28b53 sage/server/notebook/js.py
    a b function join_cell(id) { 
    22652265    whitespace, in which case the output is the output of the first
    22662266    cell.  We do this since a common way to delete a cell is to empty
    22672267    its input, then hit backspace.  It would be very confusing if the
    2268     output of the second cell were retained.
    2269        
     2268    output of the second cell were retained.  WARNING: Backspace
     2269    on the first cell if empty deletes it.
     2270
    22702271    INPUT:
    22712272        id -- integer cell id.
    22722273    OUTPUT:
    22732274        change the state of the worksheet in the DOM, global variables,
    2274         etc., and updates the server on this change. 
     2275        etc., and updates the server on this change.
    22752276    */
    22762277    var id_prev = id_of_cell_delta(id, -1);
    2277     if(id_prev == id) return;
     2278    var cell = get_cell(id);
    22782279
    2279     var cell = get_cell(id);
     2280    // The top cell is a special case.  Here we delete the top cell
     2281    // if it is empty.  Otherwise, we simply return doing nothing.
     2282    if(id_prev == id) {
     2283        // yes, top cell
     2284        if (is_whitespace(cell.value)) {
     2285            // Special case -- deleting the first cell in a worksheet and its whitespace
     2286            // get next cell
     2287            var cell_next = get_cell(id_of_cell_delta(id,1));
     2288            // put cursor on next one
     2289            cell_next.focus();
     2290            // delete this cell
     2291            cell_delete(id);
     2292            return;
     2293        } else {
     2294            return;
     2295        }
     2296    }
     2297
    22802298    var cell_prev = get_cell(id_prev);
    22812299   
    22822300    // We delete the cell above the cell with given id except in the
    22832301    // one case when the cell with id has empty input, in which case
    22842302    // we just delete that cell.
    22852303    if (is_whitespace(cell.value)) {
     2304        cell_prev.focus();
    22862305        cell_delete(id);
    2287         cell_prev.focus();
    22882306        return;
    22892307    }
    22902308
    function join_cell(id) { 
    22942312    // bottom cell.
    22952313    var val_prev = cell_prev.value;
    22962314
     2315    cell.focus();
    22972316    cell_delete(id_prev);
    2298     cell.focus();
    22992317
    23002318    // The following is so that joining two cells keeps a newline
    23012319    // between the input contents.