##// END OF EJS Templates
Merge pull request #3965 from andreabedini/patch-1...
Min RK -
r12096:ad683da4 merge
parent child Browse files
Show More
@@ -1,390 +1,390 b''
1 //----------------------------------------------------------------------------
1 //----------------------------------------------------------------------------
2 // Copyright (C) 2008-2012 The IPython Development Team
2 // Copyright (C) 2008-2012 The IPython Development Team
3 //
3 //
4 // Distributed under the terms of the BSD License. The full license is in
4 // Distributed under the terms of the BSD License. The full license is in
5 // the file COPYING, distributed as part of this software.
5 // the file COPYING, distributed as part of this software.
6 //----------------------------------------------------------------------------
6 //----------------------------------------------------------------------------
7
7
8 //============================================================================
8 //============================================================================
9 // Utilities
9 // Utilities
10 //============================================================================
10 //============================================================================
11 IPython.namespace('IPython.utils');
11 IPython.namespace('IPython.utils');
12
12
13 IPython.utils = (function (IPython) {
13 IPython.utils = (function (IPython) {
14
14
15 //============================================================================
15 //============================================================================
16 // Cross-browser RegEx Split
16 // Cross-browser RegEx Split
17 //============================================================================
17 //============================================================================
18
18
19 // This code has been MODIFIED from the code licensed below to not replace the
19 // This code has been MODIFIED from the code licensed below to not replace the
20 // default browser split. The license is reproduced here.
20 // default browser split. The license is reproduced here.
21
21
22 // see http://blog.stevenlevithan.com/archives/cross-browser-split for more info:
22 // see http://blog.stevenlevithan.com/archives/cross-browser-split for more info:
23 /*!
23 /*!
24 * Cross-Browser Split 1.1.1
24 * Cross-Browser Split 1.1.1
25 * Copyright 2007-2012 Steven Levithan <stevenlevithan.com>
25 * Copyright 2007-2012 Steven Levithan <stevenlevithan.com>
26 * Available under the MIT License
26 * Available under the MIT License
27 * ECMAScript compliant, uniform cross-browser split method
27 * ECMAScript compliant, uniform cross-browser split method
28 */
28 */
29
29
30 /**
30 /**
31 * Splits a string into an array of strings using a regex or string
31 * Splits a string into an array of strings using a regex or string
32 * separator. Matches of the separator are not included in the result array.
32 * separator. Matches of the separator are not included in the result array.
33 * However, if `separator` is a regex that contains capturing groups,
33 * However, if `separator` is a regex that contains capturing groups,
34 * backreferences are spliced into the result each time `separator` is
34 * backreferences are spliced into the result each time `separator` is
35 * matched. Fixes browser bugs compared to the native
35 * matched. Fixes browser bugs compared to the native
36 * `String.prototype.split` and can be used reliably cross-browser.
36 * `String.prototype.split` and can be used reliably cross-browser.
37 * @param {String} str String to split.
37 * @param {String} str String to split.
38 * @param {RegExp|String} separator Regex or string to use for separating
38 * @param {RegExp|String} separator Regex or string to use for separating
39 * the string.
39 * the string.
40 * @param {Number} [limit] Maximum number of items to include in the result
40 * @param {Number} [limit] Maximum number of items to include in the result
41 * array.
41 * array.
42 * @returns {Array} Array of substrings.
42 * @returns {Array} Array of substrings.
43 * @example
43 * @example
44 *
44 *
45 * // Basic use
45 * // Basic use
46 * regex_split('a b c d', ' ');
46 * regex_split('a b c d', ' ');
47 * // -> ['a', 'b', 'c', 'd']
47 * // -> ['a', 'b', 'c', 'd']
48 *
48 *
49 * // With limit
49 * // With limit
50 * regex_split('a b c d', ' ', 2);
50 * regex_split('a b c d', ' ', 2);
51 * // -> ['a', 'b']
51 * // -> ['a', 'b']
52 *
52 *
53 * // Backreferences in result array
53 * // Backreferences in result array
54 * regex_split('..word1 word2..', /([a-z]+)(\d+)/i);
54 * regex_split('..word1 word2..', /([a-z]+)(\d+)/i);
55 * // -> ['..', 'word', '1', ' ', 'word', '2', '..']
55 * // -> ['..', 'word', '1', ' ', 'word', '2', '..']
56 */
56 */
57 var regex_split = function (str, separator, limit) {
57 var regex_split = function (str, separator, limit) {
58 // If `separator` is not a regex, use `split`
58 // If `separator` is not a regex, use `split`
59 if (Object.prototype.toString.call(separator) !== "[object RegExp]") {
59 if (Object.prototype.toString.call(separator) !== "[object RegExp]") {
60 return split.call(str, separator, limit);
60 return split.call(str, separator, limit);
61 }
61 }
62 var output = [],
62 var output = [],
63 flags = (separator.ignoreCase ? "i" : "") +
63 flags = (separator.ignoreCase ? "i" : "") +
64 (separator.multiline ? "m" : "") +
64 (separator.multiline ? "m" : "") +
65 (separator.extended ? "x" : "") + // Proposed for ES6
65 (separator.extended ? "x" : "") + // Proposed for ES6
66 (separator.sticky ? "y" : ""), // Firefox 3+
66 (separator.sticky ? "y" : ""), // Firefox 3+
67 lastLastIndex = 0,
67 lastLastIndex = 0,
68 // Make `global` and avoid `lastIndex` issues by working with a copy
68 // Make `global` and avoid `lastIndex` issues by working with a copy
69 separator = new RegExp(separator.source, flags + "g"),
69 separator = new RegExp(separator.source, flags + "g"),
70 separator2, match, lastIndex, lastLength;
70 separator2, match, lastIndex, lastLength;
71 str += ""; // Type-convert
71 str += ""; // Type-convert
72
72
73 var compliantExecNpcg = typeof(/()??/.exec("")[1]) === "undefined";
73 var compliantExecNpcg = typeof(/()??/.exec("")[1]) === "undefined";
74 if (!compliantExecNpcg) {
74 if (!compliantExecNpcg) {
75 // Doesn't need flags gy, but they don't hurt
75 // Doesn't need flags gy, but they don't hurt
76 separator2 = new RegExp("^" + separator.source + "$(?!\\s)", flags);
76 separator2 = new RegExp("^" + separator.source + "$(?!\\s)", flags);
77 }
77 }
78 /* Values for `limit`, per the spec:
78 /* Values for `limit`, per the spec:
79 * If undefined: 4294967295 // Math.pow(2, 32) - 1
79 * If undefined: 4294967295 // Math.pow(2, 32) - 1
80 * If 0, Infinity, or NaN: 0
80 * If 0, Infinity, or NaN: 0
81 * If positive number: limit = Math.floor(limit); if (limit > 4294967295) limit -= 4294967296;
81 * If positive number: limit = Math.floor(limit); if (limit > 4294967295) limit -= 4294967296;
82 * If negative number: 4294967296 - Math.floor(Math.abs(limit))
82 * If negative number: 4294967296 - Math.floor(Math.abs(limit))
83 * If other: Type-convert, then use the above rules
83 * If other: Type-convert, then use the above rules
84 */
84 */
85 limit = typeof(limit) === "undefined" ?
85 limit = typeof(limit) === "undefined" ?
86 -1 >>> 0 : // Math.pow(2, 32) - 1
86 -1 >>> 0 : // Math.pow(2, 32) - 1
87 limit >>> 0; // ToUint32(limit)
87 limit >>> 0; // ToUint32(limit)
88 while (match = separator.exec(str)) {
88 while (match = separator.exec(str)) {
89 // `separator.lastIndex` is not reliable cross-browser
89 // `separator.lastIndex` is not reliable cross-browser
90 lastIndex = match.index + match[0].length;
90 lastIndex = match.index + match[0].length;
91 if (lastIndex > lastLastIndex) {
91 if (lastIndex > lastLastIndex) {
92 output.push(str.slice(lastLastIndex, match.index));
92 output.push(str.slice(lastLastIndex, match.index));
93 // Fix browsers whose `exec` methods don't consistently return `undefined` for
93 // Fix browsers whose `exec` methods don't consistently return `undefined` for
94 // nonparticipating capturing groups
94 // nonparticipating capturing groups
95 if (!compliantExecNpcg && match.length > 1) {
95 if (!compliantExecNpcg && match.length > 1) {
96 match[0].replace(separator2, function () {
96 match[0].replace(separator2, function () {
97 for (var i = 1; i < arguments.length - 2; i++) {
97 for (var i = 1; i < arguments.length - 2; i++) {
98 if (typeof(arguments[i]) === "undefined") {
98 if (typeof(arguments[i]) === "undefined") {
99 match[i] = undefined;
99 match[i] = undefined;
100 }
100 }
101 }
101 }
102 });
102 });
103 }
103 }
104 if (match.length > 1 && match.index < str.length) {
104 if (match.length > 1 && match.index < str.length) {
105 Array.prototype.push.apply(output, match.slice(1));
105 Array.prototype.push.apply(output, match.slice(1));
106 }
106 }
107 lastLength = match[0].length;
107 lastLength = match[0].length;
108 lastLastIndex = lastIndex;
108 lastLastIndex = lastIndex;
109 if (output.length >= limit) {
109 if (output.length >= limit) {
110 break;
110 break;
111 }
111 }
112 }
112 }
113 if (separator.lastIndex === match.index) {
113 if (separator.lastIndex === match.index) {
114 separator.lastIndex++; // Avoid an infinite loop
114 separator.lastIndex++; // Avoid an infinite loop
115 }
115 }
116 }
116 }
117 if (lastLastIndex === str.length) {
117 if (lastLastIndex === str.length) {
118 if (lastLength || !separator.test("")) {
118 if (lastLength || !separator.test("")) {
119 output.push("");
119 output.push("");
120 }
120 }
121 } else {
121 } else {
122 output.push(str.slice(lastLastIndex));
122 output.push(str.slice(lastLastIndex));
123 }
123 }
124 return output.length > limit ? output.slice(0, limit) : output;
124 return output.length > limit ? output.slice(0, limit) : output;
125 };
125 };
126
126
127 //============================================================================
127 //============================================================================
128 // End contributed Cross-browser RegEx Split
128 // End contributed Cross-browser RegEx Split
129 //============================================================================
129 //============================================================================
130
130
131
131
132 var uuid = function () {
132 var uuid = function () {
133 // http://www.ietf.org/rfc/rfc4122.txt
133 // http://www.ietf.org/rfc/rfc4122.txt
134 var s = [];
134 var s = [];
135 var hexDigits = "0123456789ABCDEF";
135 var hexDigits = "0123456789ABCDEF";
136 for (var i = 0; i < 32; i++) {
136 for (var i = 0; i < 32; i++) {
137 s[i] = hexDigits.substr(Math.floor(Math.random() * 0x10), 1);
137 s[i] = hexDigits.substr(Math.floor(Math.random() * 0x10), 1);
138 }
138 }
139 s[12] = "4"; // bits 12-15 of the time_hi_and_version field to 0010
139 s[12] = "4"; // bits 12-15 of the time_hi_and_version field to 0010
140 s[16] = hexDigits.substr((s[16] & 0x3) | 0x8, 1); // bits 6-7 of the clock_seq_hi_and_reserved to 01
140 s[16] = hexDigits.substr((s[16] & 0x3) | 0x8, 1); // bits 6-7 of the clock_seq_hi_and_reserved to 01
141
141
142 var uuid = s.join("");
142 var uuid = s.join("");
143 return uuid;
143 return uuid;
144 };
144 };
145
145
146
146
147 //Fix raw text to parse correctly in crazy XML
147 //Fix raw text to parse correctly in crazy XML
148 function xmlencode(string) {
148 function xmlencode(string) {
149 return string.replace(/\&/g,'&'+'amp;')
149 return string.replace(/\&/g,'&'+'amp;')
150 .replace(/</g,'&'+'lt;')
150 .replace(/</g,'&'+'lt;')
151 .replace(/>/g,'&'+'gt;')
151 .replace(/>/g,'&'+'gt;')
152 .replace(/\'/g,'&'+'apos;')
152 .replace(/\'/g,'&'+'apos;')
153 .replace(/\"/g,'&'+'quot;')
153 .replace(/\"/g,'&'+'quot;')
154 .replace(/`/g,'&'+'#96;');
154 .replace(/`/g,'&'+'#96;');
155 }
155 }
156
156
157
157
158 //Map from terminal commands to CSS classes
158 //Map from terminal commands to CSS classes
159 var ansi_colormap = {
159 var ansi_colormap = {
160 "01":"ansibold",
160 "01":"ansibold",
161
161
162 "30":"ansiblack",
162 "30":"ansiblack",
163 "31":"ansired",
163 "31":"ansired",
164 "32":"ansigreen",
164 "32":"ansigreen",
165 "33":"ansiyellow",
165 "33":"ansiyellow",
166 "34":"ansiblue",
166 "34":"ansiblue",
167 "35":"ansipurple",
167 "35":"ansipurple",
168 "36":"ansicyan",
168 "36":"ansicyan",
169 "37":"ansigray",
169 "37":"ansigray",
170
170
171 "40":"ansibgblack",
171 "40":"ansibgblack",
172 "41":"ansibgred",
172 "41":"ansibgred",
173 "42":"ansibggreen",
173 "42":"ansibggreen",
174 "44":"ansibgyellow",
174 "43":"ansibgyellow",
175 "44":"ansibgblue",
175 "44":"ansibgblue",
176 "45":"ansibgpurple",
176 "45":"ansibgpurple",
177 "46":"ansibgcyan",
177 "46":"ansibgcyan",
178 "47":"ansibggray"
178 "47":"ansibggray"
179 };
179 };
180
180
181 function _process_numbers(attrs, numbers) {
181 function _process_numbers(attrs, numbers) {
182 // process ansi escapes
182 // process ansi escapes
183 var n = numbers.shift();
183 var n = numbers.shift();
184 if (ansi_colormap[n]) {
184 if (ansi_colormap[n]) {
185 if ( ! attrs["class"] ) {
185 if ( ! attrs["class"] ) {
186 attrs["class"] = ansi_colormap[n];
186 attrs["class"] = ansi_colormap[n];
187 } else {
187 } else {
188 attrs["class"] += " " + ansi_colormap[n];
188 attrs["class"] += " " + ansi_colormap[n];
189 }
189 }
190 } else if (n == "38" || n == "48") {
190 } else if (n == "38" || n == "48") {
191 // VT100 256 color or 24 bit RGB
191 // VT100 256 color or 24 bit RGB
192 if (numbers.length < 2) {
192 if (numbers.length < 2) {
193 console.log("Not enough fields for VT100 color", numbers);
193 console.log("Not enough fields for VT100 color", numbers);
194 return;
194 return;
195 }
195 }
196
196
197 var index_or_rgb = numbers.shift();
197 var index_or_rgb = numbers.shift();
198 var r,g,b;
198 var r,g,b;
199 if (index_or_rgb == "5") {
199 if (index_or_rgb == "5") {
200 // 256 color
200 // 256 color
201 var idx = parseInt(numbers.shift());
201 var idx = parseInt(numbers.shift());
202 if (idx < 16) {
202 if (idx < 16) {
203 // indexed ANSI
203 // indexed ANSI
204 // ignore bright / non-bright distinction
204 // ignore bright / non-bright distinction
205 idx = idx % 8;
205 idx = idx % 8;
206 var ansiclass = ansi_colormap[n[0] + (idx % 8).toString()];
206 var ansiclass = ansi_colormap[n[0] + (idx % 8).toString()];
207 if ( ! attrs["class"] ) {
207 if ( ! attrs["class"] ) {
208 attrs["class"] = ansiclass;
208 attrs["class"] = ansiclass;
209 } else {
209 } else {
210 attrs["class"] += " " + ansiclass;
210 attrs["class"] += " " + ansiclass;
211 }
211 }
212 return;
212 return;
213 } else if (idx < 232) {
213 } else if (idx < 232) {
214 // 216 color 6x6x6 RGB
214 // 216 color 6x6x6 RGB
215 idx = idx - 16;
215 idx = idx - 16;
216 b = idx % 6;
216 b = idx % 6;
217 g = Math.floor(idx / 6) % 6;
217 g = Math.floor(idx / 6) % 6;
218 r = Math.floor(idx / 36) % 6;
218 r = Math.floor(idx / 36) % 6;
219 // convert to rgb
219 // convert to rgb
220 r = (r * 51);
220 r = (r * 51);
221 g = (g * 51);
221 g = (g * 51);
222 b = (b * 51);
222 b = (b * 51);
223 } else {
223 } else {
224 // grayscale
224 // grayscale
225 idx = idx - 231;
225 idx = idx - 231;
226 // it's 1-24 and should *not* include black or white,
226 // it's 1-24 and should *not* include black or white,
227 // so a 26 point scale
227 // so a 26 point scale
228 r = g = b = Math.floor(idx * 256 / 26);
228 r = g = b = Math.floor(idx * 256 / 26);
229 }
229 }
230 } else if (index_or_rgb == "2") {
230 } else if (index_or_rgb == "2") {
231 // Simple 24 bit RGB
231 // Simple 24 bit RGB
232 if (numbers.length > 3) {
232 if (numbers.length > 3) {
233 console.log("Not enough fields for RGB", numbers);
233 console.log("Not enough fields for RGB", numbers);
234 return;
234 return;
235 }
235 }
236 r = numbers.shift();
236 r = numbers.shift();
237 g = numbers.shift();
237 g = numbers.shift();
238 b = numbers.shift();
238 b = numbers.shift();
239 } else {
239 } else {
240 console.log("unrecognized control", numbers);
240 console.log("unrecognized control", numbers);
241 return;
241 return;
242 }
242 }
243 if (r !== undefined) {
243 if (r !== undefined) {
244 // apply the rgb color
244 // apply the rgb color
245 var line;
245 var line;
246 if (n == "38") {
246 if (n == "38") {
247 line = "color: ";
247 line = "color: ";
248 } else {
248 } else {
249 line = "background-color: ";
249 line = "background-color: ";
250 }
250 }
251 line = line + "rgb(" + r + "," + g + "," + b + ");"
251 line = line + "rgb(" + r + "," + g + "," + b + ");"
252 if ( !attrs["style"] ) {
252 if ( !attrs["style"] ) {
253 attrs["style"] = line;
253 attrs["style"] = line;
254 } else {
254 } else {
255 attrs["style"] += " " + line;
255 attrs["style"] += " " + line;
256 }
256 }
257 }
257 }
258 }
258 }
259 }
259 }
260
260
261 function ansispan(str) {
261 function ansispan(str) {
262 // ansispan function adapted from github.com/mmalecki/ansispan (MIT License)
262 // ansispan function adapted from github.com/mmalecki/ansispan (MIT License)
263 // regular ansi escapes (using the table above)
263 // regular ansi escapes (using the table above)
264 return str.replace(/\033\[(0?[01]|22|39)?([;\d]+)?m/g, function(match, prefix, pattern) {
264 return str.replace(/\033\[(0?[01]|22|39)?([;\d]+)?m/g, function(match, prefix, pattern) {
265 if (!pattern) {
265 if (!pattern) {
266 // [(01|22|39|)m close spans
266 // [(01|22|39|)m close spans
267 return "</span>";
267 return "</span>";
268 }
268 }
269 // consume sequence of color escapes
269 // consume sequence of color escapes
270 var numbers = pattern.match(/\d+/g);
270 var numbers = pattern.match(/\d+/g);
271 var attrs = {};
271 var attrs = {};
272 while (numbers.length > 0) {
272 while (numbers.length > 0) {
273 _process_numbers(attrs, numbers);
273 _process_numbers(attrs, numbers);
274 }
274 }
275
275
276 var span = "<span ";
276 var span = "<span ";
277 for (var attr in attrs) {
277 for (var attr in attrs) {
278 var value = attrs[attr];
278 var value = attrs[attr];
279 span = span + " " + attr + '="' + attrs[attr] + '"';
279 span = span + " " + attr + '="' + attrs[attr] + '"';
280 }
280 }
281 return span + ">";
281 return span + ">";
282 });
282 });
283 };
283 };
284
284
285 // Transform ANSI color escape codes into HTML <span> tags with css
285 // Transform ANSI color escape codes into HTML <span> tags with css
286 // classes listed in the above ansi_colormap object. The actual color used
286 // classes listed in the above ansi_colormap object. The actual color used
287 // are set in the css file.
287 // are set in the css file.
288 function fixConsole(txt) {
288 function fixConsole(txt) {
289 txt = xmlencode(txt);
289 txt = xmlencode(txt);
290 var re = /\033\[([\dA-Fa-f;]*?)m/;
290 var re = /\033\[([\dA-Fa-f;]*?)m/;
291 var opened = false;
291 var opened = false;
292 var cmds = [];
292 var cmds = [];
293 var opener = "";
293 var opener = "";
294 var closer = "";
294 var closer = "";
295
295
296 // Strip all ANSI codes that are not color related. Matches
296 // Strip all ANSI codes that are not color related. Matches
297 // all ANSI codes that do not end with "m".
297 // all ANSI codes that do not end with "m".
298 var ignored_re = /(?=(\033\[[\d;=]*[a-ln-zA-Z]{1}))\1(?!m)/g;
298 var ignored_re = /(?=(\033\[[\d;=]*[a-ln-zA-Z]{1}))\1(?!m)/g;
299 txt = txt.replace(ignored_re, "");
299 txt = txt.replace(ignored_re, "");
300
300
301 // color ansi codes
301 // color ansi codes
302 txt = ansispan(txt);
302 txt = ansispan(txt);
303 return txt;
303 return txt;
304 }
304 }
305
305
306 // Remove chunks that should be overridden by the effect of
306 // Remove chunks that should be overridden by the effect of
307 // carriage return characters
307 // carriage return characters
308 function fixCarriageReturn(txt) {
308 function fixCarriageReturn(txt) {
309 var tmp = txt;
309 var tmp = txt;
310 do {
310 do {
311 txt = tmp;
311 txt = tmp;
312 tmp = txt.replace(/\r+\n/gm, '\n'); // \r followed by \n --> newline
312 tmp = txt.replace(/\r+\n/gm, '\n'); // \r followed by \n --> newline
313 tmp = tmp.replace(/^.*\r+/gm, ''); // Other \r --> clear line
313 tmp = tmp.replace(/^.*\r+/gm, ''); // Other \r --> clear line
314 } while (tmp.length < txt.length);
314 } while (tmp.length < txt.length);
315 return txt;
315 return txt;
316 }
316 }
317
317
318 // Locate any URLs and convert them to a anchor tag
318 // Locate any URLs and convert them to a anchor tag
319 function autoLinkUrls(txt) {
319 function autoLinkUrls(txt) {
320 return txt.replace(/(^|\s)(https?|ftp)(:[^'">\s]+)/gi,
320 return txt.replace(/(^|\s)(https?|ftp)(:[^'">\s]+)/gi,
321 "$1<a target=\"_blank\" href=\"$2$3\">$2$3</a>");
321 "$1<a target=\"_blank\" href=\"$2$3\">$2$3</a>");
322 }
322 }
323
323
324 // some keycodes that seem to be platform/browser independent
324 // some keycodes that seem to be platform/browser independent
325 var keycodes = {
325 var keycodes = {
326 BACKSPACE: 8,
326 BACKSPACE: 8,
327 TAB : 9,
327 TAB : 9,
328 ENTER : 13,
328 ENTER : 13,
329 SHIFT : 16,
329 SHIFT : 16,
330 CTRL : 17,
330 CTRL : 17,
331 CONTROL : 17,
331 CONTROL : 17,
332 ALT : 18,
332 ALT : 18,
333 CAPS_LOCK: 20,
333 CAPS_LOCK: 20,
334 ESC : 27,
334 ESC : 27,
335 SPACE : 32,
335 SPACE : 32,
336 PGUP : 33,
336 PGUP : 33,
337 PGDOWN : 34,
337 PGDOWN : 34,
338 END : 35,
338 END : 35,
339 HOME : 36,
339 HOME : 36,
340 LEFT_ARROW: 37,
340 LEFT_ARROW: 37,
341 LEFTARROW: 37,
341 LEFTARROW: 37,
342 LEFT : 37,
342 LEFT : 37,
343 UP_ARROW : 38,
343 UP_ARROW : 38,
344 UPARROW : 38,
344 UPARROW : 38,
345 UP : 38,
345 UP : 38,
346 RIGHT_ARROW:39,
346 RIGHT_ARROW:39,
347 RIGHTARROW:39,
347 RIGHTARROW:39,
348 RIGHT : 39,
348 RIGHT : 39,
349 DOWN_ARROW: 40,
349 DOWN_ARROW: 40,
350 DOWNARROW: 40,
350 DOWNARROW: 40,
351 DOWN : 40,
351 DOWN : 40,
352 // all three of these keys may be COMMAND on OS X:
352 // all three of these keys may be COMMAND on OS X:
353 LEFT_SUPER : 91,
353 LEFT_SUPER : 91,
354 RIGHT_SUPER : 92,
354 RIGHT_SUPER : 92,
355 COMMAND : 93,
355 COMMAND : 93,
356 };
356 };
357
357
358
358
359 var points_to_pixels = function (points) {
359 var points_to_pixels = function (points) {
360 // A reasonably good way of converting between points and pixels.
360 // A reasonably good way of converting between points and pixels.
361 var test = $('<div style="display: none; width: 10000pt; padding:0; border:0;"></div>');
361 var test = $('<div style="display: none; width: 10000pt; padding:0; border:0;"></div>');
362 $(body).append(test);
362 $(body).append(test);
363 var pixel_per_point = test.width()/10000;
363 var pixel_per_point = test.width()/10000;
364 test.remove();
364 test.remove();
365 return Math.floor(points*pixel_per_point);
365 return Math.floor(points*pixel_per_point);
366 };
366 };
367
367
368 // http://stackoverflow.com/questions/2400935/browser-detection-in-javascript
368 // http://stackoverflow.com/questions/2400935/browser-detection-in-javascript
369 browser = (function() {
369 browser = (function() {
370 var N= navigator.appName, ua= navigator.userAgent, tem;
370 var N= navigator.appName, ua= navigator.userAgent, tem;
371 var M= ua.match(/(opera|chrome|safari|firefox|msie)\/?\s*(\.?\d+(\.\d+)*)/i);
371 var M= ua.match(/(opera|chrome|safari|firefox|msie)\/?\s*(\.?\d+(\.\d+)*)/i);
372 if (M && (tem= ua.match(/version\/([\.\d]+)/i))!= null) M[2]= tem[1];
372 if (M && (tem= ua.match(/version\/([\.\d]+)/i))!= null) M[2]= tem[1];
373 M= M? [M[1], M[2]]: [N, navigator.appVersion,'-?'];
373 M= M? [M[1], M[2]]: [N, navigator.appVersion,'-?'];
374 return M;
374 return M;
375 })();
375 })();
376
376
377
377
378 return {
378 return {
379 regex_split : regex_split,
379 regex_split : regex_split,
380 uuid : uuid,
380 uuid : uuid,
381 fixConsole : fixConsole,
381 fixConsole : fixConsole,
382 keycodes : keycodes,
382 keycodes : keycodes,
383 fixCarriageReturn : fixCarriageReturn,
383 fixCarriageReturn : fixCarriageReturn,
384 autoLinkUrls : autoLinkUrls,
384 autoLinkUrls : autoLinkUrls,
385 points_to_pixels : points_to_pixels,
385 points_to_pixels : points_to_pixels,
386 browser : browser
386 browser : browser
387 };
387 };
388
388
389 }(IPython));
389 }(IPython));
390
390
General Comments 0
You need to be logged in to leave comments. Login now