equal
deleted
inserted
replaced
1 /* Author: Makarius |
1 /* Author: Makarius |
2 |
2 |
3 Misc library functions for VSCode. |
3 Misc library functions for VSCode. |
4 */ |
4 */ |
5 |
5 |
6 import {Isabelle_Workspace} from './isabelle_filesystem/isabelle_workspace' |
|
7 import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode' |
6 import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode' |
8 |
7 |
9 |
8 |
10 /* files */ |
9 /* files */ |
11 |
10 |
12 export function is_file(uri: Uri): boolean |
11 export function is_file(uri: Uri): boolean |
13 { |
12 { |
14 return uri.scheme === "file" || uri.scheme === Isabelle_Workspace.scheme |
13 return uri.scheme === "file" |
15 } |
14 } |
16 |
15 |
17 export function find_file_editor(uri: Uri): TextEditor | undefined |
16 export function find_file_editor(uri: Uri): TextEditor | undefined |
18 { |
17 { |
19 function check(editor: TextEditor): boolean |
18 function check(editor: TextEditor): boolean |