| 220 | showFileInfo(url); |
| 221 | }, |
| 222 | async goto() { |
| 223 | const lastLine = editorManager.editor?.state?.doc?.lines; |
| 224 | const message = lastLine |
| 225 | ? `${strings["enter line number"]} (1..${lastLine})` |
| 226 | : strings["enter line number"]; |
| 227 | const res = await prompt(message, "", "number", { |
| 228 | placeholder: "line.column", |
| 229 | }); |
| 230 | |
| 231 | if (!res) return; |
| 232 | const [lineStr, colStr] = String(res).split("."); |
| 233 | editorManager.editor.gotoLine(lineStr, colStr); |
| 234 | }, |
| 235 | async "new-file"() { |
| 236 | let filename = await prompt(strings["enter file name"], "", "filename", { |
| 237 | match: config.FILE_NAME_REGEX, |