# HG changeset patch
# User wenzelm
# Date 1646322365 -3600
# Node ID 8f6b8a46f54ca308ca2db1777bcbaff9d3d045f1
# Parent  c05f0e8a54de9e9fd000fcefc708def9d38d578e
clarified modules: more uniform .scala vs. ts (amending 4519eeefe3b5);

diff -r c05f0e8a54de -r 8f6b8a46f54c src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Thu Mar 03 16:18:27 2022 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Thu Mar 03 16:46:05 2022 +0100
@@ -4,7 +4,7 @@
 import {window, OverviewRulerLane, Uri} from 'vscode';
 import { Range, DecorationOptions, DecorationRenderOptions,
   TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext } from 'vscode'
-import { Document_Decorations } from './protocol'
+import { Document_Decorations } from './lsp'
 import * as vscode_lib from './vscode_lib'
 import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace'
 
diff -r c05f0e8a54de -r 8f6b8a46f54c src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Thu Mar 03 16:18:27 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Thu Mar 03 16:46:05 2022 +0100
@@ -6,7 +6,7 @@
 import * as vscode_lib from './vscode_lib'
 import * as decorations from './decorations'
 import * as preview_panel from './preview_panel'
-import * as protocol from './protocol'
+import * as lsp from './lsp'
 import * as state_panel from './state_panel'
 import { Uri, TextEditor, ViewColumn, Selection, Position, ExtensionContext, workspace, window,
   commands, ProgressLocation } from 'vscode'
@@ -16,7 +16,7 @@
 import { register_script_decorations } from './script_decorations'
 
 
-let last_caret_update: protocol.Caret_Update = {}
+let last_caret_update: lsp.Caret_Update = {}
 
 export async function activate(context: ExtensionContext)
 {
@@ -77,7 +77,7 @@
       workspace.onDidCloseTextDocument(decorations.close_document))
 
     language_client.onReady().then(() =>
-      language_client.onNotification(protocol.decoration_type, decorations.apply_decoration))
+      language_client.onNotification(lsp.decoration_type, decorations.apply_decoration))
 
 
     /* super-/subscript decorations */
@@ -90,7 +90,7 @@
     function update_caret()
     {
       const editor = window.activeTextEditor
-      let caret_update: protocol.Caret_Update = {}
+      let caret_update: lsp.Caret_Update = {}
       if (editor) {
         const uri = editor.document.uri
         const cursor = editor.selection.active
@@ -100,13 +100,13 @@
       if (last_caret_update !== caret_update) {
         if (caret_update.uri) {
           caret_update.uri = Isabelle_Workspace.get_file(Uri.parse(caret_update.uri)).toString()
-          language_client.sendNotification(protocol.caret_update_type, caret_update)
+          language_client.sendNotification(lsp.caret_update_type, caret_update)
         }
         last_caret_update = caret_update
       }
     }
 
-    function goto_file(caret_update: protocol.Caret_Update)
+    function goto_file(caret_update: lsp.Caret_Update)
     {
       function move_cursor(editor: TextEditor)
       {
@@ -132,7 +132,7 @@
         window.onDidChangeTextEditorSelection(_ => update_caret()))
       update_caret()
 
-      language_client.onNotification(protocol.caret_update_type, goto_file)
+      language_client.onNotification(lsp.caret_update_type, goto_file)
     })
 
 
@@ -144,7 +144,7 @@
 
     language_client.onReady().then(() =>
     {
-      language_client.onNotification(protocol.dynamic_output_type,
+      language_client.onNotification(lsp.dynamic_output_type,
         params => provider.update_content(params.content))
     })
 
@@ -170,10 +170,10 @@
 
     language_client.onReady().then(() =>
     {
-      language_client.onNotification(protocol.session_theories_type,
+      language_client.onNotification(lsp.session_theories_type,
         async ({entries}) => await Isabelle_Workspace.update_sessions(entries))
 
-      language_client.onNotification(protocol.symbols_type,
+      language_client.onNotification(lsp.symbols_type,
         params =>
           {
             //register_abbreviations(params.entries, context)
@@ -181,10 +181,10 @@
 
             // request theories to load in isabelle file system
             // after a valid symbol encoder is loaded
-            language_client.sendNotification(protocol.session_theories_request_type)
+            language_client.sendNotification(lsp.session_theories_request_type)
           })
 
-      language_client.sendNotification(protocol.symbols_request_type)
+      language_client.sendNotification(lsp.symbols_request_type)
 
     })
 
@@ -195,15 +195,15 @@
     {
       context.subscriptions.push(
         commands.registerCommand("isabelle.include-word", uri =>
-          language_client.sendNotification(protocol.include_word_type)),
+          language_client.sendNotification(lsp.include_word_type)),
         commands.registerCommand("isabelle.include-word-permanently", uri =>
-          language_client.sendNotification(protocol.include_word_permanently_type)),
+          language_client.sendNotification(lsp.include_word_permanently_type)),
         commands.registerCommand("isabelle.exclude-word", uri =>
-          language_client.sendNotification(protocol.exclude_word_type)),
+          language_client.sendNotification(lsp.exclude_word_type)),
         commands.registerCommand("isabelle.exclude-word-permanently", uri =>
-          language_client.sendNotification(protocol.exclude_word_permanently_type)),
+          language_client.sendNotification(lsp.exclude_word_permanently_type)),
         commands.registerCommand("isabelle.reset-words", uri =>
-          language_client.sendNotification(protocol.reset_words_type)))
+          language_client.sendNotification(lsp.reset_words_type)))
     })
 
 
