# HG changeset patch # User wenzelm # Date 1646653023 -3600 # Node ID 57de0062dc1c9c1c00cf0aba0682f9b537e1981b # Parent 99b83e701c8ee26a53220026272103cc43fe2c6b proper file headers; diff -r 99b83e701c8e -r 57de0062dc1c src/Tools/VSCode/extension/src/completion.ts --- a/src/Tools/VSCode/extension/src/completion.ts Sun Mar 06 22:13:18 2022 +0100 +++ b/src/Tools/VSCode/extension/src/completion.ts Mon Mar 07 12:37:03 2022 +0100 @@ -1,3 +1,8 @@ +/* Author: Makarius + +Support for PIDE completion information. +*/ + 'use strict'; import { CompletionItemProvider, CompletionItem, TextDocument, Range, Position, diff -r 99b83e701c8e -r 57de0062dc1c src/Tools/VSCode/extension/src/decorations.ts --- a/src/Tools/VSCode/extension/src/decorations.ts Sun Mar 06 22:13:18 2022 +0100 +++ b/src/Tools/VSCode/extension/src/decorations.ts Mon Mar 07 12:37:03 2022 +0100 @@ -1,3 +1,8 @@ +/* Author: Makarius + +PIDE document decorations. +*/ + 'use strict'; import * as timers from 'timers' diff -r 99b83e701c8e -r 57de0062dc1c src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Sun Mar 06 22:13:18 2022 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Mon Mar 07 12:37:03 2022 +0100 @@ -1,3 +1,10 @@ +/* Author: Makarius + Author: Denis Paluca, TU Muenchen + Author: Fabian Huch, TU Muenchen + +Isabelle/VSCode extension. +*/ + 'use strict'; import * as platform from './platform' diff -r 99b83e701c8e -r 57de0062dc1c src/Tools/VSCode/extension/src/preview_panel.ts --- a/src/Tools/VSCode/extension/src/preview_panel.ts Sun Mar 06 22:13:18 2022 +0100 +++ b/src/Tools/VSCode/extension/src/preview_panel.ts Mon Mar 07 12:37:03 2022 +0100 @@ -1,3 +1,8 @@ +/* Author: Makarius + +Preview panel via HTML webview inside VSCode. +*/ + 'use strict'; import { ExtensionContext, Uri, window, ViewColumn, WebviewPanel } from 'vscode' diff -r 99b83e701c8e -r 57de0062dc1c src/Tools/VSCode/extension/src/state_panel.ts --- a/src/Tools/VSCode/extension/src/state_panel.ts Sun Mar 06 22:13:18 2022 +0100 +++ b/src/Tools/VSCode/extension/src/state_panel.ts Mon Mar 07 12:37:03 2022 +0100 @@ -1,3 +1,8 @@ +/* Author: Makarius + +State panel via HTML webview inside VSCode. +*/ + 'use strict'; import * as vscode_lib from './vscode_lib'