--- a/src/Tools/VSCode/extension/src/extension.ts Fri Jun 09 16:59:14 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Fri Jun 09 17:13:50 2017 +0200
@@ -6,6 +6,7 @@
import * as decorations from './decorations';
import * as preview from './preview';
import * as protocol from './protocol';
+import * as symbol from './symbol';
import { ExtensionContext, workspace, window, commands } from 'vscode';
import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
from 'vscode-languageclient';
@@ -110,6 +111,16 @@
language_client.onReady().then(() => preview.init(context, language_client))
+ /* Isabelle symbols */
+
+ language_client.onReady().then(() =>
+ {
+ language_client.onNotification(protocol.symbols_type,
+ params => symbol.update(params.entries))
+ language_client.sendNotification(protocol.symbols_request_type)
+ })
+
+
/* start server */
context.subscriptions.push(language_client.start())
--- a/src/Tools/VSCode/extension/src/protocol.ts Fri Jun 09 16:59:14 2017 +0200
+++ b/src/Tools/VSCode/extension/src/protocol.ts Fri Jun 09 17:13:50 2017 +0200
@@ -2,6 +2,7 @@
import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions } from 'vscode'
import { NotificationType } from 'vscode-languageclient';
+import * as symbol from './symbol'
/* decorations */
@@ -67,3 +68,17 @@
export const preview_response_type =
new NotificationType<Preview_Response, void>("PIDE/preview_response")
+
+
+/* Isabelle symbols */
+
+export interface Symbols
+{
+ entries: [symbol.Entry]
+}
+
+export const symbols_type =
+ new NotificationType<Symbols, void>("PIDE/symbols")
+
+export const symbols_request_type =
+ new NotificationType<void, void>("PIDE/symbols_request")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/symbol.ts Fri Jun 09 17:13:50 2017 +0200
@@ -0,0 +1,41 @@
+'use strict';
+
+export type Symbol = string
+
+export interface Entry
+{
+ symbol: Symbol,
+ name: string,
+ code: number
+}
+
+let symbol_entries: [Entry]
+const names = new Map<Symbol, string>()
+const codes = new Map<Symbol, number>()
+
+export function get_name(sym: Symbol): string | undefined
+{
+ return names.get(sym)
+}
+
+export function get_code(sym: Symbol): number | undefined
+{
+ return codes.get(sym)
+}
+
+export function get_unicode(sym: Symbol): string
+{
+ const code = get_code(sym)
+ return code ? String.fromCharCode(code) : ""
+}
+
+export function update(entries: [Entry])
+{
+ symbol_entries = entries
+ names.clear
+ codes.clear
+ for (const entry of entries) {
+ names.set(entry.symbol, entry.name)
+ codes.set(entry.symbol, entry.code)
+ }
+}
\ No newline at end of file
--- a/src/Tools/VSCode/src/protocol.scala Fri Jun 09 16:59:14 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala Fri Jun 09 17:13:50 2017 +0200
@@ -491,4 +491,20 @@
"label" -> label,
"content" -> content))
}
+
+
+ /* Isabelle symbols */
+
+ object Symbols_Request extends Notification0("PIDE/symbols_request")
+
+ object Symbols
+ {
+ def apply(): JSON.T =
+ {
+ val entries =
+ for ((sym, code) <- Symbol.codes)
+ yield Map("symbol" -> sym, "name" -> Symbol.names(sym), "code" -> code)
+ Notification("PIDE/symbols", Map("entries" -> entries))
+ }
+ }
}
--- a/src/Tools/VSCode/src/server.scala Fri Jun 09 16:59:14 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala Fri Jun 09 17:13:50 2017 +0200
@@ -398,6 +398,7 @@
case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
case Protocol.Caret_Update(caret) => update_caret(caret)
case Protocol.Preview_Request(file, column) => request_preview(file, column)
+ case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
case _ => log("### IGNORED")
}
}