src/Tools/VSCode/extension/src/library.ts
author wenzelm
Tue, 30 May 2017 14:21:42 +0200
changeset 65970 05e317e291a8
parent 65968 44e703278dfd
child 65972 9f6a154c6ca0
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';
65968
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
     4
import { ViewColumn, TextEditor, workspace } from 'vscode'
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
65968
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    15
/* Isabelle configuration */
65966
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    16
65968
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    17
export function get_configuration<T>(name: string): T
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    18
{
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    19
  return workspace.getConfiguration("isabelle").get<T>(name)
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    20
}
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    21
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    22
export function get_color(color: string, light: boolean): string
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    23
{
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    24
  const config = color + (light ? "_light" : "_dark") + "_color"
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    25
  return get_configuration<string>(config)
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    26
}
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    27
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    28
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    29
/* text editor column */
65966
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    30
65967
5d9da2f8fd3f clarified signature;
wenzelm
parents: 65966
diff changeset
    31
export function other_column(active_editor: TextEditor | null): ViewColumn
65966
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    32
{
65967
5d9da2f8fd3f clarified signature;
wenzelm
parents: 65966
diff changeset
    33
  if (!active_editor || active_editor.viewColumn === ViewColumn.Three) return ViewColumn.One
5d9da2f8fd3f clarified signature;
wenzelm
parents: 65966
diff changeset
    34
  else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two
65966
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    35
  else return ViewColumn.Three
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    36
}