--- a/src/Tools/VSCode/extension/src/decorations.ts Tue May 30 11:42:18 2017 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts Tue May 30 11:50:12 2017 +0200
@@ -4,8 +4,8 @@
import * as vscode from 'vscode'
import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
-import { get_color } from './extension'
import { Decoration } from './protocol'
+import * as library from './library'
/* known decoration types */
@@ -81,31 +81,31 @@
function background(color: string): TextEditorDecorationType
{
return decoration(
- { light: { backgroundColor: get_color(color, true) },
- dark: { backgroundColor: get_color(color, false) } })
+ { light: { backgroundColor: library.get_color(color, true) },
+ dark: { backgroundColor: library.get_color(color, false) } })
}
function text_color(color: string): TextEditorDecorationType
{
return decoration(
- { light: { color: get_color(color, true) },
- dark: { color: get_color(color, false) } })
+ { light: { color: library.get_color(color, true) },
+ dark: { color: library.get_color(color, false) } })
}
function text_overview_color(color: string): TextEditorDecorationType
{
return decoration(
{ overviewRulerLane: vscode.OverviewRulerLane.Right,
- light: { overviewRulerColor: get_color(color, true) },
- dark: { overviewRulerColor: get_color(color, false) } })
+ light: { overviewRulerColor: library.get_color(color, true) },
+ dark: { overviewRulerColor: library.get_color(color, false) } })
}
function bottom_border(width: string, style: string, color: string): TextEditorDecorationType
{
const border = `${width} none; border-bottom-style: ${style}; border-color: `
return decoration(
- { light: { border: border + get_color(color, true) },
- dark: { border: border + get_color(color, false) } })
+ { light: { border: border + library.get_color(color, true) },
+ dark: { border: border + library.get_color(color, false) } })
}
--- a/src/Tools/VSCode/extension/src/extension.ts Tue May 30 11:42:18 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Tue May 30 11:50:12 2017 +0200
@@ -4,6 +4,7 @@
import * as path from 'path';
import * as fs from 'fs';
import * as os from 'os';
+import * as library from './library'
import * as decorations from './decorations';
import * as preview from './preview';
import * as protocol from './protocol';
@@ -11,31 +12,15 @@
from 'vscode-languageclient';
-/* Isabelle configuration */
-
-export function get_configuration<T>(name: string): T
-{
- return vscode.workspace.getConfiguration("isabelle").get<T>(name)
-}
-
-export function get_color(color: string, light: boolean): string
-{
- const config = color + (light ? "_light" : "_dark") + "_color"
- return get_configuration<string>(config)
-}
-
-
-/* activate extension */
-
let last_caret_update: protocol.Caret_Update = {}
export function activate(context: vscode.ExtensionContext)
{
const is_windows = os.type().startsWith("Windows")
- const isabelle_home = get_configuration<string>("home")
- const isabelle_args = get_configuration<Array<string>>("args")
- const cygwin_root = get_configuration<string>("cygwin_root")
+ const isabelle_home = library.get_configuration<string>("home")
+ const isabelle_args = library.get_configuration<Array<string>>("args")
+ const cygwin_root = library.get_configuration<string>("cygwin_root")
/* server */
--- a/src/Tools/VSCode/extension/src/library.ts Tue May 30 11:42:18 2017 +0200
+++ b/src/Tools/VSCode/extension/src/library.ts Tue May 30 11:50:12 2017 +0200
@@ -1,7 +1,23 @@
'use strict';
-import { ViewColumn, TextEditor } from 'vscode'
+import { ViewColumn, TextEditor, workspace } from 'vscode'
+
+
+/* Isabelle configuration */
+export function get_configuration<T>(name: string): T
+{
+ return workspace.getConfiguration("isabelle").get<T>(name)
+}
+
+export function get_color(color: string, light: boolean): string
+{
+ const config = color + (light ? "_light" : "_dark") + "_color"
+ return get_configuration<string>(config)
+}
+
+
+/* text editor column */
export function other_column(active_editor: TextEditor | null): ViewColumn
{