src/Tools/VSCode/extension/src/symbol.ts

dynamic configuration of prettify-symbols-mode, similar to VSCoq;

'use strict';

import * as library from './library'
import { Disposable, DocumentSelector, ExtensionContext, extensions } from 'vscode';


export type Symbol = string


/* ASCII characters */

export function is_char(s: string): boolean
{ return s.length == 1 }

export function is_ascii_letter(s: string): boolean
{ return is_char(s) && "A" <= s && s <= "Z" || "a" <= s && s <= "z" }

export function is_ascii_digit(s: string): boolean
{ return is_char(s) && "0" <= s && s <= "9" }

export function is_ascii_quasi(s: string): boolean
{ return s == "_" || s == "'" }

export function is_ascii_letdig(s: string): boolean
{ return is_ascii_letter(s) || is_ascii_digit(s) || is_ascii_quasi(s) }

export function is_ascii_identifier(s: String): 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
}


/* named symbols */

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) : ""
}

function update_entries(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)
  }
}


/* completion */

export function complete_name(prefix: string): [string]
{
  let result = [] as [string]
  for (const entry of names) {
    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
            }))
      }
    })
  }
}