# HG changeset patch
# User wenzelm
# Date 1497021230 -7200
# Node ID 39eb61b1fa51bee4b2b9614125091511f8ee7111
# Parent  70d3d0818d42bf053aeefb1b552e7c11f79f2445
provide information about Isabelle symbols within VSCode;

diff -r 70d3d0818d42 -r 39eb61b1fa51 src/Tools/VSCode/extension/src/extension.ts
--- 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())
diff -r 70d3d0818d42 -r 39eb61b1fa51 src/Tools/VSCode/extension/src/protocol.ts
--- 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")
diff -r 70d3d0818d42 -r 39eb61b1fa51 src/Tools/VSCode/extension/src/symbol.ts
--- /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
diff -r 70d3d0818d42 -r 39eb61b1fa51 src/Tools/VSCode/src/protocol.scala
--- 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))
+    }
+  }
 }
diff -r 70d3d0818d42 -r 39eb61b1fa51 src/Tools/VSCode/src/server.scala
--- 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")
         }
       }