(message, className)
| 164 | } |
| 165 | |
| 166 | function print(message, className) { |
| 167 | var mode = user; |
| 168 | var ln = line; |
| 169 | user = false; |
| 170 | |
| 171 | message = String(message); |
| 172 | var text = mirror.getLine(line); |
| 173 | message = message.replace(/\n/g, '\r') + '\n'; |
| 174 | |
| 175 | if (text) { |
| 176 | mirror.setMarker(line, ""); |
| 177 | var cursor = mirror.getCursor().ch; |
| 178 | } |
| 179 | |
| 180 | mirror.setLine(line++, message); |
| 181 | if (className) mirror.markText({line: ln, ch: 0}, {line: ln, ch: message.length}, className); |
| 182 | |
| 183 | if (text) { |
| 184 | mirror.setLine(line, text); |
| 185 | mirror.setMarker(line, ">>>"); |
| 186 | mirror.setCursor({line: line, ch: cursor}); |
| 187 | } |
| 188 | |
| 189 | setTimeout(function () { |
| 190 | user = mode; |
| 191 | }, 0); |
| 192 | } |
| 193 | |
| 194 | function setMode(mode) { |
| 195 | mirror.setOption("mode", mode); |
no outgoing calls