src/Tools/VSCode/extension/src/library.ts
author wenzelm
Sat, 02 Sep 2017 17:21:52 +0200
changeset 66598 e2671e8c476f
parent 66215 9a8b6b86350c
child 75126 da1108a6d249
permissions -rw-r--r--
VSCode extension for official Isabelle release;
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';
66214
eec1c99e1bdc tuned signature;
wenzelm
parents: 66081
diff changeset
     4
import { TextEditor, Uri, ViewColumn, workspace, window } from 'vscode'
65968
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
     5
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
     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
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    15
/* platform information */
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    16
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    17
export function platform_is_windows(): boolean
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    18
{
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    19
  return os.type().startsWith("Windows")
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    20
}
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    21
05e317e291a8 clarified modules;
wenzelm
parents: 65968
diff changeset
    22
66214
eec1c99e1bdc tuned signature;
wenzelm
parents: 66081
diff changeset
    23
/* files */
65972
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    24
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    25
export function is_file(uri: Uri): boolean
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    26
{
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    27
  return uri.scheme === "file"
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    28
}
9f6a154c6ca0 clarified modules;
wenzelm
parents: 65970
diff changeset
    29
66214
eec1c99e1bdc tuned signature;
wenzelm
parents: 66081
diff changeset
    30
export function find_file_editor(uri: Uri): TextEditor | undefined
eec1c99e1bdc tuned signature;
wenzelm
parents: 66081
diff changeset
    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
eec1c99e1bdc tuned signature;
wenzelm
parents: 66081
diff changeset
    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
eec1c99e1bdc tuned signature;
wenzelm
parents: 66081
diff changeset
    38
  }
eec1c99e1bdc tuned signature;
wenzelm
parents: 66081
diff changeset
    39
  else return undefined
eec1c99e1bdc tuned signature;
wenzelm
parents: 66081
diff changeset
    40
}
eec1c99e1bdc tuned signature;
wenzelm
parents: 66081
diff changeset
    41
eec1c99e1bdc tuned signature;
wenzelm
parents: 66081
diff changeset
    42
65968
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    43
/* Isabelle configuration */
65966
169d2928cce1 clarified modules;
wenzelm
parents:
diff changeset
    44
65968
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    45
export function get_configuration<T>(name: string): T
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    46
{
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    47
  return workspace.getConfiguration("isabelle").get<T>(name)
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    48
}
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    49
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    50
export function get_color(color: string, light: boolean): string
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    51
{
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    52
  const config = color + (light ? "_light" : "_dark") + "_color"
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    53
  return get_configuration<string>(config)
44e703278dfd clarified modules;
wenzelm
parents: 65967
diff changeset
    54
}
66081
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    55
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    56
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    57
/* GUI */
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    58
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    59
export function adjacent_editor_column(editor: TextEditor, split: boolean): ViewColumn
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    60
{
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    61
  if (!editor) return ViewColumn.One
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    62
  else if (!split) return editor.viewColumn
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    63
  else if (editor.viewColumn === ViewColumn.One || editor.viewColumn === ViewColumn.Three)
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    64
    return ViewColumn.Two
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    65
  else return ViewColumn.Three
441f95b05944 clarified modules;
wenzelm
parents: 66070
diff changeset
    66
}