# HG changeset patch
# User wenzelm
# Date 1497274840 -7200
# Node ID 65a68dcd95c3752427564a3d2df5faa787a2e017
# Parent  0a34bfc15e2c668c6278a22287fda1e8bf4f8c88
dynamic configuration of prettify-symbols-mode, similar to VSCoq;

diff -r 0a34bfc15e2c -r 65a68dcd95c3 src/Tools/VSCode/extension/README.md
--- a/src/Tools/VSCode/extension/README.md	Mon Jun 12 15:20:07 2017 +0200
+++ b/src/Tools/VSCode/extension/README.md	Mon Jun 12 15:40:40 2017 +0200
@@ -19,9 +19,5 @@
 
 ## Isabelle symbols ##
 
-Isabelle symbols like `\<forall>` may be rendered using the extension Prettify
-Symbols Mode. It needs to be configured manually as follows:
-
-$ISABELLE_HOME/src/Tools/VSCode/extension/isabelle-symbols.json contains a
-configuration (generated via `isabelle build_vscode`). Its content needs to
-be copied carefully into the regular VSCode User Preferences.
+Isabelle symbols like `\<forall>` are rendered using the extension "Prettify
+Symbols Mode", which needs to be installed separately.
diff -r 0a34bfc15e2c -r 65a68dcd95c3 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Mon Jun 12 15:20:07 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Mon Jun 12 15:40:40 2017 +0200
@@ -117,7 +117,7 @@
     language_client.onReady().then(() =>
     {
       language_client.onNotification(protocol.symbols_type,
-        params => symbol.update(params.entries))
+        params => symbol.init(context, params.entries))
       language_client.sendNotification(protocol.symbols_request_type)
     })
 
diff -r 0a34bfc15e2c -r 65a68dcd95c3 src/Tools/VSCode/extension/src/library.ts
--- a/src/Tools/VSCode/extension/src/library.ts	Mon Jun 12 15:20:07 2017 +0200
+++ b/src/Tools/VSCode/extension/src/library.ts	Mon Jun 12 15:40:40 2017 +0200
@@ -4,6 +4,14 @@
 import { TextEditor, Uri, workspace } from 'vscode'
 
 
+/* regular expressions */
+
+export function escape_regex(s: string): string
+{
+  return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&")
+}
+
+
 /* platform information */
 
 export function platform_is_windows(): boolean
diff -r 0a34bfc15e2c -r 65a68dcd95c3 src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Mon Jun 12 15:20:07 2017 +0200
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Mon Jun 12 15:40:40 2017 +0200
@@ -1,5 +1,9 @@
 'use strict';
 
+import * as library from './library'
+import { Disposable, DocumentSelector, ExtensionContext, extensions } from 'vscode';
+
+
 export type Symbol = string
 
 
@@ -60,7 +64,7 @@
   return code ? String.fromCharCode(code) : ""
 }
 
-export function update(entries: [Entry])
+function update_entries(entries: [Entry])
 {
   symbol_entries = entries
   names.clear
@@ -81,4 +85,77 @@
     if (entry[1].startsWith(prefix)) { result.push(entry[0]) }
   }
   return result.sort()
+}
+
+
+/* prettify symbols mode */
+
+interface PrettyStyleProperties
+{
+  border?: string
+  textDecoration?: string
+  color?: string
+  backgroundColor?: string
+}
+
+interface PrettyStyle extends PrettyStyleProperties
+{
+  dark?: PrettyStyleProperties
+  light?: PrettyStyleProperties
+}
+
+interface Substitution
+{
+  ugly: string
+  pretty: string
+  pre?: string
+  post?: string
+  style?: PrettyStyle
+}
+
+interface LanguageEntry
+{
+  language: DocumentSelector
+  revealOn: string
+  adjustCursorMovement: boolean
+  substitutions: Substitution[]
+}
+
+interface PrettifySymbolsMode
+{
+  onDidEnabledChange: (handler: (enabled: boolean) => void) => Disposable
+  isEnabled: () => boolean,
+  registerSubstitutions: (substitutions: LanguageEntry) => Disposable
+}
+
+export function init(context: ExtensionContext, entries: [Entry])
+{
+  update_entries(entries)
+
+  const prettify_symbols_mode =
+    extensions.getExtension<PrettifySymbolsMode>("siegebell.prettify-symbols-mode")
+  if (prettify_symbols_mode) {
+    prettify_symbols_mode.activate().then(() =>
+    {
+      const substitutions = [] as [Substitution]
+      for (const entry of names) {
+        const sym = entry[0]
+        substitutions.push(
+          {
+            ugly: library.escape_regex(sym),
+            pretty: library.escape_regex(get_unicode(sym))
+          })
+      }
+      for (const language of ["isabelle", "isabelle-ml", "isabelle-output"]) {
+        context.subscriptions.push(
+          prettify_symbols_mode.exports.registerSubstitutions(
+            {
+              language: language,
+              revealOn: "none",
+              adjustCursorMovement: true,
+              substitutions: substitutions
+            }))
+      }
+    })
+  }
 }
\ No newline at end of file
diff -r 0a34bfc15e2c -r 65a68dcd95c3 src/Tools/VSCode/src/build_vscode.scala
--- a/src/Tools/VSCode/src/build_vscode.scala	Mon Jun 12 15:20:07 2017 +0200
+++ b/src/Tools/VSCode/src/build_vscode.scala	Mon Jun 12 15:40:40 2017 +0200
@@ -15,35 +15,6 @@
   val extension_dir = Path.explode("~~/src/Tools/VSCode/extension")
 
 
-  /* Prettify Symbols Mode */
-
-  def prettify_config: String =
-    """{
-  "prettifySymbolsMode.substitutions": [
-      {
-        "language": "isabelle",
-        "revealOn": "none",
-        "adjustCursorMovement": true,
-        "substitutions": [""" +
-          (for ((s, c) <- Symbol.codes)
-           yield
-            JSON.Format(
-              Map("ugly" -> Library.escape_regex(s),
-                "pretty" -> Library.escape_regex(Codepoint.string(c)))))
-            .mkString("\n          ", ",\n          ", "") +
-        """]
-      }
-    ]
-}"""
-
-  def build_symbols(progress: Progress = No_Progress)
-  {
-    val output_path = extension_dir + Path.explode("isabelle-symbols.json")
-    progress.echo(output_path.implode)
-    File.write_backup(output_path, prettify_config)
-  }
-
-
   /* grammar */
 
   def build_grammar(options: Options, progress: Progress = No_Progress)
@@ -97,7 +68,6 @@
       val options = Options.init()
       val progress = new Console_Progress()
 
-      build_symbols(progress)
       build_grammar(options, progress)
       build_extension(progress, publish = publish)
     }, admin = true)