##// END OF EJS Templates
fix missing comma
Min RK -
Show More
@@ -1,149 +1,149 b''
1 1 //----------------------------------------------------------------------------
2 2 // Copyright (C) 2008-2011 The IPython Development Team
3 3 //
4 4 // Distributed under the terms of the BSD License. The full license is in
5 5 // the file COPYING, distributed as part of this software.
6 6 //----------------------------------------------------------------------------
7 7
8 8 //============================================================================
9 9 // Utilities
10 10 //============================================================================
11 11
12 12 IPython.namespace('IPython.utils');
13 13
14 14 IPython.utils = (function (IPython) {
15 15
16 16 var uuid = function () {
17 17 // http://www.ietf.org/rfc/rfc4122.txt
18 18 var s = [];
19 19 var hexDigits = "0123456789ABCDEF";
20 20 for (var i = 0; i < 32; i++) {
21 21 s[i] = hexDigits.substr(Math.floor(Math.random() * 0x10), 1);
22 22 }
23 23 s[12] = "4"; // bits 12-15 of the time_hi_and_version field to 0010
24 24 s[16] = hexDigits.substr((s[16] & 0x3) | 0x8, 1); // bits 6-7 of the clock_seq_hi_and_reserved to 01
25 25
26 26 var uuid = s.join("");
27 27 return uuid;
28 28 };
29 29
30 30
31 31 //Fix raw text to parse correctly in crazy XML
32 32 function xmlencode(string) {
33 33 return string.replace(/\&/g,'&'+'amp;')
34 34 .replace(/</g,'&'+'lt;')
35 35 .replace(/>/g,'&'+'gt;')
36 36 .replace(/\'/g,'&'+'apos;')
37 37 .replace(/\"/g,'&'+'quot;')
38 38 .replace(/`/g,'&'+'#96;');
39 39 }
40 40
41 41
42 42 //Map from terminal commands to CSS classes
43 43 ansi_colormap = {
44 44 "30":"ansiblack", "31":"ansired",
45 45 "32":"ansigreen", "33":"ansiyellow",
46 46 "34":"ansiblue", "35":"ansipurple","36":"ansicyan",
47 47 "37":"ansigrey", "01":"ansibold"
48 48 };
49 49
50 50 // Transform ANSI color escape codes into HTML <span> tags with css
51 51 // classes listed in the above ansi_colormap object. The actual color used
52 52 // are set in the css file.
53 53 function fixConsole(txt) {
54 54 txt = xmlencode(txt);
55 55 var re = /\033\[([\dA-Fa-f;]*?)m/;
56 56 var opened = false;
57 57 var cmds = [];
58 58 var opener = "";
59 59 var closer = "";
60 60 while (re.test(txt)) {
61 61 var cmds = txt.match(re)[1].split(";");
62 62 closer = opened?"</span>":"";
63 63 opened = cmds.length > 1 || cmds[0] != 0;
64 64 var rep = [];
65 65 for (var i in cmds)
66 66 if (typeof(ansi_colormap[cmds[i]]) != "undefined")
67 67 rep.push(ansi_colormap[cmds[i]]);
68 68 opener = rep.length > 0?"<span class=\""+rep.join(" ")+"\">":"";
69 69 txt = txt.replace(re, closer + opener);
70 70 }
71 71 if (opened) txt += "</span>";
72 72 return txt;
73 73 }
74 74
75 75 // Remove chunks that should be overridden by the effect of
76 76 // carriage return characters
77 77 function fixCarriageReturn(txt) {
78 78 tmp = txt;
79 79 do {
80 80 txt = tmp;
81 81 tmp = txt.replace(/^.*\r(?!\n)/gm, '');
82 82 } while (tmp.length < txt.length);
83 83 return txt;
84 84 }
85 85
86 86 grow = function(element) {
87 87 // Grow the cell by hand. This is used upon reloading from JSON, when the
88 88 // autogrow handler is not called.
89 89 var dom = element.get(0);
90 90 var lines_count = 0;
91 91 // modified split rule from
92 92 // http://stackoverflow.com/questions/2035910/how-to-get-the-number-of-lines-in-a-textarea/2036424#2036424
93 93 var lines = dom.value.split(/\r|\r\n|\n/);
94 94 lines_count = lines.length;
95 95 if (lines_count >= 1) {
96 96 dom.rows = lines_count;
97 97 } else {
98 98 dom.rows = 1;
99 99 }
100 100 };
101 101
102 102 // some keycodes that seem to be platform/browser independant
103 103 var keycodes ={
104 104 BACKSPACE: 8,
105 105 TAB : 9,
106 106 ENTER : 13,
107 107 SHIFT : 16,
108 108 CTRL : 17,
109 109 CONTROL : 17,
110 110 ALT : 18,
111 111 ESC : 27,
112 112 SPACE : 32,
113 113 PGUP : 33,
114 114 PGDOWN : 34,
115 115 LEFT_ARROW: 37,
116 116 LEFTARROW: 37,
117 117 LEFT : 37,
118 118 UP_ARROW : 38,
119 119 UPARROW : 38,
120 120 UP : 38,
121 121 RIGHT_ARROW:39,
122 122 RIGHTARROW:39,
123 123 RIGHT : 39,
124 124 DOWN_ARROW: 40,
125 125 DOWNARROW: 40,
126 126 DOWN : 40,
127 127 };
128 128
129 129
130 130 points_to_pixels = function (points) {
131 131 // A reasonably good way of converting between points and pixels.
132 132 var test = $('<div style="display: none; width: 10000pt; padding:0; border:0;"></div>');
133 133 $(body).append(test);
134 134 var pixel_per_point = test.width()/10000;
135 135 test.remove();
136 136 return Math.floor(points*pixel_per_point);
137 137 }
138 138
139 139
140 140 return {
141 141 uuid : uuid,
142 142 fixConsole : fixConsole,
143 143 keycodes : keycodes,
144 144 grow : grow,
145 fixCarriageReturn : fixCarriageReturn
145 fixCarriageReturn : fixCarriageReturn,
146 146 points_to_pixels : points_to_pixels
147 147 };
148 148
149 149 }(IPython));
General Comments 0
You need to be logged in to leave comments. Login now