OLD | NEW |
1 /** | 1 /** |
2 * Common JS that talks XHR back to the server and runs the code and receives | 2 * Common JS that talks XHR back to the server and runs the code and receives |
3 * the results. | 3 * the results. |
4 */ | 4 */ |
5 | 5 |
6 /** | 6 /** |
7 * A polyfill for HTML Templates. | 7 * A polyfill for HTML Templates. |
8 * | 8 * |
9 * This just adds in the content attribute, it doesn't stop scripts | 9 * This just adds in the content attribute, it doesn't stop scripts |
10 * from running nor does it stop other side-effects. | 10 * from running nor does it stop other side-effects. |
(...skipping 157 matching lines...) Expand 10 before | Expand all | Expand 10 after Loading... |
168 var embedButton = document.getElementById('embedButton'); | 168 var embedButton = document.getElementById('embedButton'); |
169 var code = document.getElementById('code'); | 169 var code = document.getElementById('code'); |
170 var output = document.getElementById('output'); | 170 var output = document.getElementById('output'); |
171 var stdout = document.getElementById('stdout'); | 171 var stdout = document.getElementById('stdout'); |
172 var img = document.getElementById('img'); | 172 var img = document.getElementById('img'); |
173 var tryHistory = document.getElementById('tryHistory'); | 173 var tryHistory = document.getElementById('tryHistory'); |
174 var parser = new DOMParser(); | 174 var parser = new DOMParser(); |
175 var tryTemplate = document.getElementById('tryTemplate'); | 175 var tryTemplate = document.getElementById('tryTemplate'); |
176 | 176 |
177 var editor = CodeMirror.fromTextArea(code, { | 177 var editor = CodeMirror.fromTextArea(code, { |
178 theme: "ambiance", | 178 theme: "default", |
179 lineNumbers: true, | 179 lineNumbers: true, |
180 matchBrackets: true, | 180 matchBrackets: true, |
181 mode: "text/x-c++src", | 181 mode: "text/x-c++src", |
182 indentUnit: 4, | 182 indentUnit: 4, |
183 }); | 183 }); |
184 | 184 |
185 // Match the initial textarea size. | 185 // Match the initial textarea size. |
186 editor.setSize(editor.defaultCharWidth() * code.cols, | 186 editor.setSize(editor.defaultCharWidth() * code.cols, |
187 editor.defaultTextHeight() * code.rows); | 187 editor.defaultTextHeight() * code.rows); |
188 | 188 |
(...skipping 147 matching lines...) Expand 10 before | Expand all | Expand 10 after Loading... |
336 | 336 |
337 | 337 |
338 // Add the images to the history if we are on a workspace page. | 338 // Add the images to the history if we are on a workspace page. |
339 if (tryHistory && history) { | 339 if (tryHistory && history) { |
340 for (var i=0; i<history.length; i++) { | 340 for (var i=0; i<history.length; i++) { |
341 addToHistory(history[i].hash, '/i/'+history[i].hash+'.png'); | 341 addToHistory(history[i].hash, '/i/'+history[i].hash+'.png'); |
342 } | 342 } |
343 } | 343 } |
344 | 344 |
345 })(workspaceName); | 345 })(workspaceName); |
OLD | NEW |