--- a/Admin/components/components.sha1 Wed Oct 02 23:47:07 2024 +0200
+++ b/Admin/components/components.sha1 Thu Oct 03 13:01:31 2024 +0200
@@ -553,6 +553,7 @@
86c952d739d1eb868be88898982d4870a3d8c2dc vscode_extension-20220325.tar.gz
5293b9e77e5c887d449b671828b133fad4f18632 vscode_extension-20220829.tar.gz
0d9551ffeb968813b6017278fa7ab9bd6062883f vscode_extension-20230206.tar.gz
+0630f00067dc973dab4c9274c56b79c973c5c494 vscode_extension-20241002.tar.gz
67b271186631f84efd97246bf85f6d8cfaa5edfd vscodium-1.65.2.tar.gz
c439ab741e0cc49354cc03aa9af501202a5a38e3 vscodium-1.70.1.tar.gz
81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz
--- a/Admin/components/main Wed Oct 02 23:47:07 2024 +0200
+++ b/Admin/components/main Thu Oct 03 13:01:31 2024 +0200
@@ -37,7 +37,7 @@
stack-2.15.5
vampire-4.8
verit-2021.06.2-rmx-1
-vscode_extension-20230206
+vscode_extension-20241002
vscodium-1.70.1
xz-java-1.9
z3-4.4.0pre-4
--- a/CONTRIBUTORS Wed Oct 02 23:47:07 2024 +0200
+++ b/CONTRIBUTORS Thu Oct 03 13:01:31 2024 +0200
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* April - October 2024: Thomas Lindae and Fabian Huch, TU München
+ Improvements to the language server for Isabelle/VSCode.
+
* June - July 2024: Fabian Huch
New Build_Manager module to coordinate CI and user builds, replacing
the previous Jenkins integration.
--- a/NEWS Wed Oct 02 23:47:07 2024 +0200
+++ b/NEWS Thu Oct 03 13:01:31 2024 +0200
@@ -30,6 +30,21 @@
"cong" rules, notably for congproc implementations.
+*** Isabelle/VSCode Prover IDE ***
+
+* General improvements: Persistent decorations for PIDE markup, correct
+ font and formatting in panels, and proper completions.
+ Moreover, the PIDE extension of the LSP now features additional
+ protocol messages (e.g. to obtain the set of Isabelle symbols) and
+ more fine-grained control for unicode symbols.
+
+* Active "sendback" markup can now be used via LSP code actions, e.g.
+ to insert proof methods from Sledgehammer output.
+
+* Relevant Isabelle options can now be overriden from the
+ Isabelle/VSCode extension settings.
+
+
*** HOL ***
* Various declaration bundles support adhoc modification of notation,
--- a/etc/build.props Wed Oct 02 23:47:07 2024 +0200
+++ b/etc/build.props Thu Oct 03 13:01:31 2024 +0200
@@ -262,6 +262,7 @@
src/Tools/VSCode/src/dynamic_output.scala \
src/Tools/VSCode/src/language_server.scala \
src/Tools/VSCode/src/lsp.scala \
+ src/Tools/VSCode/src/pretty_text_panel.scala \
src/Tools/VSCode/src/preview_panel.scala \
src/Tools/VSCode/src/state_panel.scala \
src/Tools/VSCode/src/vscode_main.scala \
--- a/src/HOL/Data_Structures/Define_Time_Function.thy Wed Oct 02 23:47:07 2024 +0200
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy Thu Oct 03 13:01:31 2024 +0200
@@ -10,8 +10,8 @@
theory Define_Time_Function
imports Main
keywords "time_fun" :: thy_decl
- and "time_function" :: thy_goal
- and "time_definition" :: thy_goal
+ and "time_function" :: thy_decl
+ and "time_definition" :: thy_decl
and "equations"
and "time_fun_0" :: thy_decl
begin
--- a/src/Pure/General/json.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Pure/General/json.scala Thu Oct 03 13:01:31 2024 +0200
@@ -25,7 +25,7 @@
type T = Map[String, JSON.T]
val empty: Object.T = Map.empty
- def apply(entries: Entry*): Object.T = Map(entries:_*)
+ def apply(entries: Entry*): Object.T = entries.toMap
def unapply(obj: Any): Option[Object.T] =
obj match {
--- a/src/Pure/PIDE/line.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Pure/PIDE/line.scala Thu Oct 03 13:01:31 2024 +0200
@@ -118,12 +118,15 @@
sealed case class Document(lines: List[Line]) {
lazy val text_length: Text.Offset = Document.length(lines)
- def text_range: Text.Range = Text.Range(0, text_length)
+ def full_range: Text.Range = Text.Range(0, text_length)
lazy val text: String = Document.text(lines)
def get_text(range: Text.Range): Option[String] =
- if (text_range.contains(range)) Some(range.substring(text)) else None
+ if (full_range.contains(range)) Some(range.substring(text)) else None
+
+ def get_text(range: Line.Range): Option[String] =
+ text_range(range).flatMap(get_text)
override def toString: String = text
@@ -170,6 +173,12 @@
else None
}
+ def text_range(line_range: Range): Option[Text.Range] =
+ for {
+ start <- offset(line_range.start)
+ stop <- offset(line_range.stop)
+ } yield Text.Range(start, stop)
+
def change(remove: Range, insert: String): Option[(List[Text.Edit], Document)] = {
for {
edit_start <- offset(remove.start)
--- a/src/Pure/System/options.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Pure/System/options.scala Thu Oct 03 13:01:31 2024 +0200
@@ -109,6 +109,7 @@
val TAG_UPDATE = "update" // relevant for "isabelle update"
val TAG_CONNECTION = "connection" // private information about connections (password etc.)
val TAG_COLOR_DIALOG = "color_dialog" // special color selection dialog
+ val TAG_VSCODE = "vscode" // relevant for "isabelle vscode" and "isabelle vscode_server"
case class Entry(
public: Boolean,
@@ -156,6 +157,7 @@
def for_document: Boolean = for_tag(TAG_DOCUMENT)
def for_color_dialog: Boolean = for_tag(TAG_COLOR_DIALOG)
def for_build_sync: Boolean = for_tag(TAG_BUILD_SYNC)
+ def for_vscode: Boolean = for_tag(TAG_VSCODE)
def session_content: Boolean = for_content || for_document
}
--- a/src/Tools/VSCode/README.md Wed Oct 02 23:47:07 2024 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-# Isabelle/VSCode development #
-
-## System requirements ##
-
-* install default node.js (e.g. via Ubuntu package)
-
-* update to recent stable version:
-
- sudo npm cache clean -f
- sudo npm install -g n
- sudo n stable
-
-* install add-on tools:
-
- sudo npm install -g yarn vsce
-
-
-## Edit and debug ##
-
-* Shell commands within $ISABELLE_HOME directory:
-
- isabelle component_vscode_extension -U
- isabelle vscode src/Tools/VSCode/extension
-
-* VSCode commands:
- Run / Start Debugging (F5)
- File / Open Folder: e.g. `src/HOL/Examples/` then open .thy files
-
-
-## Build and install ##
-
- isabelle component_vscode_extension -I
--- a/src/Tools/VSCode/etc/options Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/etc/options Thu Oct 03 13:01:31 2024 +0200
@@ -1,31 +1,37 @@
(* :mode=isabelle-options: *)
-option vscode_input_delay : real = 0.1
+option vscode_input_delay : real = 0.1 for vscode
-- "delay for client input (edits)"
-option vscode_output_delay : real = 0.5
+option vscode_output_delay : real = 0.5 for vscode
-- "delay for client output (rendering)"
-option vscode_load_delay : real = 0.5
+option vscode_load_delay : real = 0.5 for vscode
-- "delay for file load operations"
-option vscode_tooltip_margin : int = 60
+option vscode_tooltip_margin : int = 60 for vscode
-- "margin for pretty-printing of tooltips"
-option vscode_message_margin : int = 80
+option vscode_message_margin : int = 80 for vscode
-- "margin for pretty-printing of diagnostic messages"
-option vscode_timing_threshold : real = 0.1
+option vscode_timing_threshold : real = 0.1 for vscode
-- "default threshold for timing display (seconds)"
-option vscode_pide_extensions : bool = false
+option vscode_pide_extensions : bool = false for vscode
-- "use PIDE extensions for Language Server Protocol"
-option vscode_unicode_symbols : bool = false
- -- "output Isabelle symbols via Unicode (according to etc/symbols)"
+option vscode_unicode_symbols_output : bool = false for vscode
+ -- "output Isabelle symbols via Unicode in Output (according to etc/symbols)"
-option vscode_caret_perspective : int = 50
+option vscode_unicode_symbols_edits : bool = false for vscode
+ -- "output Isabelle symbols via Unicode in Edits (according to etc/symbols)"
+
+option vscode_caret_perspective : int = 50 for vscode
-- "number of visible lines above and below the caret (0: unrestricted)"
-option vscode_caret_preview : bool = false
+option vscode_caret_preview : bool = false for vscode
-- "dynamic preview of caret document node"
+
+option vscode_html_output : bool = false for vscode
+ -- "output State and Output in HTML"
--- a/src/Tools/VSCode/extension/MANIFEST Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/extension/MANIFEST Thu Oct 03 13:01:31 2024 +0200
@@ -13,8 +13,6 @@
media/vscode.css
package.json
README.md
-src/abbreviations.ts
-src/completion.ts
src/decorations.ts
src/extension.ts
src/file.ts
@@ -22,11 +20,9 @@
src/lsp.ts
src/output_view.ts
src/platform.ts
-src/prefix_tree.ts
src/preview_panel.ts
src/script_decorations.ts
src/state_panel.ts
-src/symbol.ts
src/vscode_lib.ts
test/extension.test.ts
test/index.ts
--- a/src/Tools/VSCode/extension/isabelle-language.json Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/extension/isabelle-language.json Thu Oct 03 13:01:31 2024 +0200
@@ -44,5 +44,6 @@
["⦃", "⦄"],
["`", "`"],
["\"", "\""]
- ]
+ ],
+ "wordPattern": ".+"
}
--- a/src/Tools/VSCode/extension/media/main.js Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/extension/media/main.js Thu Oct 03 13:01:31 2024 +0200
@@ -1,6 +1,6 @@
(function () {
const vscode = acquireVsCodeApi();
-
+
for (const link of document.querySelectorAll('a[href^="file:"]')) {
link.addEventListener('click', () => {
vscode.postMessage({
@@ -9,19 +9,43 @@
});
});
}
-
+
const auto_update = document.getElementById('auto_update');
- auto_update && auto_update.addEventListener('change', (e) => {
+ auto_update && auto_update.addEventListener('change', e => {
vscode.postMessage({'command': 'auto_update', 'enabled': e.target.checked}) ;
});
const update_button = document.getElementById('update_button');
- update_button && update_button.addEventListener('click', (e) => {
- vscode.postMessage({'command': 'update'})
+ update_button && update_button.addEventListener('click', e => {
+ vscode.postMessage({'command': 'update'})
});
-
+
const locate_button = document.getElementById('locate_button');
- locate_button && locate_button.addEventListener('click', (e) => {
+ locate_button && locate_button.addEventListener('click', e => {
vscode.postMessage({'command': 'locate'});
});
-}());
\ No newline at end of file
+
+ const test_string = "mix";
+ const test_span = document.createElement("span");
+ test_span.textContent = test_string;
+ document.body.appendChild(test_span);
+ const symbol_width = test_span.getBoundingClientRect().width / test_string.length;
+ document.body.removeChild(test_span);
+
+ const get_window_margin = () => {
+ const width = window.innerWidth / symbol_width;
+ const result = Math.max(width - 16, 1); // extra headroom
+ return result;
+ }
+
+ const update_window_width = () => {
+ vscode.postMessage({'command': 'resize', 'margin': get_window_margin()})
+ };
+
+ var timeout;
+ window.onresize = function() {
+ clearTimeout(timeout);
+ timeout = setTimeout(update_window_width, 500);
+ };
+ window.onload = update_window_width;
+}());
--- a/src/Tools/VSCode/extension/media/vscode.css Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/extension/media/vscode.css Thu Oct 03 13:01:31 2024 +0200
@@ -9,12 +9,16 @@
body {
padding: 0 var(--container-paddding);
color: var(--vscode-foreground);
- font-size: var(--vscode-font-size);
- font-weight: var(--vscode-font-weight);
- font-family: var(--vscode-font-family);
+ font-size: var(--vscode-editor-font-size);
+ font-weight: var(--vscode-editor-font-weight);
+ font-family: var(--vscode-editor-font-family);
background-color: var(--vscode-editor-background);
}
+pre {
+ font-family: var(--vscode-editor-font-family);
+}
+
ol,
ul {
padding-left: var(--container-paddding);
@@ -79,7 +83,7 @@
display: block;
width: 100%;
border: none;
- font-family: var(--vscode-font-family);
+ font-family: var(--vscode-editor-font-family);
padding: var(--input-padding-vertical) var(--input-padding-horizontal);
color: var(--vscode-input-foreground);
outline-color: var(--vscode-input-border);
@@ -110,4 +114,4 @@
white-space: -pre-wrap; /* Opera 4-6 */
white-space: -o-pre-wrap; /* Opera 7 */
word-wrap: break-word; /* Internet Explorer 5.5+ */
-}
\ No newline at end of file
+}
--- a/src/Tools/VSCode/extension/package.json Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/extension/package.json Thu Oct 03 13:01:31 2024 +0200
@@ -193,6 +193,7 @@
"configuration": {
"title": "Isabelle",
"properties": {
+ "ISABELLE_OPTIONS": {},
"isabelle.replacement": {
"type": "string",
"default": "non-alphanumeric",
--- a/src/Tools/VSCode/extension/src/abbreviations.ts Wed Oct 02 23:47:07 2024 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,148 +0,0 @@
-/* Author: Denis Paluca, TU Muenchen
-
-Input abbreviation and autocompletion of Isabelle symbols.
-*/
-
-'use strict';
-
-import { ExtensionContext, Range, TextDocumentContentChangeEvent, workspace, WorkspaceEdit } from 'vscode'
-import { Prefix_Tree } from './prefix_tree'
-import * as library from './library'
-import * as vscode_lib from './vscode_lib'
-import * as symbol from './symbol'
-
-const entries: Record<string, string> = {}
-const prefix_tree: Prefix_Tree = new Prefix_Tree()
-
-function register_abbreviations(data: symbol.Entry[], context: ExtensionContext)
-{
- const [min_length, max_length] = set_abbrevs(data)
- const alphanumeric_regex = /[^A-Za-z0-9 ]/
- context.subscriptions.push(
- workspace.onDidChangeTextDocument(e =>
- {
- const doc = e.document
- const mode = vscode_lib.get_replacement_mode()
- if (
- mode === 'none' ||
- doc.languageId !== 'isabelle' ||
- doc.uri.scheme !== 'isabelle'
- ) { return; }
- const edits = new WorkspaceEdit()
-
- const changes = e.contentChanges.slice(0)
- changes.sort((c1, c2) => c1.rangeOffset - c2.rangeOffset)
-
- let c: TextDocumentContentChangeEvent
- while (c = changes.pop()) {
- if (c.rangeLength === 1 || library.has_newline(c.text)) {
- return
- }
-
- const end_offset = c.rangeOffset + c.text.length +
- changes.reduce((a,b) => a + b.text.length, 0)
-
- if (end_offset < min_length) {
- continue
- }
-
- const start_offset = end_offset < max_length ? 0 : end_offset - max_length
-
- const end_pos = doc.positionAt(end_offset)
- let start_pos = doc.positionAt(start_offset)
- let range = new Range(start_pos, end_pos)
- const text = library.reverse(doc.getText(range))
-
- const node = prefix_tree.get_end_or_value(text)
- if (!node || !node.value) {
- continue
- }
-
- const word = node.get_word().join('')
- if (mode === 'non-alphanumeric' && !alphanumeric_regex.test(word)) {
- continue
- }
-
- start_pos = doc.positionAt(end_offset - word.length)
- range = new Range(start_pos, end_pos)
-
- edits.replace(doc.uri, range, node.value as string)
- }
-
- apply_edits(edits)
- })
- )
-}
-
-async function apply_edits(edit: WorkspaceEdit)
-{
- await waitForNextTick()
- await workspace.applyEdit(edit)
-}
-
-function waitForNextTick(): Promise<void> {
- return new Promise((res) => setTimeout(res, 0));
-}
-
-function get_unique_abbrevs(data: symbol.Entry[]): Set<string>
-{
- const unique = new Set<string>()
- const non_unique = new Set<string>()
- for (const {code, abbrevs} of data) {
- for (const abbrev of abbrevs) {
- if (abbrev.length === 1 || non_unique.has(abbrev)) {
- continue
- }
-
- if (unique.has(abbrev)) {
- non_unique.add(abbrev)
- unique.delete(abbrev)
- entries[abbrev] = undefined
- continue
- }
-
-
- entries[abbrev] = String.fromCharCode(code)
- unique.add(abbrev)
- }
- }
- return unique
-}
-
-function set_abbrevs(data: symbol.Entry[]): [number, number]
-{
- const unique = get_unique_abbrevs(data)
-
- // Add white space to abbrevs which are prefix of other abbrevs
- for (const a1 of unique) {
- for (const a2 of unique) {
- if (a1 === a2) {
- continue
- }
-
- if (a2.startsWith(a1)) {
- const val = entries[a1]
- delete entries[a1]
- entries[a1 + ' '] = val
- break
- }
- }
- }
-
- let min_length: number
- let max_length: number
- for (const entry in entries) {
- if (!min_length || min_length > entry.length)
- min_length = entry.length
-
- if (!max_length || max_length< entry.length)
- max_length = entry.length
-
- // add reverse because we check the abbrevs from the end
- prefix_tree.insert(library.reverse(entry), entries[entry])
- }
-
- return [min_length, max_length]
-}
-
-export { register_abbreviations }
--- a/src/Tools/VSCode/extension/src/completion.ts Wed Oct 02 23:47:07 2024 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-/* Author: Makarius
-
-Support for PIDE completion information.
-*/
-
-'use strict';
-
-import { CompletionItemProvider, CompletionItem, TextDocument, Range, Position,
- CancellationToken, CompletionList } from 'vscode'
-
-export class Completion_Provider implements CompletionItemProvider
-{
- public provideCompletionItems(
- document: TextDocument, position: Position, token: CancellationToken): CompletionList
- {
- const line_text = document.lineAt(position).text
-
- return new CompletionList([])
- }
-}
--- a/src/Tools/VSCode/extension/src/decorations.ts Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts Thu Oct 03 13:01:31 2024 +0200
@@ -164,11 +164,11 @@
/* decoration for document node */
type Content = Range[] | DecorationOptions[]
-const document_decorations = new Map<Uri, Map<string, Content>>()
+const document_decorations = new Map<string, Map<string, Content>>()
export function close_document(document: TextDocument)
{
- document_decorations.delete(document.uri)
+ document_decorations.delete(document.uri.toString())
}
export function apply_decoration(decorations: Document_Decorations)
@@ -187,12 +187,12 @@
}
})
- const document = document_decorations.get(uri) || new Map<string, Content>()
+ const document = document_decorations.get(uri.toString()) || new Map<string, Content>()
document.set(decoration.type, content)
- document_decorations.set(uri, document)
+ document_decorations.set(uri.toString(), document)
for (const editor of window.visibleTextEditors) {
- if (uri.toString === editor.document.uri.toString) {
+ if (uri.toString() === editor.document.uri.toString()) {
editor.setDecorations(typ, content)
}
}
@@ -203,7 +203,7 @@
export function update_editor(editor: TextEditor)
{
if (editor) {
- const decorations = document_decorations.get(editor.document.uri)
+ const decorations = document_decorations.get(editor.document.uri.toString())
if (decorations) {
for (const [typ, content] of decorations) {
editor.setDecorations(types.get(typ), content)
--- a/src/Tools/VSCode/extension/src/extension.ts Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Thu Oct 03 13:01:31 2024 +0200
@@ -10,7 +10,6 @@
import * as platform from './platform'
import * as library from './library'
import * as file from './file'
-import * as symbol from './symbol'
import * as vscode_lib from './vscode_lib'
import * as decorations from './decorations'
import * as preview_panel from './preview_panel'
@@ -63,10 +62,6 @@
}
}
- add("-o"); add("vscode_unicode_symbols")
- add("-o"); add("vscode_pide_extensions")
- add_values("-o", "options")
-
add_value("-A", "logic_ancestor")
if (args.logic) { add_value(args.logic_requirements ? "-R" : "-l", "logic") }
@@ -76,6 +71,17 @@
add_value("-L", "log_file")
if (args.verbose) { add("-v") }
+ const config = workspace.getConfiguration("isabelle.options")
+ Object.keys(config).forEach(key =>
+ {
+ const value = config[key]
+ if (typeof value == "string" && value !== "")
+ {
+ add("-o"); add(`${key}=${value}`)
+ }
+ })
+ add_values("-o", "options")
+
return result
}
@@ -180,8 +186,8 @@
language_client.onReady().then(() =>
{
context.subscriptions.push(
- window.onDidChangeActiveTextEditor(_ => update_caret()),
- window.onDidChangeTextEditorSelection(_ => update_caret()))
+ window.onDidChangeActiveTextEditor(update_caret),
+ window.onDidChangeTextEditorSelection(update_caret))
update_caret()
language_client.onNotification(lsp.caret_update_type, goto_file)
@@ -190,7 +196,7 @@
/* dynamic output */
- const provider = new Output_View_Provider(context.extensionUri)
+ const provider = new Output_View_Provider(context.extensionUri, language_client)
context.subscriptions.push(
window.registerWebviewViewProvider(Output_View_Provider.view_type, provider))
--- a/src/Tools/VSCode/extension/src/lsp.ts Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/extension/src/lsp.ts Thu Oct 03 13:01:31 2024 +0200
@@ -7,7 +7,7 @@
'use strict';
import { MarkdownString } from 'vscode'
-import { NotificationType } from 'vscode-languageclient'
+import { NotificationType, RequestType0 } from 'vscode-languageclient'
/* decorations */
@@ -32,6 +32,15 @@
new NotificationType<Document_Decorations>("PIDE/decoration")
+export interface Decoration_Request
+{
+ uri: string
+}
+
+export const decoration_request_type =
+ new NotificationType<Decoration_Request>("PIDE/decoration_request")
+
+
/* caret handling */
export interface Caret_Update
@@ -56,6 +65,13 @@
export const dynamic_output_type =
new NotificationType<Dynamic_Output>("PIDE/dynamic_output")
+export interface Output_Set_Margin
+{
+ margin: number
+}
+
+export const output_set_margin_type =
+ new NotificationType<Output_Set_Margin>("PIDE/output_set_margin")
/* state */
@@ -69,6 +85,15 @@
export const state_output_type =
new NotificationType<State_Output>("PIDE/state_output")
+export interface State_Set_Margin
+{
+ id: number
+ margin: number
+}
+
+export const state_set_margin_type =
+ new NotificationType<State_Set_Margin>("PIDE/state_set_margin")
+
export interface State_Id
{
id: number
@@ -80,7 +105,7 @@
enabled: boolean
}
-export const state_init_type = new NotificationType<void>("PIDE/state_init")
+export const state_init_type = new RequestType0("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")
--- a/src/Tools/VSCode/extension/src/output_view.ts Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/extension/src/output_view.ts Thu Oct 03 13:01:31 2024 +0200
@@ -10,6 +10,8 @@
import { text_colors } from './decorations'
import * as vscode_lib from './vscode_lib'
import * as path from 'path'
+import * as lsp from './lsp'
+import { LanguageClient } from 'vscode-languageclient/node';
class Output_View_Provider implements WebviewViewProvider
@@ -20,7 +22,10 @@
private _view?: WebviewView
private content: string = ''
- constructor(private readonly _extension_uri: Uri) { }
+ constructor(
+ private readonly _extension_uri: Uri,
+ private readonly _language_client: LanguageClient
+ ) { }
public resolveWebviewView(
view: WebviewView,
@@ -40,9 +45,15 @@
view.webview.html = this._get_html(this.content)
view.webview.onDidReceiveMessage(async message =>
- {
- if (message.command === 'open') {
- open_webview_link(message.link)
+ {
+ switch (message.command) {
+ case "open":
+ open_webview_link(message.link)
+ break
+ case "resize":
+ this._language_client.sendNotification(
+ lsp.output_set_margin_type, { margin: message.margin })
+ break
}
})
}
@@ -78,6 +89,8 @@
{
const script_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'main.js')))
const css_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'vscode.css')))
+ const font_uri =
+ webview.asWebviewUri(Uri.file(path.join(extension_path, 'fonts', 'IsabelleDejaVuSansMono.ttf')))
return `<!DOCTYPE html>
<html lang='en'>
@@ -86,7 +99,11 @@
<meta name='viewport' content='width=device-width, initial-scale=1.0'>
<link href='${css_uri}' rel='stylesheet' type='text/css'>
<style>
- ${_get_decorations()}
+ @font-face {
+ font-family: "Isabelle DejaVu Sans Mono";
+ src: url(${font_uri});
+ }
+ ${_get_decorations()}
</style>
<title>Output</title>
</head>
--- a/src/Tools/VSCode/extension/src/prefix_tree.ts Wed Oct 02 23:47:07 2024 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-/* Author: Denis Paluca, TU Muenchen
-
-Prefix tree for symbol autocompletion.
-*/
-
-'use strict';
-
-class Tree_Node
-{
- public key: number | string
- public parent: Tree_Node = null
- public end: boolean = false
- public value: number[] | string
- public children: Record<number | string, Tree_Node> = {}
- constructor(key: number | string)
- {
- this.key = key
- }
-
- public get_word(): number[] | string[]
- {
- let output = []
- let node: Tree_Node = this
-
- while (node.key !== null) {
- output.unshift(node.key)
- node = node.parent
- }
-
- return output
- }
-}
-
-class Prefix_Tree
-{
- private root: Tree_Node
-
- constructor()
- {
- this.root = new Tree_Node(null)
- }
-
- public insert(word: number[] | string, value: number[] | string)
- {
- let node = this.root
- for (var i = 0; i < word.length; i++) {
- if (!node.children[word[i]]) {
- node.children[word[i]] = new Tree_Node(word[i])
-
- node.children[word[i]].parent = node
- }
-
- node = node.children[word[i]]
- node.end = false
-
- if (i === word.length-1) {
- node.end = true
- node.value = value
- }
- }
- }
-
- public get_node(prefix: number[] | string): Tree_Node | undefined
- {
- let node = this.root
-
- for (let i = 0; i < prefix.length; i++) {
- if (!node.children[prefix[i]]) {
- return
- }
- node = node.children[prefix[i]]
- }
- return node
- }
-
- public get_end_or_value(prefix: number[] | string): Tree_Node | undefined
- {
- let node = this.root
- let resNode: Tree_Node
- for (let i = 0; i < prefix.length; i++) {
- if (!node.children[prefix[i]]) {
- return resNode
- }
- node = node.children[prefix[i]]
- if (node.value) {
- resNode = node
- }
-
- if (node.end) {
- return node
- }
- }
- return node
- }
-}
-
-export { Prefix_Tree, Tree_Node }
--- a/src/Tools/VSCode/extension/src/state_panel.ts Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/extension/src/state_panel.ts Thu Oct 03 13:01:31 2024 +0200
@@ -61,6 +61,10 @@
case "open":
open_webview_link(message.link)
break
+ case "resize":
+ language_client.sendNotification(
+ lsp.state_set_margin_type, { id: this.state_id, margin: message.margin })
+ break
default:
break
}
@@ -97,7 +101,7 @@
{
if (language_client) {
if (panel) panel.reveal()
- else language_client.sendNotification(lsp.state_init_type)
+ else language_client.sendRequest(lsp.state_init_type, null)
}
}
--- a/src/Tools/VSCode/extension/src/symbol.ts Wed Oct 02 23:47:07 2024 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-/* Author: Makarius
-
-Isabelle text symbols versus UTF-8/Unicode encoding. See also:
-
- - Pure/General/symbol.scala
- - Pure/General/utf8.scala
- - https://encoding.spec.whatwg.org
-*/
-
-'use strict';
-
-import * as file from './file'
-import * as library from './library'
-
-
-/* ASCII characters */
-
-export type Symbol = string
-
-export function is_char(s: Symbol): boolean
-{ return s.length === 1 }
-
-export function is_ascii_letter(s: Symbol): boolean
-{ return is_char(s) && "A" <= s && s <= "Z" || "a" <= s && s <= "z" }
-
-export function is_ascii_digit(s: Symbol): boolean
-{ return is_char(s) && "0" <= s && s <= "9" }
-
-export function is_ascii_quasi(s: Symbol): boolean
-{ return s === "_" || s === "'" }
-
-export function is_ascii_letdig(s: Symbol): boolean
-{ return is_ascii_letter(s) || is_ascii_digit(s) || is_ascii_quasi(s) }
-
-export function is_ascii_identifier(s: Symbol): boolean
-{
- const n = s.length
-
- let all_letdig = true
- for (const c of s) { all_letdig = all_letdig && is_ascii_letdig(c) }
-
- return n > 0 && is_ascii_letter(s.charAt(0)) && all_letdig
-}
-
-
-/* defined symbols */
-
-export interface Entry {
- symbol: string;
- name: string;
- abbrevs: string[];
- code?: number;
-}
-
-export class Symbols
-{
- entries: Entry[]
- private entries_map: Map<Symbol, Entry>
-
- constructor(entries: Entry[])
- {
- this.entries = entries
- this.entries_map = new Map<Symbol, Entry>()
- for (const entry of entries) {
- this.entries_map.set(entry.symbol, entry)
- }
- }
-
- public get(sym: Symbol): Entry | undefined
- {
- return this.entries_map.get(sym)
- }
-
- public defined(sym: Symbol): boolean
- {
- return this.entries_map.has(sym)
- }
-}
-
-function load_symbols(): Entry[]
-{
- const vscodium_resources = library.getenv("ISABELLE_VSCODIUM_RESOURCES")
- if (vscodium_resources) {
- const path = vscodium_resources + "/vscodium/out/vs/base/browser/ui/fonts/symbols.json"
- return file.read_json_sync(file.platform_path(path))
- }
- else { return [] }
-}
-
-export const symbols: Symbols = new Symbols(load_symbols())
--- a/src/Tools/VSCode/src/component_vscode_extension.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/src/component_vscode_extension.scala Thu Oct 03 13:01:31 2024 +0200
@@ -132,6 +132,51 @@
}
""")
}
+
+
+ private def options_json(options: Options): String = {
+ val relevant_options =
+ Set(
+ "editor_output_state",
+ "auto_time_start",
+ "auto_time_limit",
+ "auto_nitpick",
+ "auto_sledgehammer",
+ "auto_methods",
+ "auto_quickcheck",
+ "auto_solve_direct",
+ "sledgehammer_provers",
+ "sledgehammer_timeout")
+
+ (for {
+ opt <- options.iterator
+ if opt.for_vscode || opt.for_content || relevant_options.contains(opt.name)
+ } yield {
+ val (enum_values, enum_descriptions) = opt.typ match {
+ case Options.Bool => (
+ Some(List("", "true", "false")),
+ Some(List("Use System Preference.", "Enable.", "Disable.")))
+ case _ => (None, None)
+ }
+
+ val default = opt.name match {
+ case "vscode_unicode_symbols_output" => "true"
+ case "vscode_unicode_symbols_edits" => "true"
+ case "vscode_pide_extensions" => "true"
+ case "vscode_html_output" => "true"
+ case _ => ""
+ }
+
+ quote("isabelle.options." + opt.name) + ": " +
+ JSON.Format(
+ JSON.Object(
+ "type" -> "string",
+ "default" -> default,
+ "description" -> opt.description) ++
+ JSON.optional("enum" -> enum_values) ++
+ JSON.optional("enumDescriptions" -> enum_descriptions)) + ","
+ }).mkString
+ }
/* build extension */
@@ -160,20 +205,36 @@
Isabelle_System.with_tmp_dir("build") { build_dir =>
val manifest_text = File.read(VSCode_Main.extension_dir + VSCode_Main.MANIFEST)
val manifest_entries = split_lines(manifest_text).filter(_.nonEmpty)
- val manifest_shasum: SHA1.Shasum = {
- val a = SHA1.shasum_meta_info(SHA1.digest(manifest_text))
- val bs =
- for (name <- manifest_entries)
- yield SHA1.shasum(SHA1.digest(VSCode_Main.extension_dir + Path.explode(name)), name)
- SHA1.flat_shasum(a :: bs)
- }
for (name <- manifest_entries) {
val path = Path.explode(name)
Isabelle_System.copy_file(VSCode_Main.extension_dir + path,
Isabelle_System.make_directory(build_dir + path.dir))
}
+
+ val fonts_dir = Isabelle_System.make_directory(build_dir + Path.basic("fonts"))
+ for (entry <- Isabelle_Fonts.fonts()) { Isabelle_System.copy_file(entry.path, fonts_dir) }
+ val manifest_text2 =
+ manifest_text + cat_lines(Isabelle_Fonts.fonts().map(e => "fonts/" + e.path.file_name))
+ val manifest_entries2 = split_lines(manifest_text2).filter(_.nonEmpty)
+
+ val manifest_shasum: SHA1.Shasum = {
+ val a = SHA1.shasum_meta_info(SHA1.digest(manifest_text2))
+ val bs =
+ for (name <- manifest_entries2)
+ yield SHA1.shasum(SHA1.digest(build_dir + Path.explode(name)), name)
+ SHA1.flat_shasum(a :: bs)
+ }
File.write(build_dir + VSCode_Main.MANIFEST.shasum, manifest_shasum.toString)
+
+ /* options */
+
+ val opt_json = options_json(options)
+ val package_path = build_dir + Path.basic("package.json")
+ val package_body = File.read(package_path).replace("\"ISABELLE_OPTIONS\": {},", opt_json)
+ File.write(package_path, package_body)
+
+
build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress)
val result =
--- a/src/Tools/VSCode/src/dynamic_output.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala Thu Oct 03 13:01:31 2024 +0200
@@ -11,58 +11,35 @@
object Dynamic_Output {
- sealed case class State(do_update: Boolean = true, output: List[XML.Tree] = Nil) {
- def handle_update(
- resources: VSCode_Resources,
- channel: Channel,
- restriction: Option[Set[Command]]
- ): State = {
- val st1 =
- resources.get_caret() match {
- case None => copy(output = Nil)
- case Some(caret) =>
- val snapshot = resources.snapshot(caret.model)
- if (do_update && !snapshot.is_outdated) {
- snapshot.current_command(caret.node_name, caret.offset) match {
- case None => copy(output = Nil)
- case Some(command) =>
- copy(output =
- if (restriction.isEmpty || restriction.get.contains(command)) {
- val output_state = resources.options.bool("editor_output_state")
- Rendering.output_messages(snapshot.command_results(command), output_state)
- } else output)
- }
- }
- else this
- }
- if (st1.output != output) {
- val node_context =
- new Browser_Info.Node_Context {
- override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
- for {
- thy_file <- Position.Def_File.unapply(props)
- def_line <- Position.Def_Line.unapply(props)
- source <- resources.source_file(thy_file)
- uri = File.uri(Path.explode(source).absolute_file)
- } yield HTML.link(uri.toString + "#" + def_line, body)
- }
- val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
- val html = node_context.make_html(elements, Pretty.separate(st1.output))
- channel.write(LSP.Dynamic_Output(HTML.source(html).toString))
- }
- st1
- }
- }
-
def apply(server: Language_Server): Dynamic_Output = new Dynamic_Output(server)
}
+class Dynamic_Output private(server: Language_Server) {
+ private val pretty_panel_ = Synchronized(None: Option[Pretty_Text_Panel])
+ def pretty_panel: Pretty_Text_Panel =
+ pretty_panel_.value.getOrElse(error("No Pretty Panel for Dynamic Output"))
-class Dynamic_Output private(server: Language_Server) {
- private val state = Synchronized(Dynamic_Output.State())
-
- private def handle_update(restriction: Option[Set[Command]]): Unit =
- state.change(_.handle_update(server.resources, server.channel, restriction))
+ private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = {
+ val output =
+ server.resources.get_caret() match {
+ case None => Some(Nil)
+ case Some(caret) =>
+ val snapshot = server.resources.snapshot(caret.model)
+ snapshot.current_command(caret.node_name, caret.offset) match {
+ case None => Some(Nil)
+ case Some(command) =>
+ if (restriction.isEmpty || restriction.get.contains(command)) {
+ val output_state = server.resources.options.bool("editor_output_state")
+ Some(Rendering.output_messages(snapshot.command_results(command), output_state))
+ } else None
+ }
+ }
+
+ output match {
+ case None =>
+ case Some(output) => pretty_panel.refresh(output)
+ }
+ }
/* main */
@@ -79,6 +56,11 @@
def init(): Unit = {
server.session.commands_changed += main
server.session.caret_focus += main
+ pretty_panel_.change(_ =>
+ Some(Pretty_Text_Panel(
+ server.resources,
+ server.channel,
+ LSP.Dynamic_Output.apply)))
handle_update(None)
}
@@ -86,4 +68,8 @@
server.session.commands_changed -= main
server.session.caret_focus -= main
}
+
+ def set_margin(margin: Double): Unit = {
+ pretty_panel.update_margin(margin)
+ }
}
--- a/src/Tools/VSCode/src/language_server.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Thu Oct 03 13:01:31 2024 +0200
@@ -166,18 +166,7 @@
version: Long,
changes: List[LSP.TextDocumentChange]
): Unit = {
- val norm_changes = new mutable.ListBuffer[LSP.TextDocumentChange]
- @tailrec def norm(chs: List[LSP.TextDocumentChange]): Unit = {
- if (chs.nonEmpty) {
- val (full_texts, rest1) = chs.span(_.range.isEmpty)
- val (edits, rest2) = rest1.span(_.range.nonEmpty)
- norm_changes ++= full_texts
- norm_changes ++= edits.sortBy(_.range.get.start)(Line.Position.Ordering).reverse
- norm(rest2)
- }
- }
- norm(changes)
- norm_changes.foreach(change =>
+ changes.foreach(change =>
resources.change_model(session, editor, file, version, change.text, change.range))
delay_input.invoke()
@@ -208,7 +197,7 @@
if (preview_panel.flush(channel)) delay_preview.invoke()
}
- private def request_preview(file: JFile, column: Int): Unit = {
+ private def preview_request(file: JFile, column: Int): Unit = {
preview_panel.request(file, column)
delay_preview.invoke()
}
@@ -239,10 +228,16 @@
private val syslog_messages =
Session.Consumer[Prover.Output](getClass.getName) {
- case output => channel.log_writeln(resources.output_xml(output.message))
+ case output => channel.log_writeln(resources.output_xml_text(output.message))
}
+ /* decoration request */
+
+ private def decoration_request(file: JFile): Unit =
+ resources.force_decorations(channel, file)
+
+
/* init and exit */
def init(id: LSP.Id): Unit = {
@@ -424,6 +419,80 @@
}
+ /* code actions */
+
+ def code_action_request(id: LSP.Id, file: JFile, range: Line.Range): Unit = {
+ def extract_sendbacks(body: XML.Body): List[(String, Properties.T)] = {
+ body match {
+ case XML.Elem(Markup(Markup.SENDBACK, p), b) :: rest =>
+ (XML.content(b), p) :: extract_sendbacks(rest)
+ case XML.Elem(m, b) :: rest => extract_sendbacks(b ++ rest)
+ case e :: rest => extract_sendbacks(rest)
+ case Nil => Nil
+ }
+ }
+
+ for {
+ model <- resources.get_model(file)
+ version <- model.version
+ snapshot = resources.snapshot(model)
+ doc = model.content.doc
+ text_range <- doc.text_range(range)
+ text_range2 = Text.Range(text_range.start - 1, text_range.stop + 1)
+ } {
+ val edits = snapshot
+ .select(
+ text_range2,
+ Markup.Elements.full,
+ command_states => _ => Some(command_states.flatMap(_.results.iterator.map(_._2).toList)))
+ .flatMap(info => extract_sendbacks(info.info).flatMap {
+ (s, p) =>
+ for {
+ id <- Position.Id.unapply(p)
+ (node, command) <- snapshot.find_command(id)
+ start <- node.command_start(command)
+ range = command.core_range + start
+ current_text <- model.get_text(range)
+ line_range = doc.range(range)
+
+ whole_line = doc.lines(line_range.start.line)
+ indent = whole_line.text.takeWhile(_.isWhitespace)
+ padding = p.contains(Markup.PADDING_COMMAND)
+
+ indented_text = Library.prefix_lines(indent, s)
+ edit_text =
+ resources.output_edit(
+ if (padding) current_text + "\n" + indented_text else current_text + s)
+ edit = LSP.TextEdit(line_range, edit_text)
+ } yield (s, edit)
+ })
+ .distinct
+
+ val actions = edits.map((name, edit) => {
+ val text_edits = List(LSP.TextDocumentEdit(file, Some(version), List(edit)))
+
+ LSP.CodeAction(name, text_edits)
+ })
+ val reply = LSP.CodeActionRequest.reply(id, actions)
+
+ channel.write(reply)
+ }
+ }
+
+
+ /* symbols */
+
+ def symbols_request(id: LSP.Id): Unit = {
+ val symbols = Component_VSCodium.symbols
+ channel.write(LSP.Symbols_Request.reply(id, symbols))
+ }
+
+ def symbols_convert_request(id: LSP.Id, text: String, unicode: Boolean): Unit = {
+ val converted = Symbol.output(unicode, text)
+ channel.write(LSP.Symbols_Convert_Request.reply(id, converted))
+ }
+
+
/* main loop */
def start(): Unit = {
@@ -451,13 +520,21 @@
case LSP.Hover(id, node_pos) => hover(id, node_pos)
case LSP.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
case LSP.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
+ case LSP.CodeActionRequest(id, file, range) => code_action_request(id, file, range)
+ case LSP.Decoration_Request(file) => decoration_request(file)
case LSP.Caret_Update(caret) => update_caret(caret)
- case LSP.State_Init(()) => State_Panel.init(server)
- case LSP.State_Exit(id) => State_Panel.exit(id)
- case LSP.State_Locate(id) => State_Panel.locate(id)
- case LSP.State_Update(id) => State_Panel.update(id)
- case LSP.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
- case LSP.Preview_Request(file, column) => request_preview(file, column)
+ case LSP.Output_Set_Margin(margin) => dynamic_output.set_margin(margin)
+ case LSP.State_Init(id) => State_Panel.init(id, server)
+ case LSP.State_Exit(state_id) => State_Panel.exit(state_id)
+ case LSP.State_Locate(state_id) => State_Panel.locate(state_id)
+ case LSP.State_Update(state_id) => State_Panel.update(state_id)
+ case LSP.State_Auto_Update(state_id, enabled) =>
+ State_Panel.auto_update(state_id, enabled)
+ case LSP.State_Set_Margin(state_id, margin) => State_Panel.set_margin(state_id, margin)
+ case LSP.Symbols_Request(id) => symbols_request(id)
+ case LSP.Symbols_Convert_Request(id, text, boolean) =>
+ symbols_convert_request(id, text, boolean)
+ case LSP.Preview_Request(file, column) => preview_request(file, column)
case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
}
}
--- a/src/Tools/VSCode/src/lsp.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala Thu Oct 03 13:01:31 2024 +0200
@@ -109,7 +109,10 @@
def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
if (error == "") apply(id, result = result)
- else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
+ else {
+ apply(id, error =
+ Some(ResponseError(code = ErrorCodes.jsonrpcReservedErrorRangeEnd, message = error)))
+ }
def is_empty(json: JSON.T): Boolean =
JSON.string(json, "id") == Some("") && JSON.value(json, "result").isDefined
@@ -126,10 +129,20 @@
val MethodNotFound = -32601
val InvalidParams = -32602
val InternalError = -32603
- val serverErrorStart = -32099
- val serverErrorEnd = -32000
+
+ val jsonrpcReservedErrorRangeStart = -32099
+ val ServerNotInitialized = -32002
+ val UnknownErrorCode = -32001
+ val jsonrpcReservedErrorRangeEnd = -32000
+
+ val lspReservedErrorRangeStart = -32899
+ val RequestFailed = -32803
+ val ServerCancelled = -32802
+ val ContentModified = -32801
+ val RequestCancelled = -32800
+ val lspReservedErrorRangeEnd = -32800
}
-
+
/* init and exit */
@@ -146,11 +159,13 @@
"completionProvider" -> JSON.Object(
"resolveProvider" -> false,
"triggerCharacters" ->
- Symbol.symbols.entries.flatMap(_.abbrevs).flatMap(_.toList).map(_.toString).distinct
+ (Symbol.symbols.entries.flatMap(_.abbrevs).flatMap(_.toList).map(_.toString)
+ ++ Symbol.symbols.entries.map(_.name).flatMap(_.toList).map(_.toString)).distinct
),
"hoverProvider" -> true,
"definitionProvider" -> true,
- "documentHighlightProvider" -> true)
+ "documentHighlightProvider" -> true,
+ "codeActionProvider" -> true)
}
object Initialized extends Notification0("initialized")
@@ -318,27 +333,67 @@
def json: JSON.T = JSON.Object("range" -> Range(range), "newText" -> new_text)
}
- sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit]) {
+ sealed case class TextDocumentEdit(file: JFile, version: Option[Long], edits: List[TextEdit]) {
def json: JSON.T =
JSON.Object(
- "textDocument" -> JSON.Object("uri" -> Url.print_file(file), "version" -> version),
- "edits" -> edits.map(_.json))
+ "textDocument" -> (
+ JSON.Object("uri" -> Url.print_file(file)) ++
+ JSON.optional("version" -> version)
+ ),
+ "edits" -> edits.map(_.json)
+ )
}
object WorkspaceEdit {
def apply(edits: List[TextDocumentEdit]): JSON.T =
+ JSON.Object("documentChanges" -> edits.map(_.json))
+ }
+
+ object ApplyWorkspaceEdit {
+ def apply(edits: List[TextDocumentEdit]): JSON.T =
RequestMessage(Id.empty, "workspace/applyEdit",
- JSON.Object("edit" -> JSON.Object("documentChanges" -> edits.map(_.json))))
+ JSON.Object("edit" -> WorkspaceEdit(edits))
+ )
}
/* completion */
+
+ object CompletionItemKind {
+ val Text = 1;
+ val Method = 2;
+ val Function = 3;
+ val Constructor = 4;
+ val Field = 5;
+ val Variable = 6;
+ val Class = 7;
+ val Interface = 8;
+ val Module = 9;
+ val Property = 10;
+ val Unit = 11;
+ val Value = 12;
+ val Enum = 13;
+ val Keyword = 14;
+ val Snippet = 15;
+ val Color = 16;
+ val File = 17;
+ val Reference = 18;
+ val Folder = 19;
+ val EnumMember = 20;
+ val Constant = 21;
+ val Struct = 22;
+ val Event = 23;
+ val Operator = 24;
+ val TypeParameter = 25;
+ }
sealed case class CompletionItem(
label: String,
kind: Option[Int] = None,
detail: Option[String] = None,
documentation: Option[String] = None,
+ filter_text: Option[String] = None,
+ commit_characters: Option[List[String]] = None,
text: Option[String] = None,
range: Option[Line.Range] = None,
command: Option[Command] = None
@@ -348,9 +403,9 @@
JSON.optional("kind" -> kind) ++
JSON.optional("detail" -> detail) ++
JSON.optional("documentation" -> documentation) ++
- JSON.optional("insertText" -> text) ++
- JSON.optional("range" -> range.map(Range(_))) ++
- JSON.optional("textEdit" -> range.map(r => TextEdit(r, text.getOrElse(label)).json)) ++
+ JSON.optional("filterText" -> filter_text) ++
+ JSON.optional("textEdit" -> range.map(TextEdit(_, text.getOrElse(label)).json)) ++
+ JSON.optional("commitCharacters" -> commit_characters) ++
JSON.optional("command" -> command.map(_.json))
}
@@ -460,6 +515,32 @@
}
+ /* code actions */
+
+ sealed case class CodeAction(title: String, edits: List[TextDocumentEdit]) {
+ def json: JSON.T =
+ JSON.Object("title" -> title, "edit" -> WorkspaceEdit(edits))
+ }
+
+ object CodeActionRequest {
+ def unapply(json: JSON.T): Option[(Id, JFile, Line.Range)] =
+ json match {
+ case RequestMessage(id, "textDocument/codeAction", Some(params)) =>
+ for {
+ doc <- JSON.value(params, "textDocument")
+ uri <- JSON.string(doc, "uri")
+ if Url.is_wellformed_file(uri)
+ range_json <- JSON.value(params, "range")
+ range <- Range.unapply(range_json)
+ } yield (id, Url.absolute_file(uri), range)
+ case _ => None
+ }
+
+ def reply(id: Id, actions: List[CodeAction]): JSON.T =
+ ResponseMessage(id, Some(actions.map(_.json)))
+ }
+
+
/* decorations */
sealed case class Decoration_Options(range: Line.Range, hover_message: List[MarkedString]) {
@@ -468,16 +549,31 @@
JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
}
- sealed case class Decoration(decorations: List[(String, List[Decoration_Options])]) {
+ type Decoration_List = List[(String, List[Decoration_Options])]
+
+ sealed case class Decoration(decorations: Decoration_List) {
+ def json_entries: JSON.T =
+ decorations.map(decoration => JSON.Object(
+ "type" -> decoration._1,
+ "content" -> decoration._2.map(_.json)))
+
def json(file: JFile): JSON.T =
Notification("PIDE/decoration",
JSON.Object(
"uri" -> Url.print_file(file),
- "entries" -> decorations.map(decoration => JSON.Object(
- "type" -> decoration._1,
- "content" -> decoration._2.map(_.json))
- ))
- )
+ "entries" -> json_entries))
+ }
+
+ object Decoration_Request {
+ def unapply(json: JSON.T): Option[JFile] =
+ json match {
+ case Notification("PIDE/decoration_request", Some(params)) =>
+ for {
+ uri <- JSON.string(params, "uri")
+ if Url.is_wellformed_file(uri)
+ } yield Url.absolute_file(uri)
+ case _ => None
+ }
}
@@ -510,17 +606,34 @@
/* dynamic output */
object Dynamic_Output {
- def apply(content: String): JSON.T =
- Notification("PIDE/dynamic_output", JSON.Object("content" -> content))
+ def apply(content: String, decoration: Option[Decoration] = None): JSON.T =
+ Notification("PIDE/dynamic_output",
+ JSON.Object("content" -> content) ++
+ JSON.optional("decorations" -> decoration.map(_.json_entries)))
+ }
+
+ object Output_Set_Margin {
+ def unapply(json: JSON.T): Option[Double] =
+ json match {
+ case Notification("PIDE/output_set_margin", Some(params)) =>
+ JSON.double(params, "margin")
+ case _ => None
+ }
}
/* state output */
object State_Output {
- def apply(id: Counter.ID, content: String, auto_update: Boolean): JSON.T =
+ def apply(
+ id: Counter.ID,
+ content: String,
+ auto_update: Boolean,
+ decorations: Option[Decoration] = None
+ ): JSON.T =
Notification("PIDE/state_output",
- JSON.Object("id" -> id, "content" -> content, "auto_update" -> auto_update))
+ JSON.Object("id" -> id, "content" -> content, "auto_update" -> auto_update) ++
+ JSON.optional("decorations" -> decorations.map(_.json_entries)))
}
class State_Id_Notification(name: String) {
@@ -531,7 +644,11 @@
}
}
- object State_Init extends Notification0("PIDE/state_init")
+ object State_Init extends Request0("PIDE/state_init") {
+ def reply(id: Id, state_id: Counter.ID): JSON.T =
+ ResponseMessage(id, Some(JSON.Object("state_id" -> state_id)))
+ }
+
object State_Exit extends State_Id_Notification("PIDE/state_exit")
object State_Locate extends State_Id_Notification("PIDE/state_locate")
object State_Update extends State_Id_Notification("PIDE/state_update")
@@ -548,6 +665,53 @@
}
}
+ object State_Set_Margin {
+ def unapply(json: JSON.T): Option[(Counter.ID, Double)] =
+ json match {
+ case Notification("PIDE/state_set_margin", Some(params)) =>
+ for {
+ id <- JSON.long(params, "id")
+ margin <- JSON.double(params, "margin")
+ } yield (id, margin)
+ case _ => None
+ }
+ }
+
+
+ /* symbols */
+
+ object Symbols_Request extends Request0("PIDE/symbols_request") {
+ def reply(id: Id, symbols: Symbol.Symbols): JSON.T = {
+ def json(symbol: Symbol.Entry): JSON.T =
+ JSON.Object(
+ "symbol" -> symbol.symbol,
+ "name" -> symbol.name,
+ "argument" -> symbol.argument.toString) ++
+ JSON.optional("code", symbol.code) ++
+ JSON.optional("font", symbol.font) ++
+ JSON.Object(
+ "groups" -> symbol.groups,
+ "abbrevs" -> symbol.abbrevs)
+
+ ResponseMessage(id, Some(symbols.entries.map(s => json(s))))
+ }
+ }
+
+ object Symbols_Convert_Request {
+ def unapply(json: JSON.T): Option[(Id, String, Boolean)] =
+ json match {
+ case RequestMessage(id, "PIDE/symbols_convert_request", Some(params)) =>
+ for {
+ s <- JSON.string(params, "text")
+ unicode <- JSON.bool(params, "unicode")
+ } yield (id, s, unicode)
+ case _ => None
+ }
+
+ def reply(id: Id, new_string: String): JSON.T =
+ ResponseMessage(id, Some(JSON.Object("text" -> new_string)))
+ }
+
/* preview */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala Thu Oct 03 13:01:31 2024 +0200
@@ -0,0 +1,91 @@
+/* Title: Tools/VSCode/src/pretty_text_panel.scala
+ Author: Thomas Lindae, TU Muenchen
+
+Pretty-printed text or HTML with decorations.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+object Pretty_Text_Panel {
+ def apply(
+ resources: VSCode_Resources,
+ channel: Channel,
+ output: (String, Option[LSP.Decoration]) => JSON.T
+ ): Pretty_Text_Panel = new Pretty_Text_Panel(resources, channel, output)
+}
+
+class Pretty_Text_Panel private(
+ resources: VSCode_Resources,
+ channel: Channel,
+ output: (String, Option[LSP.Decoration]) => JSON.T
+) {
+ private var current_body: XML.Body = Nil
+ private var current_formatted: XML.Body = Nil
+ private var margin: Double = resources.message_margin
+
+ private val delay_margin = Delay.last(resources.output_delay, channel.Error_Logger) {
+ refresh(current_body)
+ }
+
+ def update_margin(new_margin: Double): Unit = {
+ margin = new_margin
+ delay_margin.invoke()
+ }
+
+ def refresh(body: XML.Body): Unit = {
+ val formatted = Pretty.formatted(Pretty.separate(body), margin = margin, metric = Symbol.Metric)
+
+ if (formatted == current_formatted) return
+
+ current_body = body
+ current_formatted = formatted
+
+ if (resources.html_output) {
+ val node_context =
+ new Browser_Info.Node_Context {
+ override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
+ for {
+ thy_file <- Position.Def_File.unapply(props)
+ def_line <- Position.Def_Line.unapply(props)
+ source <- resources.source_file(thy_file)
+ uri = File.uri(Path.explode(source).absolute_file)
+ } yield HTML.link(uri.toString + "#" + def_line, body)
+ }
+ val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
+ val html = node_context.make_html(elements, formatted)
+ val message = output(HTML.source(html).toString, None)
+ channel.write(message)
+ } else {
+ def convert_symbols(body: XML.Body): XML.Body = {
+ body.map {
+ case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body))
+ case XML.Text(content) => XML.Text(resources.output_text(content))
+ }
+ }
+
+ val converted = convert_symbols(formatted)
+
+ val tree = Markup_Tree.from_XML(converted)
+ val text = XML.content(converted)
+
+ val document = Line.Document(text)
+ val decorations = tree
+ .cumulate(Text.Range.full, None: Option[String], Rendering.text_color_elements, (_, m) => {
+ Some(Some(m.info.name))
+ })
+ .flatMap(e => e.info match {
+ case None => None
+ case Some(i) => Some((document.range(e._1), "text_" ++ Rendering.text_color(i).toString))
+ })
+ .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList
+
+ val message = output(text, Some(LSP.Decoration(decorations)))
+ channel.write(message)
+ }
+ }
+}
+
--- a/src/Tools/VSCode/src/state_panel.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Thu Oct 03 13:01:31 2024 +0200
@@ -14,10 +14,11 @@
private val make_id = Counter.make()
private val instances = Synchronized(Map.empty[Counter.ID, State_Panel])
- def init(server: Language_Server): Unit = {
+ def init(id: LSP.Id, server: Language_Server): Unit = {
val instance = new State_Panel(server)
instances.change(_ + (instance.id -> instance))
instance.init()
+ instance.init_response(id)
}
def exit(id: Counter.ID): Unit = {
@@ -39,6 +40,11 @@
def auto_update(id: Counter.ID, enabled: Boolean): Unit =
instances.value.get(id).foreach(state =>
state.server.editor.send_dispatcher(state.auto_update(Some(enabled))))
+
+ def set_margin(id: Counter.ID, margin: Double): Unit =
+ instances.value.get(id).foreach(state => {
+ state.pretty_panel.value.update_margin(margin)
+ })
}
@@ -47,31 +53,26 @@
val id: Counter.ID = State_Panel.make_id()
- private def output(content: String): Unit =
- server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value))
+ private def init_response(id: LSP.Id): Unit =
+ server.channel.write(LSP.State_Init.reply(id, this.id))
/* query operation */
private val output_active = Synchronized(true)
+ private val pretty_panel =
+ Synchronized(Pretty_Text_Panel(
+ server.resources,
+ server.channel,
+ (content, decorations) =>
+ LSP.State_Output(id, content, auto_update_enabled.value, decorations)
+ ))
private val print_state =
new Query_Operation(server.editor, (), "print_state", _ => (),
(_, _, body) =>
- if (output_active.value && body.nonEmpty){
- val node_context =
- new Browser_Info.Node_Context {
- override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
- for {
- thy_file <- Position.Def_File.unapply(props)
- def_line <- Position.Def_Line.unapply(props)
- source <- server.resources.source_file(thy_file)
- uri = File.uri(Path.explode(source).absolute_file)
- } yield HTML.link(uri.toString + "#" + def_line, body)
- }
- val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
- val html = node_context.make_html(elements, Pretty.separate(body))
- output(HTML.source(html).toString)
+ if (output_active.value && body.nonEmpty) {
+ pretty_panel.value.refresh(body)
})
def locate(): Unit = print_state.locate_query()
@@ -103,7 +104,6 @@
}
-
/* main */
private val main =
--- a/src/Tools/VSCode/src/vscode_main.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_main.scala Thu Oct 03 13:01:31 2024 +0200
@@ -32,7 +32,7 @@
verbose: Boolean = false,
background: Boolean = false,
progress: Progress = new Progress
-): Process_Result = {
+ ): Process_Result = {
def platform_path(s: String): String = File.platform_path(Path.explode(s))
val args_json =
@@ -146,8 +146,11 @@
"editor.fontSize": 18,
"editor.lineNumbers": "off",
"editor.renderIndentGuides": false,
+ "editor.renderWhitespace": "none",
"editor.rulers": [80, 100],
+ "editor.quickSuggestions": { "strings": "on" },
"editor.unicodeHighlight.ambiguousCharacters": false,
+ "editor.wordBasedSuggestions": false,
"extensions.autoCheckUpdates": false,
"extensions.autoUpdate": false,
"terminal.integrated.fontFamily": "monospace",
--- a/src/Tools/VSCode/src/vscode_model.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_model.scala Thu Oct 03 13:01:31 2024 +0200
@@ -29,7 +29,7 @@
sealed case class Content(node_name: Document.Node.Name, doc: Line.Document) {
override def toString: String = doc.toString
def text_length: Text.Offset = doc.text_length
- def text_range: Text.Range = doc.text_range
+ def text_range: Text.Range = doc.full_range
def text: String = doc.text
lazy val bytes: Bytes = Bytes(Symbol.encode(text))
@@ -176,25 +176,14 @@
}
def flush_edits(
- unicode_symbols: Boolean,
doc_blobs: Document.Blobs,
file: JFile,
caret: Option[Line.Position]
- ): Option[((List[LSP.TextDocumentEdit], List[Document.Edit_Text]), VSCode_Model)] = {
- val workspace_edits =
- if (unicode_symbols && version.isDefined) {
- val edits = content.recode_symbols
- if (edits.nonEmpty) List(LSP.TextDocumentEdit(file, version.get, edits))
- else Nil
- }
- else Nil
-
+ ): Option[(List[Document.Edit_Text], VSCode_Model)] = {
val (reparse, perspective) = node_perspective(doc_blobs, caret)
- if (reparse || pending_edits.nonEmpty || last_perspective != perspective ||
- workspace_edits.nonEmpty) {
+ if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
val prover_edits = node_edits(node_header, pending_edits, perspective)
- val edits = (workspace_edits, prover_edits)
- Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
+ Some(prover_edits, copy(pending_edits = Nil, last_perspective = perspective))
}
else None
}
@@ -205,11 +194,8 @@
def publish(
rendering: VSCode_Rendering
): (Option[List[Text.Info[Command.Results]]], Option[List[VSCode_Model.Decoration]], VSCode_Model) = {
- val diagnostics = rendering.diagnostics
- val decorations =
- if (node_visible) rendering.decorations
- else { for (deco <- published_decorations) yield VSCode_Model.Decoration.empty(deco.typ) }
-
+ val (diagnostics, decorations, model) = publish_full(rendering)
+
val changed_diagnostics =
if (diagnostics == published_diagnostics) None else Some(diagnostics)
val changed_decorations =
@@ -217,7 +203,18 @@
else if (published_decorations.isEmpty) Some(decorations)
else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a)
- (changed_diagnostics, changed_decorations,
+ (changed_diagnostics, changed_decorations, model)
+ }
+
+ def publish_full(
+ rendering: VSCode_Rendering
+ ): (List[Text.Info[Command.Results]],List[VSCode_Model.Decoration], VSCode_Model) = {
+ val diagnostics = rendering.diagnostics
+ val decorations =
+ if (node_visible) rendering.decorations
+ else { for (deco <- published_decorations) yield VSCode_Model.Decoration.empty(deco.typ) }
+
+ (diagnostics, decorations,
copy(published_diagnostics = diagnostics, published_decorations = decorations))
}
--- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Thu Oct 03 13:01:31 2024 +0200
@@ -79,8 +79,8 @@
def completion(node_pos: Line.Node_Position, caret: Text.Offset): List[LSP.CompletionItem] = {
val doc = model.content.doc
- val line = node_pos.pos.line
- val unicode = File.is_thy(node_pos.name)
+ val line = node_pos.line
+ val unicode = resources.unicode_symbols_edits
doc.offset(Line.Position(line)) match {
case None => Nil
case Some(line_start) =>
@@ -109,11 +109,25 @@
results match {
case None => Nil
case Some(result) =>
- result.items.map(item =>
+ val commit_characters = (' ' to '~').toList.map(_.toString)
+
+ result.items.map(item => {
+ val kind = item.description match {
+ case _ :: "(keyword)" :: _ => LSP.CompletionItemKind.Keyword
+ case _ => LSP.CompletionItemKind.Text
+ }
+
LSP.CompletionItem(
- label = item.description.mkString(" "),
+ label = item.replacement,
+ kind = Some(kind),
+ detail = Some(item.description.mkString(" ")),
+ filter_text = Some(item.original),
+ commit_characters =
+ if (result.unique && item.immediate) Some(commit_characters) else None,
text = Some(item.replacement),
- range = Some(doc.range(item.range))))
+ range = Some(doc.range(item.range)),
+ )
+ })
}
items ::: VSCode_Spell_Checker.menu_items(rendering, caret)
}
@@ -153,9 +167,7 @@
def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = {
snapshot.select(range, Rendering.text_color_elements, _ =>
{
- case Text.Info(_, XML.Elem(Markup(name, props), _)) =>
- if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None
- else Rendering.text_color.get(name)
+ case Text.Info(_, elem) => Rendering.text_color.get(elem.name)
})
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Wed Oct 02 23:47:07 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Thu Oct 03 13:01:31 2024 +0200
@@ -80,9 +80,13 @@
/* options */
def pide_extensions: Boolean = options.bool("vscode_pide_extensions")
- def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols")
+ def html_output: Boolean = options.bool("vscode_html_output")
def tooltip_margin: Int = options.int("vscode_tooltip_margin")
def message_margin: Int = options.int("vscode_message_margin")
+ def output_delay: Time = options.seconds("vscode_output_delay")
+
+ def unicode_symbols_output: Boolean = options.bool("vscode_unicode_symbols_output")
+ def unicode_symbols_edits: Boolean = options.bool("vscode_unicode_symbols_edits")
/* document node name */
@@ -272,13 +276,10 @@
file <- st.pending_input.iterator
model <- st.models.get(file)
(edits, model1) <-
- model.flush_edits(false, st.document_blobs, file, st.get_caret(file))
+ model.flush_edits(st.document_blobs, file, st.get_caret(file))
} yield (edits, (file, model1))).toList
- for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
- channel.write(LSP.WorkspaceEdit(workspace_edits))
-
- session.update(st.document_blobs, changed_models.flatMap(res => res._1._2))
+ session.update(st.document_blobs, changed_models.flatMap(_._1))
st.copy(
models = st.models ++ changed_models.iterator.map(_._2),
@@ -330,13 +331,12 @@
/* output text */
- def output_text(text: String): String =
- Symbol.output(unicode_symbols, text)
+ def output_text(content: String): String = Symbol.output(unicode_symbols_output, content)
+ def output_edit(content: String): String = Symbol.output(unicode_symbols_edits, content)
- def output_xml(xml: XML.Tree): String =
- output_text(XML.content(xml))
+ def output_xml_text(body: XML.Tree): String = output_text(XML.content(body))
- def output_pretty(body: XML.Body, margin: Int): String =
+ def output_pretty(body: XML.Body, margin: Double): String =
output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric))
def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
@@ -358,6 +358,18 @@
}
+ /* decoration requests */
+
+ def force_decorations(channel: Channel, file: JFile): Unit = {
+ val model = state.value.models(file)
+ val rendering1 = rendering(model)
+ val (_, decos, model1) = model.publish_full(rendering1)
+ if (pide_extensions) {
+ channel.write(rendering1.decoration_output(decos).json(file))
+ }
+ }
+
+
/* spell checker */
val spell_checker = new Spell_Checker_Variable