| 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 |