(cm)
| 2204 | // something in the input textarea, we poll faster, to ensure that |
| 2205 | // the change appears on the screen quickly. |
| 2206 | function fastPoll(cm) { |
| 2207 | var missed = false; |
| 2208 | cm.display.pollingFast = true; |
| 2209 | function p() { |
| 2210 | var changed = readInput(cm); |
| 2211 | if (!changed && !missed) {missed = true; cm.display.poll.set(60, p);} |
| 2212 | else {cm.display.pollingFast = false; slowPoll(cm);} |
| 2213 | } |
| 2214 | cm.display.poll.set(20, p); |
| 2215 | } |
| 2216 | |
| 2217 | // Read input from the textarea, and update the document to match. |
| 2218 | // When something is selected, it is present in the textarea, and |
no outgoing calls
no test coverage detected
searching dependent graphs…