clarified modules;

--- a/src/Tools/VSCode/extension/src/decorations.ts	Sun Mar 12 18:05:06 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Sun Mar 12 18:45:53 2017 +0100
@@ -4,6 +4,7 @@
 import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
   TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
 import { get_color } from './extension'
+import { Decoration } from './protocol'
 
 
 /* known decoration types */
@@ -133,18 +134,6 @@
 
 /* decoration for document node */
 
-interface DecorationOpts {
-  range: number[],
-  hover_message?: MarkedString | MarkedString[]
-}
-
-export interface Decoration
-{
-  uri: string,
-  "type": string,
-  content: DecorationOpts[]
-}
-
 type Content = Range[] | DecorationOptions[]
 const document_decorations = new Map<string, Map<string, Content>>()
 

--- a/src/Tools/VSCode/extension/src/extension.ts	Sun Mar 12 18:05:06 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sun Mar 12 18:45:53 2017 +0100
@@ -5,7 +5,7 @@
 import * as fs from 'fs';
 import * as os from 'os';
 import * as decorations from './decorations';
-import { Decoration } from './decorations'
+import * as protocol from './protocol';
 import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
   from 'vscode-languageclient';
 
@@ -24,29 +24,9 @@
 }
 
 
-/* caret handling and dynamic output */
-
-interface Caret_Update
-{
-  uri?: string
-  line?: number
-  character?: number
-}
-
-const caret_update_type = new NotificationType<Caret_Update, void>("PIDE/caret_update")
-let last_caret_update: Caret_Update = {}
+/* activate extension */
 
-
-interface Dynamic_Output
-{
-  body: string
-}
-
-const dynamic_output_type = new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output")
-
-
-
-/* activate extension */
+let last_caret_update: protocol.Caret_Update = {}
 
 export function activate(context: vscode.ExtensionContext)
 {
@@ -80,6 +60,17 @@
     const client = new LanguageClient("Isabelle", server_options, client_options, false)
 
 
+    /* decorations */
+
+    decorations.init(context)
+    vscode.workspace.onDidChangeConfiguration(() => decorations.init(context))
+    vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)
+    vscode.workspace.onDidCloseTextDocument(decorations.close_document)
+
+    client.onReady().then(() =>
+      client.onNotification(protocol.decoration_type, decorations.apply_decoration))
+
+
     /* caret handling and dynamic output */
 
     const dynamic_output = vscode.window.createOutputChannel("Isabelle Output")
@@ -90,7 +81,7 @@
     function update_caret()
     {
       const editor = vscode.window.activeTextEditor
-      let caret_update: Caret_Update = {}
+      let caret_update: protocol.Caret_Update = {}
       if (editor) {
         const uri = editor.document.uri
         const cursor = editor.selection.active
@@ -98,14 +89,14 @@
           caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character }
       }
       if (last_caret_update !== caret_update) {
-        client.sendNotification(caret_update_type, caret_update)
+        client.sendNotification(protocol.caret_update_type, caret_update)
         last_caret_update = caret_update
       }
     }
 
     client.onReady().then(() =>
     {
-      client.onNotification(dynamic_output_type,
+      client.onNotification(protocol.dynamic_output_type,
         params => { dynamic_output.clear(); dynamic_output.appendLine(params.body) })
       vscode.window.onDidChangeActiveTextEditor(_ => update_caret())
       vscode.window.onDidChangeTextEditorSelection(_ => update_caret())
@@ -113,18 +104,6 @@
     })
 
 
-    /* decorations */
-
-    decorations.init(context)
-    vscode.workspace.onDidChangeConfiguration(() => decorations.init(context))
-    vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)
-    vscode.workspace.onDidCloseTextDocument(decorations.close_document)
-
-    client.onReady().then(() =>
-      client.onNotification(
-        new NotificationType<Decoration, void>("PIDE/decoration"), decorations.apply_decoration))
-
-
     /* start server */
 
     context.subscriptions.push(client.start());

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/protocol.ts	Sun Mar 12 18:45:53 2017 +0100
@@ -0,0 +1,46 @@
+'use strict';
+
+import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions } from 'vscode'
+import { NotificationType } from 'vscode-languageclient';
+
+
+/* decorations */
+
+export interface DecorationOpts {
+  range: number[],
+  hover_message?: MarkedString | MarkedString[]
+}
+
+export interface Decoration
+{
+  uri: string,
+  "type": string,
+  content: DecorationOpts[]
+}
+
+export const decoration_type =
+  new NotificationType<Decoration, void>("PIDE/decoration")
+
+
+/* caret handling */
+
+export interface Caret_Update
+{
+  uri?: string
+  line?: number
+  character?: number
+}
+
+export const caret_update_type =
+  new NotificationType<Caret_Update, void>("PIDE/caret_update")
+
+
+/* dynamic output */
+
+export interface Dynamic_Output
+{
+  body: string
+}
+
+export const dynamic_output_type =
+  new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output")

--- a/src/Tools/VSCode/src/protocol.scala	Sun Mar 12 18:05:06 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Sun Mar 12 18:45:53 2017 +0100
@@ -422,7 +422,7 @@
   }
 
 
-  /* caret handling and dynamic output */
+  /* caret handling */
 
   object Caret_Update
   {
@@ -440,6 +440,9 @@
       }
   }
 
+
+  /* dynamic output */
+
   object Dynamic_Output
   {
     def apply(body: String): JSON.T =