merged

--- a/src/Tools/VSCode/extension/src/abbreviations.ts	Wed Mar 02 15:57:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/abbreviations.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -8,6 +8,7 @@
 import { ExtensionContext, Range, TextDocumentContentChangeEvent, workspace, WorkspaceEdit } from 'vscode'
 import { Prefix_Tree } from './isabelle_filesystem/prefix_tree'
 import * as library from './library'
+import * as vscode_lib from './vscode_lib'
 import * as symbol from './symbol'
 
 const entries: Record<string, string> = {}
@@ -21,7 +22,7 @@
     workspace.onDidChangeTextDocument(e =>
     {
       const doc = e.document
-      const mode = library.get_replacement_mode()
+      const mode = vscode_lib.get_replacement_mode()
       if (
         mode === 'none' ||
         doc.languageId !== 'isabelle' ||

--- a/src/Tools/VSCode/extension/src/decorations.ts	Wed Mar 02 15:57:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -6,6 +6,7 @@
   TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext } from 'vscode'
 import { Document_Decorations } from './protocol'
 import * as library from './library'
+import * as vscode_lib from './vscode_lib'
 import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace'
 
 
@@ -87,31 +88,31 @@
   function background(color: string): TextEditorDecorationType
   {
     return decoration(
-      { light: { backgroundColor: library.get_color(color, true) },
-        dark: { backgroundColor: library.get_color(color, false) } })
+      { light: { backgroundColor: vscode_lib.get_color(color, true) },
+        dark: { backgroundColor: vscode_lib.get_color(color, false) } })
   }
 
   function text_color(color: string): TextEditorDecorationType
   {
     return decoration(
-      { light: { color: library.get_color(color, true) },
-        dark: { color: library.get_color(color, false) } })
+      { light: { color: vscode_lib.get_color(color, true) },
+        dark: { color: vscode_lib.get_color(color, false) } })
   }
 
   function text_overview_color(color: string): TextEditorDecorationType
   {
     return decoration(
       { overviewRulerLane: OverviewRulerLane.Right,
-        light: { overviewRulerColor: library.get_color(color, true) },
-        dark: { overviewRulerColor: library.get_color(color, false) } })
+        light: { overviewRulerColor: vscode_lib.get_color(color, true) },
+        dark: { overviewRulerColor: vscode_lib.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 + library.get_color(color, true) },
-        dark: { border: border + library.get_color(color, false) } })
+      { light: { border: border + vscode_lib.get_color(color, true) },
+        dark: { border: border + vscode_lib.get_color(color, false) } })
   }
 
 

--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Mar 02 15:57:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -2,6 +2,7 @@
 
 import * as platform from './platform'
 import * as library from './library'
+import * as vscode_lib from './vscode_lib'
 import * as decorations from './decorations'
 import * as preview_panel from './preview_panel'
 import * as protocol from './protocol'
@@ -30,7 +31,7 @@
     const isabelle_tool = isabelle_home + "/bin/isabelle"
     const isabelle_args =
       ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
-        .concat(library.get_configuration<Array<string>>("args"))
+        .concat(vscode_lib.get_configuration<Array<string>>("args"))
         .concat(roots.length > 0 && workspace_dir !== undefined ? ["-D", workspace_dir] : [])
 
     const server_options: ServerOptions =
@@ -60,7 +61,7 @@
       async (progress) =>
         {
           progress.report({
-            message: "Waiting for Isabelle server..."
+            message: "Waiting for Isabelle language server..."
           })
           await language_client.onReady()
         })
@@ -93,7 +94,7 @@
       if (editor) {
         const uri = editor.document.uri
         const cursor = editor.selection.active
-        if (library.is_file(uri) && cursor)
+        if (vscode_lib.is_file(uri) && cursor)
           caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character }
       }
       if (last_caret_update !== caret_update) {
@@ -117,7 +118,7 @@
         caret_update.uri = Isabelle_Workspace.get_isabelle(Uri.parse(caret_update.uri)).toString()
         workspace.openTextDocument(Uri.parse(caret_update.uri)).then(document =>
         {
-          const editor = library.find_file_editor(document.uri)
+          const editor = vscode_lib.find_file_editor(document.uri)
           const column = editor ? editor.viewColumn : ViewColumn.One
           window.showTextDocument(document, column, !caret_update.focus).then(move_cursor)
         })

--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts	Wed Mar 02 15:57:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -15,6 +15,7 @@
   workspace
 } from 'vscode';
 import * as library from '../library';
