# 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 `\` 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 `\` 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("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)