| 61 | else if (confirm(shortText)) fs[0](); |
| 62 | } |
| 63 | function parseQuery(query) { |
| 64 | var isRE = query.match(/^\/(.*)\/([a-z]*)$/); |
| 65 | if (isRE) { |
| 66 | try { query = new RegExp(isRE[1], isRE[2].indexOf("i") == -1 ? "" : "i"); } |
| 67 | catch(e) {} // Not a regular expression after all, do a string search |
| 68 | } |
| 69 | if (typeof query == "string" ? query == "" : query.test("")) |
| 70 | query = /x^/; |
| 71 | return query; |
| 72 | } |
| 73 | var queryDialog = |
| 74 | 'Search: <input type="text" style="width: 10em" class="CodeMirror-search-field"/> <span style="color: #888" class="CodeMirror-search-hint">(Use /re/ syntax for regexp search)</span>'; |
| 75 | function doSearch(cm, rev) { |