+import * as vscode_lib from '../vscode_lib';
 import { Session_Theories } from '../protocol';
 import * as symbol from '../symbol';
 import { Mapping_FSP } from './mapping_fsp';
@@ -219,7 +220,7 @@
 
   private async open_theory_dialogue(file_uri: Uri)
   {
-    const always_open = library.get_configuration<boolean>('always_open_thys')
+    const always_open = vscode_lib.get_configuration<boolean>('always_open_thys')
     if (!always_open) {
       const answer = await window.showInformationMessage(
         'Would you like to open the Isabelle theory associated with this file?',
@@ -227,7 +228,7 @@
         'Always yes'
       )
       if (answer === 'Always yes') {
-        library.set_configuration('always_open_thys', true)
+        vscode_lib.set_configuration('always_open_thys', true)
       } else if (answer !== 'Yes') {
         return
       }

--- a/src/Tools/VSCode/extension/src/library.ts	Wed Mar 02 15:57:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/library.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -1,9 +1,12 @@
+/*  Author:     Makarius
+
+Basic library (see Pure/library.scala).
+*/
+
 'use strict';
 
 import * as platform from './platform'
 import * as path from 'path'
-import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode'
-import {Isabelle_Workspace} from './isabelle_filesystem/isabelle_workspace'
 
 
 /* regular expressions */
@@ -154,59 +157,3 @@
 
   return result()
 }
-
-
-/* files */
-
-export function is_file(uri: Uri): boolean
-{
-  return uri.scheme === "file" || uri.scheme === Isabelle_Workspace.scheme
-}
-
-export function find_file_editor(uri: Uri): TextEditor | undefined
-{
-  function check(editor: TextEditor): boolean
-  { return editor && is_file(editor.document.uri) && editor.document.uri.fsPath === uri.fsPath }
-
-  if (is_file(uri)) {
-    if (check(window.activeTextEditor)) return window.activeTextEditor
-    else return window.visibleTextEditors.find(check)
-  }
-  else return undefined
-}
-
-
-/* Isabelle configuration */
-
-export function get_configuration<T>(name: string): T
-{
-  return workspace.getConfiguration("isabelle").get<T>(name)
-}
-
-export function set_configuration<T>(name: string, configuration: T)
-{
-  workspace.getConfiguration("isabelle").update(name, configuration)
-}
-
-export function get_replacement_mode()
-{
-  return get_configuration<"none" | "non-alphanumeric" | "all">("replacement")
-}
-
-export function get_color(color: string, light: boolean): string
-{
-  const colors = get_configuration<object>("text_color")
-  return colors[color + (light ? "_light" : "_dark")]
-}
-
-
-/* GUI */
-
-export function adjacent_editor_column(editor: TextEditor, split: boolean): ViewColumn
-{
-  if (!editor) return ViewColumn.One
-  else if (!split) return editor.viewColumn
-  else if (editor.viewColumn === ViewColumn.One || editor.viewColumn === ViewColumn.Three)
-    return ViewColumn.Two
-  else return ViewColumn.Three
-}

--- a/src/Tools/VSCode/extension/src/output_view.ts	Wed Mar 02 15:57:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/output_view.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -9,6 +9,7 @@
    CancellationToken, window, Position, Selection, Webview} from 'vscode'
 import { text_colors } from './decorations'
 import * as library from './library'
+import * as vscode_lib from './vscode_lib'
 import * as path from 'path'
 import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace'
 
