Process backspace characters in output

These are like carriage return, but only affect a character before them
instead of the whole line. I've checked that this makes the output from
'man ls' look OK.

Closes gh-1572

notebook/static/base/js/utils.js

@@ -453,6 +453,22 @@ define([
         return txt;
     }
 
+    // Remove characters that are overridden by backspace characters
+    function fixBackspace(txt) {
+        var tmp = txt;
+        do {
+            txt = tmp;
+            // Cancel out anything-but-newline followed by backspace
+            tmp = txt.replace(/[^\n]\x08/gm, '');
+        } while (tmp.length < txt.length);
+        return txt;
+    }
+
+    // Remove characters overridden by backspace and carriage return
+    function fixOverwrittenChars(txt) {
+        return fixCarriageReturn(fixBackspace(txt));
+    }
+
     // Locate any URLs and convert them to a anchor tag
     function autoLinkUrls(txt) {
         return txt.replace(/(^|\s)(https?|ftp)(:[^'"<>\s]+)/gi,
@@ -972,6 +988,8 @@ define([
         uuid : uuid,
         fixConsole : fixConsole,
         fixCarriageReturn : fixCarriageReturn,
+        fixBackspace : fixBackspace,
+        fixOverwrittenChars: fixOverwrittenChars,
         autoLinkUrls : autoLinkUrls,
         points_to_pixels : points_to_pixels,
         get_body_data : get_body_data,

notebook/static/notebook/js/outputarea.js

@@ -504,7 +504,7 @@ define([
                     // latest output was in the same stream,
                     // so append to it instead of making a new output.
                     // escape ANSI & HTML specials:
-                    last.text = utils.fixCarriageReturn(last.text + json.text);
+                    last.text = utils.fixOverwrittenChars(last.text + json.text);
                     var pre = this.element.find('div.'+subclass).last().find('pre');
                     var html = utils.fixConsole(last.text);
                     html = utils.autoLinkUrls(html);
@@ -659,7 +659,7 @@ define([
     var append_text = function (data, md, element) {
         var type = 'text/plain';
         var toinsert = this.create_output_subarea(md, "output_text", type);
-        data = utils.fixCarriageReturn(data);
+        data = utils.fixOverwrittenChars(data);
         // escape ANSI & HTML specials in plaintext:
         data = utils.fixConsole(data);
         data = utils.autoLinkUrls(data);

notebook/static/notebook/js/pager.js

@@ -157,7 +157,7 @@ define([
          * The only user content injected with this HTML call is escaped by
          * the fixConsole() method.
          */
-        this.pager_element.find(".container").append($('<pre/>').html(utils.fixConsole(utils.fixCarriageReturn(text))));
+        this.pager_element.find(".container").append($('<pre/>').html(utils.fixConsole(utils.fixOverwrittenChars(text))));
     };
 
     Pager.prototype.append = function (htm) {