##// END OF EJS Templates
Merge pull request #2389 from takluyver/catch-histdb-errors...
Merge pull request #2389 from takluyver/catch-histdb-errors Catch sqlite DatabaseErrors in more places when reading the history database It seems sqlite can encounter corruption and throw an error when reading the database, although it has connected successfully. This borrows the move-and-recreate machinery we already had on connecting to the database. If such an error occurs, the corrupted file is moved and the user get warned of the name of the corrupted file.

File last commit:

r7357:7f3891a1
r8503:7904325b merge
Show More
utils.js
149 lines | 4.9 KiB | application/javascript | JavascriptLexer
//----------------------------------------------------------------------------
// Copyright (C) 2008-2011 The IPython Development Team
//
// Distributed under the terms of the BSD License. The full license is in
// the file COPYING, distributed as part of this software.
//----------------------------------------------------------------------------
//============================================================================
// Utilities
//============================================================================
IPython.namespace('IPython.utils');
IPython.utils = (function (IPython) {
var uuid = function () {
// http://www.ietf.org/rfc/rfc4122.txt
var s = [];
var hexDigits = "0123456789ABCDEF";
for (var i = 0; i < 32; i++) {
s[i] = hexDigits.substr(Math.floor(Math.random() * 0x10), 1);
}
s[12] = "4"; // bits 12-15 of the time_hi_and_version field to 0010
s[16] = hexDigits.substr((s[16] & 0x3) | 0x8, 1); // bits 6-7 of the clock_seq_hi_and_reserved to 01
var uuid = s.join("");
return uuid;
};
//Fix raw text to parse correctly in crazy XML
function xmlencode(string) {
return string.replace(/\&/g,'&'+'amp;')
.replace(/</g,'&'+'lt;')
.replace(/>/g,'&'+'gt;')
.replace(/\'/g,'&'+'apos;')
.replace(/\"/g,'&'+'quot;')
.replace(/`/g,'&'+'#96;');
}
//Map from terminal commands to CSS classes
ansi_colormap = {
"30":"ansiblack", "31":"ansired",
"32":"ansigreen", "33":"ansiyellow",
"34":"ansiblue", "35":"ansipurple","36":"ansicyan",
"37":"ansigrey", "01":"ansibold"
};
// Transform ANSI color escape codes into HTML <span> tags with css
// classes listed in the above ansi_colormap object. The actual color used
// are set in the css file.
function fixConsole(txt) {
txt = xmlencode(txt);
var re = /\033\[([\dA-Fa-f;]*?)m/;
var opened = false;
var cmds = [];
var opener = "";
var closer = "";
while (re.test(txt)) {
var cmds = txt.match(re)[1].split(";");
closer = opened?"</span>":"";
opened = cmds.length > 1 || cmds[0] != 0;
var rep = [];
for (var i in cmds)
if (typeof(ansi_colormap[cmds[i]]) != "undefined")
rep.push(ansi_colormap[cmds[i]]);
opener = rep.length > 0?"<span class=\""+rep.join(" ")+"\">":"";
txt = txt.replace(re, closer + opener);
}
if (opened) txt += "</span>";
return txt;
}
// Remove chunks that should be overridden by the effect of
// carriage return characters
function fixCarriageReturn(txt) {
tmp = txt;
do {
txt = tmp;
tmp = txt.replace(/^.*\r(?!\n)/gm, '');
} while (tmp.length < txt.length);
return txt;
}
grow = function(element) {
// Grow the cell by hand. This is used upon reloading from JSON, when the
// autogrow handler is not called.
var dom = element.get(0);
var lines_count = 0;
// modified split rule from
// http://stackoverflow.com/questions/2035910/how-to-get-the-number-of-lines-in-a-textarea/2036424#2036424
var lines = dom.value.split(/\r|\r\n|\n/);
lines_count = lines.length;
if (lines_count >= 1) {
dom.rows = lines_count;
} else {
dom.rows = 1;
}
};
// some keycodes that seem to be platform/browser independant
var keycodes ={
BACKSPACE: 8,
TAB : 9,
ENTER : 13,
SHIFT : 16,
CTRL : 17,
CONTROL : 17,
ALT : 18,
ESC : 27,
SPACE : 32,
PGUP : 33,
PGDOWN : 34,
LEFT_ARROW: 37,
LEFTARROW: 37,
LEFT : 37,
UP_ARROW : 38,
UPARROW : 38,
UP : 38,
RIGHT_ARROW:39,
RIGHTARROW:39,
RIGHT : 39,
DOWN_ARROW: 40,
DOWNARROW: 40,
DOWN : 40,
};
points_to_pixels = function (points) {
// A reasonably good way of converting between points and pixels.
var test = $('<div style="display: none; width: 10000pt; padding:0; border:0;"></div>');
$(body).append(test);
var pixel_per_point = test.width()/10000;
test.remove();
return Math.floor(points*pixel_per_point);
}
return {
uuid : uuid,
fixConsole : fixConsole,
keycodes : keycodes,
grow : grow,
fixCarriageReturn : fixCarriageReturn,
points_to_pixels : points_to_pixels
};
}(IPython));