diff -r c05f0e8a54de -r 8f6b8a46f54c src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts	Thu Mar 03 16:18:27 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts	Thu Mar 03 16:46:05 2022 +0100
@@ -14,7 +14,7 @@
   workspace
 } from 'vscode';
 import * as vscode_lib from '../vscode_lib';
-import { Session_Theories } from '../protocol';
+import { Session_Theories } from '../lsp';
 import * as symbol from '../symbol';
 import { Mapping_FSP } from './mapping_fsp';
 import { Symbol_Encoder } from './symbol_encoder';
diff -r c05f0e8a54de -r 8f6b8a46f54c src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts	Thu Mar 03 16:18:27 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts	Thu Mar 03 16:46:05 2022 +0100
@@ -6,7 +6,7 @@
 'use strict';
 
 import { ExtensionContext } from 'vscode'
-import { Session_Theories } from '../protocol'
+import { Session_Theories } from '../lsp'
 import * as symbol from '../symbol'
 
 interface Setup_Data
diff -r c05f0e8a54de -r 8f6b8a46f54c src/Tools/VSCode/extension/src/lsp.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Thu Mar 03 16:46:05 2022 +0100
@@ -0,0 +1,160 @@
+/*  Author:     Makarius
+
+Message formats for Language Server Protocol, with adhoc PIDE extensions
+(see Tools/VSCode/src/lsp.scala).
+*/
+
+'use strict';
+
+import { MarkdownString } from 'vscode'
+import { NotificationType } from 'vscode-languageclient'
+import * as symbol from './symbol'
+
+
+/* decorations */
+
+export interface Decoration_Options {
+  range: number[],
+  hover_message?: MarkdownString | MarkdownString[]
+}
+
+export interface Decoration
+{
+  "type": string
+  content: Decoration_Options[]
+}
+
+export interface Document_Decorations {
+  uri: string
+  entries: Decoration[]
+}
+
+export const decoration_type =
+  new NotificationType<Document_Decorations>("PIDE/decoration")
+
+
+/* caret handling */
+
+export interface Caret_Update
+{
+  uri?: string
+  line?: number
+  character?: number
+  focus?: boolean
+}
+
+export const caret_update_type =
+  new NotificationType<Caret_Update>("PIDE/caret_update")
+
+
+/* dynamic output */
+
+export interface Dynamic_Output
+{
+  content: string
+}
+
+export const dynamic_output_type =
+  new NotificationType<Dynamic_Output>("PIDE/dynamic_output")
+
+
+/* state */
+
+export interface State_Output
+{
+  id: number
+  content: string
+  auto_update: boolean
+}
+
+export const state_output_type =
+  new NotificationType<State_Output>("PIDE/state_output")
+
+export interface State_Id
+{
+  id: number
+}
+
+export interface Auto_Update
+{
+  id: number
+  enabled: boolean
+}
+
+export const state_init_type = new NotificationType<void>("PIDE/state_init")
+export const state_exit_type = new NotificationType<State_Id>("PIDE/state_exit")
+export const state_locate_type = new NotificationType<State_Id>("PIDE/state_locate")
+export const state_update_type = new NotificationType<State_Id>("PIDE/state_update")
+export const state_auto_update_type =
+  new NotificationType<Auto_Update>("PIDE/state_auto_update")
+
+
+/* preview */
+
+export interface Preview_Request
+{
+  uri: string
+  column: number
+}
+
+export interface Preview_Response
+{
+  uri: string
+  column: number
+  label: string
+  content: string
+}
+
+export const preview_request_type =
+  new NotificationType<Preview_Request>("PIDE/preview_request")
+
+export const preview_response_type =
+  new NotificationType<Preview_Response>("PIDE/preview_response")
+
+
+/* Isabelle symbols */
+
+export interface Symbols
+{
+  entries: [symbol.Entry]
+}
+
+export const symbols_type =
+  new NotificationType<Symbols>("PIDE/symbols")
+
+export const symbols_request_type =
+  new NotificationType<void>("PIDE/symbols_request")
+
+export interface Entries<T>
+{
+  entries: T[]
+}
+
+export interface Session_Theories
+{
+  session_name: string
+  theories: string[]
+}
+
+export const session_theories_type =
+  new NotificationType<Entries<Session_Theories>>("PIDE/session_theories")
+
+export const session_theories_request_type =
+  new NotificationType<void>("PIDE/session_theories_request")
+
+/* spell checker */
+
+export const include_word_type =
+  new NotificationType<void>("PIDE/include_word")
+
+export const include_word_permanently_type =
+  new NotificationType<void>("PIDE/include_word_permanently")
+
+export const exclude_word_type =
+  new NotificationType<void>("PIDE/exclude_word")
+
+export const exclude_word_permanently_type =
+  new NotificationType<void>("PIDE/exclude_word_permanently")
+
+export const reset_words_type =
+  new NotificationType<void>("PIDE/reset_words")
diff -r c05f0e8a54de -r 8f6b8a46f54c src/Tools/VSCode/extension/src/preview_panel.ts
--- a/src/Tools/VSCode/extension/src/preview_panel.ts	Thu Mar 03 16:18:27 2022 +0100
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts	Thu Mar 03 16:46:05 2022 +0100
@@ -3,7 +3,7 @@
 import { ExtensionContext, Uri, window, ViewColumn, WebviewPanel } from 'vscode'
 import { LanguageClient } from 'vscode-languageclient/node'
 import * as vscode_lib from './vscode_lib'
