author | wenzelm |
Sat, 02 Sep 2017 17:21:52 +0200 | |
changeset 66598 | e2671e8c476f |
parent 66215 | 9a8b6b86350c |
child 75126 | da1108a6d249 |
permissions | -rw-r--r-- |
65966 | 1 |
'use strict'; |
2 |
||
65970 | 3 |
import * as os from 'os'; |
66214 | 4 |
import { TextEditor, Uri, ViewColumn, workspace, window } from 'vscode' |
65968 | 5 |
|
6 |
||
66070
65a68dcd95c3
dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents:
65983
diff
changeset
|
7 |
/* regular expressions */ |
65a68dcd95c3
dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents:
65983
diff
changeset
|
8 |
|
65a68dcd95c3
dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents:
65983
diff
changeset
|
9 |
export function escape_regex(s: string): string |
65a68dcd95c3
dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents:
65983
diff
changeset
|
10 |
{ |
65a68dcd95c3
dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents:
65983
diff
changeset
|
11 |
return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&") |
65a68dcd95c3
dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents:
65983
diff
changeset
|
12 |
} |
65a68dcd95c3
dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents:
65983
diff
changeset
|
13 |
|
65a68dcd95c3
dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents:
65983
diff
changeset
|
14 |
|
65970 | 15 |
/* platform information */ |
16 |
||
17 |
export function platform_is_windows(): boolean |
|
18 |
{ |
|
19 |
return os.type().startsWith("Windows") |
|
20 |
} |
|
21 |
||
22 |
||
66214 | 23 |
/* files */ |
65972 | 24 |
|
25 |
export function is_file(uri: Uri): boolean |
|
26 |
{ |
|
27 |
return uri.scheme === "file" |
|
28 |
} |
|
29 |
||
66214 | 30 |
export function find_file_editor(uri: Uri): TextEditor | undefined |
31 |
{ |
|
66215
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66214
diff
changeset
|
32 |
function check(editor: TextEditor): boolean |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66214
diff
changeset
|
33 |
{ return editor && is_file(editor.document.uri) && editor.document.uri.fsPath === uri.fsPath } |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66214
diff
changeset
|
34 |
|
66214 | 35 |
if (is_file(uri)) { |
66215
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66214
diff
changeset
|
36 |
if (check(window.activeTextEditor)) return window.activeTextEditor |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66214
diff
changeset
|
37 |
else return window.visibleTextEditors.find(check) |
66214 | 38 |
} |
39 |
else return undefined |
|
40 |
} |
|
41 |
||
42 |
||
65968 | 43 |
/* Isabelle configuration */ |
65966 | 44 |
|
65968 | 45 |
export function get_configuration<T>(name: string): T |
46 |
{ |
|
47 |
return workspace.getConfiguration("isabelle").get<T>(name) |
|
48 |
} |
|
49 |
||
50 |
export function get_color(color: string, light: boolean): string |
|
51 |
{ |
|
52 |
const config = color + (light ? "_light" : "_dark") + "_color" |
|
53 |
return get_configuration<string>(config) |
|
54 |
} |
|
66081 | 55 |
|
56 |
||
57 |
/* GUI */ |
|
58 |
||
59 |
export function adjacent_editor_column(editor: TextEditor, split: boolean): ViewColumn |
|
60 |
{ |
|
61 |
if (!editor) return ViewColumn.One |
|
62 |
else if (!split) return editor.viewColumn |
|
63 |
else if (editor.viewColumn === ViewColumn.One || editor.viewColumn === ViewColumn.Three) |
|
64 |
return ViewColumn.Two |
|
65 |
else return ViewColumn.Three |
|
66 |
} |