@@ -103,8 +104,8 @@
 {
   let style: string = ''
   for (const key of text_colors) {
-  style += `body.vscode-light .${key} { color: ${library.get_color(key, true)} }\n`
-  style += `body.vscode-dark .${key} { color: ${library.get_color(key, false)} }\n`
+  style += `body.vscode-light .${key} { color: ${vscode_lib.get_color(key, true)} }\n`
+  style += `body.vscode-dark .${key} { color: ${vscode_lib.get_color(key, false)} }\n`
   }
 
   return style

--- a/src/Tools/VSCode/extension/src/platform.ts	Wed Mar 02 15:57:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/platform.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -1,3 +1,8 @@
+/*  Author:     Makarius
+
+System platform identification (see Pure/System/platform.scala).
+*/
+
 'use strict';
 
 import * as os from 'os'

--- a/src/Tools/VSCode/extension/src/preview_panel.ts	Wed Mar 02 15:57:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -3,6 +3,7 @@
 import { ExtensionContext, Uri, window, ViewColumn, WebviewPanel } from 'vscode'
 import { LanguageClient } from 'vscode-languageclient/node'
 import * as library from './library'
+import * as vscode_lib from './vscode_lib'
 import * as protocol from './protocol'
 
 
@@ -53,6 +54,6 @@
   if (language_client) {
     language_client.sendNotification(protocol.preview_request_type,
       { uri: document_uri.toString(),
-        column: library.adjacent_editor_column(window.activeTextEditor, split) })
+        column: vscode_lib.adjacent_editor_column(window.activeTextEditor, split) })
   }
 }

--- a/src/Tools/VSCode/extension/src/state_panel.ts	Wed Mar 02 15:57:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -1,6 +1,7 @@
 'use strict';
 
 import * as library from './library'
+import * as vscode_lib from './vscode_lib'
 import * as protocol from './protocol'
 import {LanguageClient} from 'vscode-languageclient/node'
 import {ExtensionContext, Uri, ViewColumn, WebviewPanel, window} from 'vscode'
@@ -11,7 +12,7 @@
 
 function panel_column(): ViewColumn
 {
-  return library.adjacent_editor_column(window.activeTextEditor, true)
+  return vscode_lib.adjacent_editor_column(window.activeTextEditor, true)
 }
 
 class Panel

--- a/src/Tools/VSCode/extension/src/symbol.ts	Wed Mar 02 15:57:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -1,3 +1,8 @@
+/*  Author:     Makarius
+
+Isabelle text symbols (see Pure/General/symbol.scala).
+*/
+
 'use strict';
 
 import * as library from './library'

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/vscode_lib.ts	Wed Mar 02 16:08:17 2022 +0100
@@ -0,0 +1,63 @@
+/*  Author:     Makarius
+
+Misc library functions for VSCode.
+*/
+
+import {Isabelle_Workspace} from './isabelle_filesystem/isabelle_workspace'
+import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode'
+
+
+/* files */
+
+export function is_file(uri: Uri): boolean
+{
+  return uri.scheme === "file" || uri.scheme === Isabelle_Workspace.scheme
+}
+
+export function find_file_editor(uri: Uri): TextEditor | undefined
+{
+  function check(editor: TextEditor): boolean
+  { return editor && is_file(editor.document.uri) && editor.document.uri.fsPath === uri.fsPath }
+
+  if (is_file(uri)) {
+    if (check(window.activeTextEditor)) return window.activeTextEditor
+    else return window.visibleTextEditors.find(check)
+  }
+  else return undefined
+}
+
+
+/* GUI */
+
+export function adjacent_editor_column(editor: TextEditor, split: boolean): ViewColumn
+{
+  if (!editor) return ViewColumn.One
+  else if (!split) return editor.viewColumn
+  else if (editor.viewColumn === ViewColumn.One || editor.viewColumn === ViewColumn.Three)
+    return ViewColumn.Two
+  else return ViewColumn.Three
+}
+
+
+/* Isabelle configuration */
+
+export function get_configuration<T>(name: string): T
+{
+  return workspace.getConfiguration("isabelle").get<T>(name)
+}
+
+export function set_configuration<T>(name: string, configuration: T)
+{
+  workspace.getConfiguration("isabelle").update(name, configuration)
+}
+
+export function get_replacement_mode()
+{
+  return get_configuration<"none" | "non-alphanumeric" | "all">("replacement")
+}
+
+export function get_color(color: string, light: boolean): string
+{
+  const colors = get_configuration<object>("text_color")
+  return colors[color + (light ? "_light" : "_dark")]
+}