-import * as protocol from './protocol'
+import * as lsp from './lsp'
 
 
 let language_client: LanguageClient
@@ -39,7 +39,7 @@
 export function setup(context: ExtensionContext, client: LanguageClient)
 {
   language_client = client
-  language_client.onNotification(protocol.preview_response_type, params =>
+  language_client.onNotification(lsp.preview_response_type, params =>
     {
       if (!panel) { panel = new Panel(params.column) }
       else panel.reveal(params.column)
@@ -51,7 +51,7 @@
 {
   const document_uri = uri || window.activeTextEditor.document.uri
   if (language_client) {
-    language_client.sendNotification(protocol.preview_request_type,
+    language_client.sendNotification(lsp.preview_request_type,
       { uri: document_uri.toString(),
         column: vscode_lib.adjacent_editor_column(window.activeTextEditor, split) })
   }
diff -r c05f0e8a54de -r 8f6b8a46f54c src/Tools/VSCode/extension/src/protocol.ts
--- a/src/Tools/VSCode/extension/src/protocol.ts	Thu Mar 03 16:18:27 2022 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
-'use strict';
-
-import { MarkdownString } from 'vscode'
-import { NotificationType } from 'vscode-languageclient'
-import * as symbol from './symbol'
-
-/* decorations */
-
-export interface Decoration_Options {
-  range: number[],
-  hover_message?: MarkdownString | MarkdownString[]
-}
-
-export interface Decoration
-{
-  "type": string
-  content: Decoration_Options[]
-}
-
-export interface Document_Decorations {
-  uri: string
-  entries: Decoration[]
-}
-
-export const decoration_type =
-  new NotificationType<Document_Decorations>("PIDE/decoration")
-
-
-/* caret handling */
-
-export interface Caret_Update
-{
-  uri?: string
-  line?: number
-  character?: number
-  focus?: boolean
-}
-
-export const caret_update_type =
-  new NotificationType<Caret_Update>("PIDE/caret_update")
-
-
-/* dynamic output */
-
-export interface Dynamic_Output
-{
-  content: string
-}
-
-export const dynamic_output_type =
-  new NotificationType<Dynamic_Output>("PIDE/dynamic_output")
-
-
-/* state */
-
-export interface State_Output
-{
-  id: number
-  content: string
-  auto_update: boolean
-}
-
-export const state_output_type =
-  new NotificationType<State_Output>("PIDE/state_output")
-
-export interface State_Id
-{
-  id: number
-}
-
-export interface Auto_Update
-{
-  id: number
-  enabled: boolean
-}
-
-export const state_init_type = new NotificationType<void>("PIDE/state_init")
-export const state_exit_type = new NotificationType<State_Id>("PIDE/state_exit")
-export const state_locate_type = new NotificationType<State_Id>("PIDE/state_locate")
-export const state_update_type = new NotificationType<State_Id>("PIDE/state_update")
-export const state_auto_update_type =
-  new NotificationType<Auto_Update>("PIDE/state_auto_update")
-
-
-/* preview */
-
-export interface Preview_Request
-{
-  uri: string
-  column: number
-}
-
-export interface Preview_Response
-{
-  uri: string
-  column: number
-  label: string
-  content: string
-}
-
-export const preview_request_type =
-  new NotificationType<Preview_Request>("PIDE/preview_request")
-
-export const preview_response_type =
-  new NotificationType<Preview_Response>("PIDE/preview_response")
-
-
-/* Isabelle symbols */
-
-export interface Symbols
-{
-  entries: [symbol.Entry]
-}
-
-export const symbols_type =
-  new NotificationType<Symbols>("PIDE/symbols")
-
-export const symbols_request_type =
-  new NotificationType<void>("PIDE/symbols_request")
-
-export interface Entries<T>
-{
-  entries: T[]
-}
-
-export interface Session_Theories
-{
-  session_name: string
-  theories: string[]
-}
-
-export const session_theories_type =
-  new NotificationType<Entries<Session_Theories>>("PIDE/session_theories")
-
-export const session_theories_request_type =
-  new NotificationType<void>("PIDE/session_theories_request")
-
-/* spell checker */
-
-export const include_word_type =
-  new NotificationType<void>("PIDE/include_word")
-
-export const include_word_permanently_type =
-  new NotificationType<void>("PIDE/include_word_permanently")
-
-export const exclude_word_type =
-  new NotificationType<void>("PIDE/exclude_word")
-
-export const exclude_word_permanently_type =
-  new NotificationType<void>("PIDE/exclude_word_permanently")
-
-export const reset_words_type =
-  new NotificationType<void>("PIDE/reset_words")
diff -r c05f0e8a54de -r 8f6b8a46f54c src/Tools/VSCode/extension/src/state_panel.ts
--- a/src/Tools/VSCode/extension/src/state_panel.ts	Thu Mar 03 16:18:27 2022 +0100
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Thu Mar 03 16:46:05 2022 +0100
@@ -1,7 +1,7 @@
 'use strict';
 
 import * as vscode_lib from './vscode_lib'
-import * as protocol from './protocol'
+import * as lsp from './lsp'
 import {LanguageClient} from 'vscode-languageclient/node'
 import {ExtensionContext, Uri, ViewColumn, WebviewPanel, window} from 'vscode'
 import {get_webview_html, open_webview_link} from './output_view'
@@ -23,7 +23,7 @@
   public get_id(): number { return this.state_id }
   public check_id(id: number): boolean { return this.state_id === id }
 
-  public set_content(state: protocol.State_Output)
+  public set_content(state: lsp.State_Output)
   {
     this.state_id = state.id
     this.webview_panel.webview.html = this._get_html(state.content, state.auto_update)
@@ -45,13 +45,13 @@
       switch (message.command) {
         case "auto_update":
           language_client.sendNotification(
-            protocol.state_auto_update_type, { id: this.state_id, enabled: message.enabled })
+            lsp.state_auto_update_type, { id: this.state_id, enabled: message.enabled })
           break
         case "update":
-          language_client.sendNotification(protocol.state_update_type, { id: this.state_id })
+          language_client.sendNotification(lsp.state_update_type, { id: this.state_id })
           break
         case "locate":
-          language_client.sendNotification(protocol.state_locate_type, { id: this.state_id })
+          language_client.sendNotification(lsp.state_locate_type, { id: this.state_id })
           break
         case "open":
           open_webview_link(message.link)
@@ -83,7 +83,7 @@
 function exit_panel()
 {
   if (panel) {
-    language_client.sendNotification(protocol.state_exit_type, { id: panel.get_id() })
+    language_client.sendNotification(lsp.state_exit_type, { id: panel.get_id() })
     panel = null
   }
 }
@@ -92,14 +92,14 @@
 {
   if (language_client) {
     if (panel) panel.reveal()
-    else language_client.sendNotification(protocol.state_init_type)
+    else language_client.sendNotification(lsp.state_init_type)
   }
 }
 
 export function setup(context: ExtensionContext, client: LanguageClient)
 {
   language_client = client
-  language_client.onNotification(protocol.state_output_type, params =>
+  language_client.onNotification(lsp.state_output_type, params =>
     {
       if (!panel) {
         panel = new Panel(context.extensionPath)
diff -r c05f0e8a54de -r 8f6b8a46f54c src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Thu Mar 03 16:18:27 2022 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Thu Mar 03 16:46:05 2022 +0100
@@ -1,8 +1,8 @@
 /*  Title:      Tools/VSCode/src/lsp.scala
     Author:     Makarius
 
-Message formats for Language Server Protocol 3.0, see
-https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
+Message formats for Language Server Protocol, with adhoc PIDE extensions.
+See https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
 */
 
 package isabelle.vscode