src/Tools/VSCode/extension/src/library.ts
author wenzelm
Tue, 30 May 2017 15:29:42 +0200
changeset 65972 9f6a154c6ca0
parent 65970 05e317e291a8
child 65983 d8c5603c1732
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65966
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
     1
'use strict';
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
     2
65970
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
     3
import * as os from 'os';
65972
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
     4
import { ViewColumn, TextEditor, Uri, workspace } from 'vscode'
65968
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
     5
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
     6
65970
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
     7
/* platform information */
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
     8
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
     9
export function platform_is_windows(): boolean
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    10
{
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    11
  return os.type().startsWith("Windows")
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    12
}
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    13
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    14
65972
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    15
/* file URIs */
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    16
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    17
export function is_file(uri: Uri): boolean
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    18
{
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    19
  return uri.scheme === "file"
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    20
}
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    21
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    22
65968
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    23
/* Isabelle configuration */
65966
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    24
65968
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    25
export function get_configuration<T>(name: string): T
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    26
{
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    27
  return workspace.getConfiguration("isabelle").get<T>(name)
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    28
}
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    29
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    30
export function get_color(color: string, light: boolean): string
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    31
{
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    32
  const config = color + (light ? "_light" : "_dark") + "_color"
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    33
  return get_configuration<string>(config)
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    34
}
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    35
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    36
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    37
/* text editor column */
65966
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    38
65967
5d9da2f8fd3f clarified signature;
wenzelm
parents: 65966
diff changeset
    39
export function other_column(active_editor: TextEditor | null): ViewColumn
65966
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    40
{
65967
5d9da2f8fd3f clarified signature;
wenzelm
parents: 65966
diff changeset
    41
  if (!active_editor || active_editor.viewColumn === ViewColumn.Three) return ViewColumn.One
5d9da2f8fd3f clarified signature;
wenzelm
parents: 65966
diff changeset
    42
  else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two
65966
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    43
  else return ViewColumn.Three
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    44
}