From 40fbb28f1faf5754b56ce3cbe1c24182caab4928 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 1 Jun 2024 19:11:07 +0200 Subject: [PATCH] setup vscode-lean4 as submodule --- .gitmodules | 6 +- client/monaco-lean4 | 1 + client/src/Editor.tsx | 19 +- client/src/Untitled-1.md | 66 ++ client/src/config/editor.json | 23 + client/src/{editor => css}/infoview.css | 0 client/src/{editor => css}/vscode.css | 0 .../abbreviation/AbbreviationHoverProvider.ts | 49 -- .../abbreviation/AbbreviationProvider.ts | 108 ---- .../rewriter/AbbreviationRewriter.ts | 278 --------- .../rewriter/TrackedAbbreviation.ts | 111 ---- client/src/editor/codicon.ttf | Bin 69776 -> 0 bytes client/src/editor/config.ts | 5 - client/src/editor/infoview.ts | 580 ------------------ client/src/editor/leanclient.ts | 343 ----------- client/src/editor/taskgutter.ts | 119 ---- client/src/editor/utils/converters.ts | 76 --- client/src/monacoSetup.ts | 2 +- client/vscode-lean4 | 1 - 19 files changed, 104 insertions(+), 1683 deletions(-) create mode 160000 client/monaco-lean4 create mode 100644 client/src/Untitled-1.md create mode 100644 client/src/config/editor.json rename client/src/{editor => css}/infoview.css (100%) rename client/src/{editor => css}/vscode.css (100%) delete mode 100644 client/src/editor/abbreviation/AbbreviationHoverProvider.ts delete mode 100644 client/src/editor/abbreviation/AbbreviationProvider.ts delete mode 100644 client/src/editor/abbreviation/rewriter/AbbreviationRewriter.ts delete mode 100644 client/src/editor/abbreviation/rewriter/TrackedAbbreviation.ts delete mode 100644 client/src/editor/codicon.ttf delete mode 100644 client/src/editor/config.ts delete mode 100644 client/src/editor/infoview.ts delete mode 100644 client/src/editor/leanclient.ts delete mode 100644 client/src/editor/taskgutter.ts delete mode 100644 client/src/editor/utils/converters.ts delete mode 160000 client/vscode-lean4 diff --git a/.gitmodules b/.gitmodules index 1f2b97bc..c9f7a251 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,6 @@ [submodule "Projects/lean4web-tools"] path = Projects/lean4web-tools url = https://github.com/hhu-adam/lean4web-tools.git -[submodule "client/vscode-lean4"] - path = client/vscode-lean4 - url = https://github.com/leanprover/vscode-lean4.git +[submodule "client/monaco-lean4"] + path = client/monaco-lean4 + url = git@github.com:hhu-adam/monaco-lean4.git diff --git a/client/monaco-lean4 b/client/monaco-lean4 new file mode 160000 index 00000000..f0187e26 --- /dev/null +++ b/client/monaco-lean4 @@ -0,0 +1 @@ +Subproject commit f0187e2641dd08eb668c9bfff1be996eb7bfd9a4 diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx index feef1ade..b805c01d 100644 --- a/client/src/Editor.tsx +++ b/client/src/Editor.tsx @@ -3,11 +3,11 @@ import { useEffect, useRef, useState } from 'react' import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { loadRenderInfoview } from '@leanprover/infoview/loader' import { InfoviewApi } from '@leanprover/infoview-api' -import { InfoProvider } from './editor/infoview' -import { LeanClient } from './editor/leanclient' -import { AbbreviationRewriter } from './editor/abbreviation/rewriter/AbbreviationRewriter' -import { AbbreviationProvider } from './editor/abbreviation/AbbreviationProvider' -import { LeanTaskGutter } from './editor/taskgutter' +import { InfoProvider } from '../monaco-lean4/vscode-lean4/src/infoview' +import { LeanClient } from '../monaco-lean4/vscode-lean4/src/leanclient' +import { AbbreviationRewriter } from '../monaco-lean4/vscode-lean4/src/abbreviation/rewriter/AbbreviationRewriter' +import { AbbreviationProvider } from '../monaco-lean4/vscode-lean4/src/abbreviation/AbbreviationProvider' +import { LeanTaskGutter } from '../monaco-lean4/vscode-lean4/src/taskgutter' import Split from 'react-split' import Notification from './Notification' import settings from './config/settings' @@ -17,9 +17,10 @@ import { DisposingWebSocketMessageReader } from './reader' import { monacoSetup } from './monacoSetup' import './css/Editor.css' -import './editor/infoview.css' -import './editor/vscode.css' +import './css/infoview.css' +import './css/vscode.css' import { render } from '@testing-library/react' +import { AbbreviationConfig } from '../monaco-lean4/vscode-lean4/src/abbreviation/config' monacoSetup() @@ -96,7 +97,8 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: wrappingStrategy: "advanced", }) setEditor(editor) - const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor) + + const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(AbbreviationConfig), model, editor) return () => { editor.dispose(); model.dispose(); @@ -184,7 +186,6 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: setRestart((project?) => restart) }, [editor, infoviewApi, infoProvider]) - return (
+Date: Wed May 29 15:52:58 2024 +0200 + + add vscode-lean4 as submodule + +commit c06471c81129dbad2f8a7cbd2718b2f1b79127de (origin/dev) +Author: Jon Eugster +Date: Tue May 7 12:20:09 2024 +0200 + + many things + +commit 3cc8a85d28bf42ca3254f1458b725f77251d33d0 +Author: Jon Eugster +Date: Thu May 2 17:18:45 2024 +0200 + + temp. add entire vscode-lean4 extension + +commit 013dbada1fd2557ce5d25b8fd88f32aba1ce8e41 +Author: Jon Eugster +Date: Thu May 2 04:06:56 2024 +0200 + + cleanup App.tsx and config + + + + + + + + + + + + + +commit 5e2ea468ab9401eb0d5d16efbde21bbe9cc6521f +Author: Jon Eugster +Date: Thu May 2 02:32:02 2024 +0200 + + cleanup navigation. includes #12. + +commit 012f97aa23a1a516171c075b6f45ad7be789e2b0 +Author: Jon Eugster +Date: Tue Apr 30 17:29:49 2024 +0200 + + cleanup App.tsx, part 2 + +commit 30055c00891c2caff8a8446feee78766c1807063 +Author: Jon Eugster +Date: Tue Apr 30 17:17:35 2024 +0200 + + cleanup App.tsx, part 1 + +commit 182ba518ea89d046914b3242e97dc4cc9974944f +Author: Jon Eugster +Date: Tue Apr 30 17:17:04 2024 +0200 + + fix updated infoview + +commit 88d83ea6b1cd0885c9fcd19223d629ddf507af44 +Author: Jon Eugster +Date: Mon Apr 29 20:30:14 2024 +0200 + + temporarily use my own npm packages instead diff --git a/client/src/config/editor.json b/client/src/config/editor.json new file mode 100644 index 00000000..963c835b --- /dev/null +++ b/client/src/config/editor.json @@ -0,0 +1,23 @@ +{ + "glyphMargin": true, + "lineDecorationsWidth": 5, + "folding": false, + "lineNumbers": "on", + "lineNumbersMinChars": 1, + "rulers": [100], + "lightbulb": { + "enabled": true + }, + "unicodeHighlight": { + "ambiguousCharacters": false + }, + "automaticLayout": true, + "minimap": { + "enabled": false + }, + "tabSize": 2, + "semanticHighlighting.enabled": true, + "theme": "vs", + "fontFamily": "JuliaMono", + "wrappingStrategy": "advanced" +} diff --git a/client/src/editor/infoview.css b/client/src/css/infoview.css similarity index 100% rename from client/src/editor/infoview.css rename to client/src/css/infoview.css diff --git a/client/src/editor/vscode.css b/client/src/css/vscode.css similarity index 100% rename from client/src/editor/vscode.css rename to client/src/css/vscode.css diff --git a/client/src/editor/abbreviation/AbbreviationHoverProvider.ts b/client/src/editor/abbreviation/AbbreviationHoverProvider.ts deleted file mode 100644 index 81422481..00000000 --- a/client/src/editor/abbreviation/AbbreviationHoverProvider.ts +++ /dev/null @@ -1,49 +0,0 @@ -/* This file is based on `vscode-lean4/vscode-lean4/src/abbreviation/AbbreviationHoverProvider.ts` */ - -import { AbbreviationProvider } from './AbbreviationProvider'; -import settings from '../../config/settings'; -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' - -/** - * Adds hover behaviour for getting translations of unicode characters. - * Eg: "Type ⊓ using \glb or \sqcap" - */ -export class AbbreviationHoverProvider implements monaco.languages.HoverProvider { - constructor( - private readonly abbreviations: AbbreviationProvider - ) {} - - provideHover(model: monaco.editor.ITextModel, pos: monaco.Position): monaco.languages.Hover | undefined { - const context = model.getLineContent(pos.lineNumber).substring(pos.column-1); - const symbolsAtCursor = this.abbreviations.findSymbolsIn(context); - const allAbbrevs = symbolsAtCursor.map((symbol) => ({ - symbol, - abbrevs: this.abbreviations.getAllAbbreviations(symbol), - })); - - if ( - allAbbrevs.length === 0 || - allAbbrevs.every((a) => a.abbrevs.length === 0) - ) { - return undefined; - } - - const leader = settings.abbreviationCharacter; - - const hoverMarkdown = allAbbrevs - .map( - ({ symbol, abbrevs }) => - `Type ${symbol} using ${abbrevs - .map((a) => '`' + leader + a + '`') - .join(' or ')}` - ) - .join('\n\n'); - - const maxSymbolLength = Math.max( - ...allAbbrevs.map((a) => a.symbol.length) - ); - const hoverRange = new monaco.Range(pos.lineNumber, pos.column-1, pos.lineNumber, pos.column-1 + maxSymbolLength); - - return {contents: [{value: hoverMarkdown}], range: hoverRange}; - } -} diff --git a/client/src/editor/abbreviation/AbbreviationProvider.ts b/client/src/editor/abbreviation/AbbreviationProvider.ts deleted file mode 100644 index 7b656d1c..00000000 --- a/client/src/editor/abbreviation/AbbreviationProvider.ts +++ /dev/null @@ -1,108 +0,0 @@ -/* This file is based on `vscode-lean4/vscode-lean4/src/abbreviation/AbbreviationProvider.ts` */ - -import { computed } from 'mobx'; -// import { Disposable } from 'vscode'; -// import { autorunDisposable } from '../utils/autorunDisposable'; -import abbreviations from '../../../vscode-lean4/vscode-lean4/src/abbreviation/abbreviations.json'; -import settings from '../../config/settings'; - -export interface SymbolsByAbbreviation { - [abbrev: string]: string; -} - -/** - * Answers queries to a database of abbreviations. - */ -export class AbbreviationProvider { - // private readonly disposables = new Array(); - private cache: Record = {}; - - constructor() { - // this.disposables.push( - // autorunDisposable(() => { - // // For the livetime of this component, cache the computed's - // const _ = this.symbolsByAbbreviation; - // // clear cache on change - // this.cache = {}; - // }) - // ); - } - - private get symbolsByAbbreviation(): SymbolsByAbbreviation { - // There are only like 1000 symbols. Building an index is not required yet. - return { - ...abbreviations, - ...settings.inputModeCustomTranslations - }; - } - - getAllAbbreviations(symbol: string): string[] { - return Object.entries(this.symbolsByAbbreviation) - .filter(([abbr, sym]) => sym === symbol) - .map(([abbr]) => abbr); - } - - findSymbolsIn(symbolPlusUnknown: string): string[] { - const result = new Set(); - for (const [abbr, sym] of Object.entries(this.symbolsByAbbreviation)) { - if (symbolPlusUnknown.startsWith(sym)) { - result.add(sym); - } - } - return [...result.values()]; - } - - /** - * Computes the replacement text for a typed abbreviation (excl. leader). - * This converts the longest non-empty prefix with the best-matching abbreviation. - * - * For example: - * getReplacementText("alp") returns "α" - * getReplacementText("alp7") returns "α7" - * getReplacementText("") returns undefined - */ - getReplacementText(abbrev: string): string | undefined { - if (abbrev in this.cache) { - return this.cache[abbrev]; - } - const result = this._getReplacementText(abbrev); - this.cache[abbrev] = result; - return result; - } - - private _getReplacementText(abbrev: string): string | undefined { - if (abbrev.length === 0) { - return undefined; - } - - const matchingSymbol = this.findSymbolsByAbbreviationPrefix(abbrev)[0]; - if (matchingSymbol) { - return matchingSymbol; - } - - // Convert the `alp` in `\alp7` - const prefixReplacement = this.getReplacementText( - abbrev.slice(0, abbrev.length - 1) - ); - if (prefixReplacement) { - return prefixReplacement + abbrev.slice(abbrev.length - 1); - } - - return undefined; - } - - getSymbolForAbbreviation(abbrev: string): string | undefined { - return this.symbolsByAbbreviation[abbrev]; - } - - findSymbolsByAbbreviationPrefix(abbrevPrefix: string): string[] { - const matchingAbbreviations = Object.keys( - this.symbolsByAbbreviation - ).filter((abbrev) => abbrev.startsWith(abbrevPrefix)); - - matchingAbbreviations.sort((a, b) => a.length - b.length); - return matchingAbbreviations.map( - (abbr) => this.symbolsByAbbreviation[abbr] - ); - } -} diff --git a/client/src/editor/abbreviation/rewriter/AbbreviationRewriter.ts b/client/src/editor/abbreviation/rewriter/AbbreviationRewriter.ts deleted file mode 100644 index 28a36065..00000000 --- a/client/src/editor/abbreviation/rewriter/AbbreviationRewriter.ts +++ /dev/null @@ -1,278 +0,0 @@ -/* This file is based on `vscode-lean4/vscode-lean4/src/abbreviation/rewriter/AbbreviationRewriter.ts` */ - -// import { Range as LineColRange } from 'vscode'; -import { Disposable } from 'vscode'; -import { assert } from '../../../../vscode-lean4/vscode-lean4/src/utils/assert'; -import { AbbreviationProvider } from '../AbbreviationProvider'; -import { Range } from '../../../../vscode-lean4/vscode-lean4/src/abbreviation/rewriter/Range'; -import settings from '../../../config/settings'; -import { TrackedAbbreviation } from './TrackedAbbreviation'; -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import {IRange, Range as MonacoRange} from 'monaco-editor' -import { AbbreviationHoverProvider } from '../AbbreviationHoverProvider'; - -/** - * Tracks abbreviations in a given text editor and replaces them when dynamically. - */ -export class AbbreviationRewriter { - private readonly disposables = new Array(); - // /** - // * All tracked abbreviations are disjoint. - // */ - private readonly trackedAbbreviations = new Set(); - // private readonly decorationType = window.createTextEditorDecorationType({ - // textDecoration: 'underline', - // }); - - private dontTrackNewAbbr = false; - private decosIds: string[] = []; - // private isActiveContextKey: monaco.editor.IContextKey; - abbreviationHoverProvider: AbbreviationHoverProvider; - // private stderrOutput: OutputChannel; - // private firstOutput = true; - - constructor( - private readonly abbreviationProvider: AbbreviationProvider, - private readonly model: monaco.editor.ITextModel, - private readonly editor: monaco.editor.IStandaloneCodeEditor - ) { - this.disposables.push(model.onDidChangeContent((e: monaco.editor.IModelContentChangedEvent) => { - const changes = e.changes.slice(0); - // // We need to process the changes at the bottom first. - // // Otherwise, changes at the top will move spans at the bottom down. - changes.sort((c1, c2) => c2.rangeOffset - c1.rangeOffset); - - for (const c of changes) { - const range = new Range(c.rangeOffset, c.rangeLength); - this.processChange(range, c.text); - } - - this.updateState(); - - // // Replace any tracked abbreviation that is either finished or unique. - void this.forceReplace( - [...this.trackedAbbreviations].filter( - (abbr) => - abbr.finished || - (settings.eagerReplacementEnabled && - abbr.isAbbreviationUniqueAndComplete) - ) - ); - })) - - - this.disposables.push( - editor.onDidChangeCursorSelection((e: monaco.editor.ICursorSelectionChangedEvent) => { - // Replace any tracked abbreviation that lost selection. - void this.forceReplace( - [...this.trackedAbbreviations].filter( - (abbr) => - ![...e.secondarySelections, e.selection].some((s) => - abbr.range.containsRange( - fromVsCodeRange( - s, - this.model - ).withLength(0) - ) - ) - ) - ); - }) - ) - - // this.isActiveContextKey = this.editor.createContextKey('lean4.input.isActive', false); - - this.disposables.push( - monaco.editor.addEditorAction({ - id: 'lean4.input.convert', - label: 'Convert abbreviation', - precondition: "editorTextFocus && editorLangId == lean4 && lean4.input.isActive", - keybindings: [monaco.KeyCode.Tab], - run: async () => this.forceReplace([...this.trackedAbbreviations]) - }) - ) - - this.abbreviationHoverProvider = new AbbreviationHoverProvider(this.abbreviationProvider) - - this.disposables.push( - monaco.languages.registerHoverProvider('lean4', this.abbreviationHoverProvider) - ) - } - - private async forceReplace( - abbreviations: TrackedAbbreviation[] - ): Promise { - if (abbreviations.length === 0) { - return; - } - for (const a of abbreviations) { - this.trackedAbbreviations.delete(a); - } - - // Wait for VS Code to trigger `onDidChangeTextEditorSelection` - await waitForNextTick(); - - const cursorVar = '$CURSOR'; - const replacements = new Array<{ - range: Range; - newText: string; - transformOffsetInRange: (offset: number) => number; - }>(); - for (const abbr of abbreviations) { - const symbol = abbr.matchingSymbol; - if (symbol) { - const newText = symbol.replace(cursorVar, ''); - let cursorOffset = symbol.indexOf(cursorVar); - if (cursorOffset === -1) { - // position the cursor after the inserted symbol - cursorOffset = newText.length; - } - replacements.push({ - range: abbr.range, - newText, - transformOffsetInRange: (offset) => cursorOffset, - }); - } - } - // Process replacements with highest offset first - replacements.sort((a, b) => b.range.offset - a.range.offset); - - // We cannot rely on VS Code to update the selections - - // it becomes janky if symbols are inserted that are longer - // than their abbreviation. It also does not really work for \[[]]. - const newSelections = this.editor.getSelections() - .map((s) => ({range: fromVsCodeRange(s, this.model), dir: s.getDirection()})) - .map(({range: s, dir}) => { - // Apply the replacement of abbreviations to the selections. - let newSel = s; - for (const r of replacements) { - if ( - r.range.isBefore(newSel) && - !r.range.containsRange(newSel) - ) { - // don't do this on ` \abbr| ` - newSel = newSel.move(r.newText.length - r.range.length); - } else if ( - !r.range.isAfter(newSel) || - r.range.containsRange(newSel) - ) { - // do this on ` \abbr| ` or ` \ab|br ` - // newSel and r.range intersect - const offset = newSel.offset - r.range.offset; - const newOffset = r.transformOffsetInRange(offset); - newSel = newSel.move(newOffset - offset); - } - } - return {range: newSel, dir}; - }); - - // We don't want replaced symbols (e.g. "\") to trigger abbreviations. - this.dontTrackNewAbbr = true; - let ok = false; - try { - await this.editor.pushUndoStop() - await this.editor.executeEdits("abbreviation-rewriter", - replacements.map((r) => { - return { - range: toVsCodeRange(r.range, this.model), - text: r.newText - } - })); - - ok = true - } catch (e) { - throw Error('Error: while replacing abbreviation: ' + e); - } - this.dontTrackNewAbbr = false; - - if (ok) { - this.editor.setSelections(newSelections.map(({range: s, dir}) => { - const vr = toVsCodeRange(s, this.model); - return monaco.Selection.fromRange(vr, dir); - })); - - // this.abbreviationProvider.onAbbreviationsCompleted(this.textEditor); - } - else { - // Our edit did not succeed, do not update the selections. - // This can happen if `waitForNextTick` waits too long. - throw Error('Error: Unable to replace abbreviation'); - } - - this.updateState(); - } - - private updateState() { - this.decosIds = this.model.deltaDecorations(this.decosIds, - [...this.trackedAbbreviations].map((a: TrackedAbbreviation) => { - return { - range: toVsCodeRange(a.range, this.model), - options: { - inlineClassName: 'abbreviation' - } - }})) - - // void this.setInputActive(this.trackedAbbreviations.size > 0); - } - - // private async setInputActive(isActive: boolean) { - // this.isActiveContextKey.set(isActive); - // } - - private processChange( - range: Range, - text: string - ): { affectedAbbr: TrackedAbbreviation | undefined } { - let affectedAbbr: TrackedAbbreviation | undefined; - for (const abbr of [...this.trackedAbbreviations]) { - const { isAffected, shouldStopTracking } = abbr.processChange( - range, - text - ); - if (isAffected) { - // At most one abbreviation should be affected - assert(() => !affectedAbbr); - affectedAbbr = abbr; - } - if (shouldStopTracking) { - this.trackedAbbreviations.delete(abbr); - } - } - - if ( - text === settings.abbreviationCharacter && - !affectedAbbr && - !this.dontTrackNewAbbr - ) { - const abbr = new TrackedAbbreviation( - new Range(range.offset + 1, 0), - '', - this.abbreviationProvider - ); - this.trackedAbbreviations.add(abbr); - } - return { affectedAbbr }; - } - - dispose(): void { - for (const d of this.disposables) { - d.dispose(); - } - } -} - -function fromVsCodeRange(range: IRange, model: monaco.editor.ITextModel): Range { - const start = model.getOffsetAt(MonacoRange.getStartPosition(range)); - const end = model.getOffsetAt(MonacoRange.getEndPosition(range)); - return new Range(start, end - start); -} - -function toVsCodeRange(range: Range, model: monaco.editor.ITextModel): monaco.Range { - const start = model.getPositionAt(range.offset); - const end = model.getPositionAt(range.offsetEnd + 1); - return MonacoRange.fromPositions(start, end); -} - -function waitForNextTick(): Promise { - return new Promise((res) => setTimeout(res, 0)); -} diff --git a/client/src/editor/abbreviation/rewriter/TrackedAbbreviation.ts b/client/src/editor/abbreviation/rewriter/TrackedAbbreviation.ts deleted file mode 100644 index 540bd380..00000000 --- a/client/src/editor/abbreviation/rewriter/TrackedAbbreviation.ts +++ /dev/null @@ -1,111 +0,0 @@ -// import { AbbreviationProvider } from '../AbbreviationProvider'; -import { AbbreviationProvider } from '../AbbreviationProvider'; -import { Range } from '../../../../vscode-lean4/vscode-lean4/src/abbreviation/rewriter/Range'; -/* This file is based on `vscode-lean4/vscode-lean4/src/abbreviation/rewriter/TrackedAbbreviation.ts` */ - -/** - * Represents an abbreviation that is tracked and currently typed by the user. - * When the multi-cursor feature is used, multiple abbreviations can be tracked at once. - */ -export class TrackedAbbreviation { - private _abbreviationRange: Range; - - get abbreviationRange(): Range { - return this._abbreviationRange; - } - - get range(): Range { - return this.abbreviationRange.moveKeepEnd(-1); - } - - get abbreviation(): string { - return this._text; - } - - get matchingSymbol(): string | undefined { - return this.abbreviationProvider.getReplacementText(this.abbreviation); - } - - /** - * Does this abbreviation uniquely identify a symbol and is it complete? - */ - get isAbbreviationUniqueAndComplete(): boolean { - return ( - this.abbreviation !== "" && // Check empty string for speed up - this.abbreviationProvider.findSymbolsByAbbreviationPrefix( - this.abbreviation - ).length === 1 && - !!this.abbreviationProvider.getSymbolForAbbreviation( - this.abbreviation - ) - ); - } - - private _finished = false; - /** - * Indicates whether this abbreviation has been continued with non-abbreviation characters. - * Such abbreviations should be replaced immediately. - */ - get finished(): boolean { - return this._finished; - } - - constructor( - abbreviationRange: Range, - private _text: string, - private readonly abbreviationProvider: AbbreviationProvider - ) { - this._abbreviationRange = abbreviationRange; - } - - processChange( - range: Range, - newText: string - ): { shouldStopTracking: boolean; isAffected: boolean } { - if (this.abbreviationRange.containsRange(range)) { - this._finished = false; - - if (this.abbreviationRange.isBefore(range)) { - // `newText` is appended to `this.abbreviation` - if ( - this.abbreviationProvider.findSymbolsByAbbreviationPrefix( - this.abbreviation + newText - ).length === 0 - ) { - // newText is not helpful anymore. Finish this and don't accept the change. - this._finished = true; - return { - shouldStopTracking: false, - isAffected: false, - }; - } - } - - this._abbreviationRange = this.abbreviationRange.moveEnd( - newText.length - range.length - ); - const startStr = this.abbreviation.substr( - 0, - range.offset - this.abbreviationRange.offset - ); - const endStr = this.abbreviation.substr( - range.offsetEnd + 1 - this.abbreviationRange.offset - ); - this._text = startStr + newText + endStr; - - return { shouldStopTracking: false, isAffected: true }; - } else if (range.isBefore(this.range)) { - // The changed happened before us. We need to move. - this._abbreviationRange = this._abbreviationRange.move( - newText.length - range.length - ); - return { shouldStopTracking: false, isAffected: false }; - } else if (range.isAfter(this.range)) { - // The change does not affect us. - return { shouldStopTracking: false, isAffected: false }; - } else { - // We cannot process the change. Abort tracking. - return { shouldStopTracking: true, isAffected: false }; - } - } -} diff --git a/client/src/editor/codicon.ttf b/client/src/editor/codicon.ttf deleted file mode 100644 index 1095acb90f25c4eaf28ec2bef8c7d3cfedfd0265..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 69776 zcmeFa37lJ3c{hB{z0zHE7u_rAN*awcGa5;=k7v=7EdiQRo2?pmSrey_@a`mJ?1xFfA9eE7k6^}M!#~L z;Y?|tjqqXq5R2m5r`T8VIn+)cVm3RMp=ePVXMe?O_qE%uW=}M)X#FCrT^Bza{VASw z>gup&^!tC)f49N^o-y$3v;TXZ```Wj-|hbYwlVPk&A9+^Lh^~E3rSwcu*f5!jAin> zaF(Rr2vSH&oR7#a!gm*cxW4(C<^#R-Cg0C~$!FPj`6jlRzY5ZOhF96k*(i^&TiHk0 zH`xq-0lS`g{3v@3yN##VPg#?-_|5Et>`m-F{5rm!-N7&6Tlj9|JyFC#d55h{7O$U5R>L!>(lq*>&s& z_Cj_eyNTV*ZefSmB6|^gF?$KSo!!aqVlQL&uvf5q*%5Y>y^_6(y_&t2-OnCiuVW9g z*RzM%8`+!LZ?Pp@^A`42_BQq|_Aq-ddxRZh$JqzihuDYN@3TkQN7)~;kFh^uA7_8e zKEWPmf5E=O{*rwS5bm$pH`w2>zhi&T{s9%+&csI}U0`K9yypI?803YN-z&Rs) zluz(UKEhxj6Y5q~kio!`k1^Oy3M^Sk*y{9b;9znZ^>zn0&}@8_=vp86laQctqKV&}2l z>~f5#1MEV6FtQWzu;%E zXL*dB18h3W{*k?u{Vw|!`!TmzAA6ep8yjQeY!knX-^Fj^w*oW1gZJ|?`xo{C{s4cF zzm8wYui{tpYxuSNAV0t?b|(9u>^}ZVb_sh72=9|X$Mb9pI|JkW57^t;JK1)2F|V*U zu!~rny^sAK`*)UR8TPl#;V)x9WPi^7ggwDN$3DY8%RbM(!2XPVk$s7Mn*AwX0FNUq z`TzG6Luff2`Ria6;C6i6HPq*1Sy+qx^3d1U|`{cL)N{UM2`UmNlt-AaGmOyju|XE^FQ+h_#TuLJ)W{Yu+me zT$weG2m*g*O?n=Py$9(l1#xO)YA+DDH*3CH5TmkFnLzv!r1uHpTaex_i0?-FfFQmL z>FWjYd87{s;^!l!u>#`zkiJn6hd$e+GJzl=So6(-*zX|yEkV$?SaV4bAd;cYw+kZeulWu^kT|UQPC=wAHfj8UAca`-U4lrqHXjxQ$;6uP76ci^ zn$%t(NGsNSuOP@R)}*q6Ai-Gk5kZh;togfwNXu=$PY~oAYyO@fNIKR$CWti9=5axg zeysU^L6C#2`2j(Yh^+ZRL6D8C`5{4&lC1e*L6DcM`TK$(Iaw3BKM`aoYkou!q$z7Y zCJ1tsHUB^mBrI!wR1jn>YyP1iNL|+am>|es*8C$uki@L{aY2yDtog@+Ae~wB6M`V8 zS@Us0glU?~f*`wD^OJ%g#aZ)Hf*{XX^G^gpva{wBf*|8r^G^jq+Oy`T1wrn!=4S)} z0kGz01py1N=H~69f#xnokM>8ez@95(HernqLO zfPz?aMG){1Ykpf0kP&PCqaa`;*8Gkjpe5G)t{~th*8H9zASl-SCqckctoeOG>>i{) z5CrVRnoU7KTCCX;1kA;nKNJM?#hU*t2sn&2ebx1&w0MCMeCs|7p1Z2rtvLIkg z)`|!M+GMS$AmC2cQUn2kvX&|cSd_IiK|rOfr3(T+Wi3+>kSc4%1OcfZJKCA_xecwFU$M%d^&?AfS5I0#76Y zzGtmrK@4N1H6jSz&sw8`IE{rdL7c|IxFAkrVVxjO{XZdyP-$yY5U2j162z(hrv-89 z|EeHvAe|A!sh?|tIQ4T~5T|~g6~w8Z*9+p*&l?1B>gSDuIQ8=;L7e(|P7tTQ-7JXg z&aE>9aq7=4f;jc(ydX|}c%~pueYjN+r#{>!i1#2pOAx0%JX;W_KHM&dQy-oqh*O{J z5X7lZ8iF|W$xcC>`s7?eWX);q5=3_E)^0(Z+WUM#oZ9;WL7dwALP4C`dygPa?Rt?Q zviZ063gXn37YpLlmiq*8YRgLmacaLy1#xP>7YO3iHkS$F)HeGCacY|dL7dv=azUKh z;0i&U+Teg7PHk|dAWrqZN)SH}>D7Wb)$bZXoa%I~AWro-D2UT@t`o%RIoAu~l-?kS zQ~E+doYETwaY}Cz#3{X55WfX!oA@Cdw}~&}xJ~>;IBpYvF^=2BZ^!Yig7}?CUm}Pf zMtYkd{!*lL9f-di=^cXj-AL&k5Wfd0-2>wHBBgsk{0P#!1o2lReVHKs8l;pLh`$yo zf}mrw)~f_T+h#3#HVAq* zYtgeo(7;)Xo(+O7&RXY;w7XH3xb`2wcafV76;aPk03_p z-YbZ&L;5>{V2@y}M+C87ApKoI{0yY;6GUFB*6#^|-Ga4_31a6UJuZm+Y%QuA2v!Z& z`hXzVH(2X~f?(-jtq%!;&4aZ*EC|*Q*7|)x?8itS6$Fb2YkfozY$L4om>^h5SnCf2 z!Ct~z9~A`432XhKAlOh?>tll0CZvBPh*O__ToAtt=^qQ?G*><$h~J9zaY3-Zu-395 zMt$;0LA)R7rv$+|!&-kL2zDCQdO{F;0n$GeL_W{frv-5ucb^f&X*_;b5Wf=X=LGSq zkbYhezZ&Tm1o3N-{+S?tEz&Ov;s=p_Nf4|;to7%DU>{;F8aE(VidgF}1i@y+S|
DFD@nWqNL9l(X*0%-03dUMAE8y=u)eVtjT;c`aI8gh z00fI1YyGPr*ydR4CxT$5W38VGg1wHlh!=ohxnr%L34#rewSF!L);!jtc>-cI9%-I~ z$ij!$o55?p4;$+wtfZInn_=@@;_v65;!p9PO9|;(=?UqF@?QB7`Kyus$QhBRqHm5q zsVpdWDc@1|YPR-iUDMa;^ZI@IJM|CiPv~FOf2coW7{-9H$GF${o@tv~&Bx5|#3o}m z#$FZsmNjF&+g1ifoXyMlbM zE4VfIbnsMKNte?*($}V6lm0~ddl@aWE^}GtXy#klh3rGw_h-M|wXW;xuCM1Nb2sFc zyZgIu?0&5KC;5H(!}(+RPvpN|xU_Ib;mw6d3(xdy>^ao)u3oqIHN8*vxqS~6Q^oi9 zm-|0lnlIf`?km5uGE@0@<>v#&!0v%t2i`sK)SxnW_2B1+q@i^~w+(%LSQ*|ke8=$j zMmCPzF>-9==c6AUeQNBiu@8?+<6FmHG=AUsd&i#`|Ngqzy0LXT*WIx0-gR$Z_t?5G zO++Tnn0VvFS0{cxxo`5&e+g|epmgG*`e91Xa9cvz=qg{ts8FJ@U4w(T=A)b6x%so3zjMacGw#?TZMkC0r{}%-x%o%tpPc{YnHQXS z^O<*To!R=%txs%QzwO>_KRIjPS&y9cA7>ApeZ|?I*q+*cX!~2YFK>V99Cl9sIrp6N ziF1Crqi4sS9S`pKVI$wTwDG;2yLW!+T<_f1ocqMNzudKF*W1ri&g(yKe)qcFSMI)J z_q%p~|9tKI_2<9*0{en>7u;~c`!6_g!7ne&U3kHT-`|tlvwhEl7oBy{p^JXJcVzF< z-cRlQ#l<&Y{Qir7v~S(M8}~i7@0m;XUUK-7&t7`jr60ZQqYF1IEG>NE@~xL&clnzy z|KR1%T(SF#9~~GtP(QH!z`g_59r&{=wJWz@`Nk{1an<&#UUbzHSD$tDx3BT8x%!%= zYrcBzz_mAA`>|`kesJBv-3K2$_=)Qh*G*pc^Xsp@LA&9e8$SEO&?`mWHK61;q|h{3 zGfLBAywB#zM5@43lbhjaQ2Q#ixyaOHo(HKwsg$SZq{+OLu(_&K#(1!96P!wwa%HB5 zzsk&*)Mrb{gt%D6MaeNkJ(*DW$iTJ>whiPmR{65Boz5){_Ho&;-K61kCly)h z+ZWL+FBP{n&DQ;dX1_WTkLhMKqDBqQ%|y04>zj(EMWTiti$}dgapU%lMSp2<+rYrK z!QPEYBbzmn8?Q{OM%*@{X42O5^!<9mvvke&l5snNd+ir+Zl`rMDo0e!P1xClVI;D) z;oDjy5>fTE!@YIc{*A@r#{TR&;v*7$z(4uyxCF6y3?6IJdN>#=xK~M=kmnx+tLzhe0c;4eq zE-okg60vk48{mTQsuUg_K3~Q2O*}nWOctxf>Qr?q$<;;w&>{ageH=POmeY1QEm);f zWLe}zH5p9dU8~});m@Of7qyxm&?bO zmKOam%kaYkN`qXe1!|>=kEu#6NUD`ueZZ>Mt$}5c96@5u+5-djEDq3EqU;f9vpU^7 zRja7gVzRPf!CJ6(`MZwn-*4~w>}Pj%>IjQCU57%~DpS>Bt@Ha&aJ_x5f9kq_rRz5H zYDEoD7xnnUg1zfApV>9A-`;QS^4ixyZmfv>iYP7WUHjs=HEtFB!hPf8R{px{3gWrI z>R$=36E#Z~gTwf}aQ*d#tHkyB=Uf-o9F19dugE8V0@vAjzms44xtsYES_|E!F0`Nf zSUcaPd-(r^EPg@Mt<;vkyo@+Z=;11{>W|Z^z^nZRf=j*OHNe-9ubXu zZl_VG`%aBvm3py+u1i*eYEVf!JQ-AZX3MqfkMV`Q+0yslT`iRw)uSEOSL&!8I#fmQcAtrbglIYBwD_lyi(;&OAB z?WNB;&+&p@>Jynh;1SNEN5a`!I#ohy&Y4PB@S<9qLZ@!`4*5GGrm<|8uaV0AH&?pv z?H+qw_$(tHe<-r+yt5m#v#0VUel-Ql_}OR)aC5boP>Ox!O1X-;0A9U`Plr5vN>Te% zg;=%H%@Zp6bgEJw=acFrey$c1L7vwVN?&<;W-@hBj>L>Dfuq?Gb6z(iTyh*MX}e&g zQQL}|k|Ig6_E9w=b8DZh%1T+0)mQb7_2T_X-|DfPloB-^tH;q|#!#x@T1qtPMC4e+ zRvc%@w6%CLX(S{2C0S8b2!zK2x|JGBw3Px2Qx;y2Y1FBV8jMMmvMr(94iBahsmU2| zITeMiPNh&uTrel0Z}af2Ckp)ERWMdBQSNqCQ=3l}QuF#%ier}e&8lt%1t;(8hNfPd z49Z?_S6q^;uKvVeknBaNQ;wBYOik-brn7@?K50mil-XsMvzbJvY~VB};ZI7De+Jz) znS#7iL#bD+B&Sfa>0$-Rba|LBY%cV;mh1K9hladFX}IDhJilCD&ZezoG?I>Iy7z7M z+`fd{Z4*}tdAbUnB0%1K@Zk(WADpCl$cqji7c3r}l^8s}Ri_GczFM17X|RJT_^c6^ z48J9d+&!qqV(LL%zsj}UtMmsV%Kl62!wafpUAibx`uXi{F36hn#;Q{fe1Cfo_)IZH|R75v_l5zSCC zO3VbX(99SP4K3m+mZl*VL~|(*FfZAQ;@OI;(aTZ~dpO1Eu{gt3I_00rM~eG}zO-WH z;$R^io+sMx<)rQYKi7ibpBUnTeX5Yc5I&IEwg1bTbH+whMWyGHNjsIY!_WUa+BU2A zb~;b$JO@uBFLZkjT0qKOu#ycz1{SLr-pLSO)v7eb01CoWm1;mDAD;xfYDwkCjM z^^^LsMq{aA)b+-Z^8N;}R%0b+7&(2(FqU$@Zx88)p$}Vi-)~$otmwKjbU8g*^fTeV zK14;lfN;7`;)@61+EtnWb5a>1*_Kj4G7%(6qA5l2pJBePI5EaI@jhafGY}~$%mB5P zP?4Uxr#f9L&q?`EL$Zk9uDQl*wl_Sy%97{JOJ(J7mwqa!ZiA zBDMV#dZSv*0o|U|{S~~xbyjqJWqxVNFH?I8S%Ro5_^W5h)(5^)?t}O%(m19xxq*|& z#E=G{Cv*es01ks}tH3nCu*E9L!)_iVX%a|%V-gy%`sJR{9=BlTxn3UN5sR11q7*Ci z6=J;KEZNb)3WR;$EZh|I1l_uo>gvv=V%j&%R8LRJq}#GxF}Ev8w{hEbY}{4msV+Cx zm8IKEHwawQ<*7_i$vIB05@b>#yoLoR9G`?Ed`Jlzp+z9IVb}_%;8)*(QFA7EY=dmf z5D=jP(HXg<6OcMV!h!?@!RcB%rSBv-ph1M^pZlFgJ$G~dlAoi-_NcL!Arit@8P<-@ ztK2z>wA4A~D*bFw*ZlP{-(T=anuyP%IHGSNT>wB9eMXpO6Fk-TqR%kixg#mSDj56H zW@!#xP#KepeGVo9R8WP)!)8u^4wv8!g_ZCRuBn#8U#2FZ9_{DPz{>3i? z@Qg+jKq|Rn#-dtOjsjHaN=%PJuxPeo#SN#gwf}0F4V0N z(^Bn1K4)d)8eu!Z+a;h!(#!hEx?d|out0GMFjk9bt)N()An0D5-pr?qeQFhL4XrJ- z(h#tGpYLpPyjt8%0ikdnd@ODz9j~vD^c*MAA5X_(rXF+89~gM(k~vvXawHYL1nM(U)O78Eqf=Ovo57$v_V*ASRwwD$_&O&HC{SDw$I!byXAt| z#TUn@xKw6bLG9GBhln5BSFT?3734(Mpr}x|KN)85+-pw4_CVLbmI7-*`&V)4YCccH zGX&dDtqroM{;#|!eo^PW)H%Qz+!N~hDBVfSVik8mA`+LcFZ)YNCzqFxFLm+-@?N5u z4x3Vyt6y32{r0?9+xH^3&fSoyVMkPp_2d4LBZvGWe);%`W5BM}}(qedK}dd(Se=<9JK8f}jwVSi(O zJ6|PKTKmQ#om{PApB>bNUV7Wq%)s-e5X_&h27t_G7hl2tie>!UC7Zl83;$# zRMUuA_Jz+aVZSIjm!J@6PR8mk*twM95c$yE)$vXm$$62$@f*w#JJjrT;O{T(M82|Cl=vsT{5kXr#Q1H1{i4_yrW zUIl{>1#og|x?F*pi(U;arZC4AH}15ohcojV`oC?9lxIRaZTN8{QF0$n>bY8P=RmBK z5cX9Sn*An3>V-IkESJJ&ndhPA+^2vOkQ548A2?sA@{_$rQH!v-0>lt1BWp!PB-5m& z2{?Rv?_F zxFO}#S4JWp1V_pR6;d#v8s+2dJLvk(d$n$uPlQr^c;9m98!#^LgpiF@daJ!jPykpq zmBh!g1$o`mu^i>HzVVA7_ zyR4FpL#uqOG_Lz(7V-6E{ku`%2sp;D$ietv;_9mtR)7Bs`mOM2Rd*qjo?$%{nJVfX zvNDK-5VnWNy|zIj@E$Vy_uAPms|#=N^g-|!@av-L+pIDJc zzc-H5kD@&UfBrtAzKCb8wzL{7ZMC;;v$uwyuk9S*>nT2fsIGDH^4FmKz+P4*gH5Ff zdiSGi~d- zoz-Ki*%h~Ky*ymFJng5g0ocxY&v>t&%BQ&Nq@u2E1C`iDF6;WHX%+hdS&k%9O5wKj zwbumJz(9v*p{$b>1uM!L+Cxq+EpezdrLDmjMulygq)FU}(w0iUy1e7#D6bPS)gTv^ zS1x3{Ut3^qwM*;{d+^PKB~ES6TzgF#-hfp;i!vuEnxRwX=QLy6K=z#Wo)X1;;PlqJ z`v}dy=eKg$nx{3~i!nu?)3R+jm%zMK5J^CC4(J9(_^Hs60hC*-?3}@ z833jm9+TObDnJN;JTl>V;wvC>Afb(LAvC|bVT^$xh_p^gUH41yBf%tYl<>NF{d(W( z>$5`t5`L_g%OxbZa<*I^r_1&6Qt61ksN-EPFF-}~VtrO0@YpH6&x7@|LYNFl3N~zX z6`5I3j)DYxD~duKF64VSs5JbPi=wR<{)wD^Tak{JbiFZuv|CT@^ShGjIDOyKII7S0 zDLG@mfw$ji=uUEVtO6aG)b<@8S}l}Du&jcs3h&vtJ9D@09aaa7u@$Zw$Mtb_MnC?r zJkVawpqibim7P0!h{<6V)(qz@l^!98Xg(buB+vA?b zl&IV0|60w+W={g@H>=M$_+{^S&u>(Ti@=w07fl7B=MbJGd|adz47FgK(|Za^=&$M? zQesy-=XiN%c@LWPPKlcBx!thPX~N>h<2%bc_n-k!U9z^l51&FsopDY!K2>O5Fa z_c&4AhL2*}jCpxaw_Leg&+@2886cZnZOi&&9!2yGJ2ChxCzP zRqGk&)l@B2JDC}o9LYdCk07=M)`|T|-}Uhx63G>u`;Ir{IX>sbfq`PvO2uL+OM0Ig z4}!S*zI-%d8y4&g5zDY6(a*}!7=4LFH+Yq5@uu-7QeGlRu%k2A!Qkc zY7BuCS?S55NuX#3T(b%zb`4lLS)86BV=}Zf3^Nr>33mW{S7G-IlCO$uG@ zO#^r72KRg^Wx27K+rT|M>E!-E+q?Dho?zU)I(63N!OiZev7A~{r~hh=Nc~1#lEvSs zD!zUE#=Q^vzfnCtpe?%FgW1cWOSbvUARlS>$r=CE9;u1a!v$9R&nqA$PwR`1-*dxz zb;IsdAW7Y~rXw;Mb%dNets|~*&rh9s@HRz$d1#smc_m_9{}FSX&`l5OaB6--@snUu zrI}3Q3v^?Apg)kj-huv<>~+U-8Aq~AZ!oRxAaCN6F)7~HxnMz)VnHsWnObpZ1I)cb z*0*(7mn3g(E$Sg@UjwbtV7*48v2sd#UGRiLBIiS;d7TH*RX* zFMfw4DK0gZR$j4s->MyktVtMz>g@jg`=_U;mlhWG4^CIXQiQ%DuEYIm1wSpE1R;+Q z|Fqj*w8&$l4wx%MuMIymTt#8v0?g)-$$W&O1mLO*g>rR4 zFq|Ze*0347AW1RdV$h6OEM{m*M9rlnY#tyz+u<@-L@hPEF1$gtOc$D_2}?6>GEK#B z;Ua>Yy2Fd&z!!0#{~Fo4(32RAn7$PB5x~SXLkD4SNNBo)(HGrKMhXb#Rnf5-fg+*1 zi-xoEtQ^glSyfLYOs)I;Zaty}vf{1x6xBtPMMOD}i**%qv7FhhYf*(R^^!@gdq#7e zm=dE4zoV;JGowh5lNs4raj7yT2iWo;XpQ@Hb&|0##cnq^}|FL7w{L;SW8r$Eo2#;C$-$Y-rzrfkha_q%j03 zVOCI70%_iuGVSs3s!XM*dB*5uQO%A|z>G4IHj1TSz&?J-nGgDnL_zaBHOQ!?$r0a5 z1e1o3fX4iL(Cr&iqa<9~^BLueV6>6ld^D`BqM{@5L|847CD@e$05B>A$_>$;q*B;m z*+2pQ0f`5?`P%EF@&Ph2eZk8r@!lRiQPNy%sFG6hLnYl&f<=!MHO*Vp4Ij?EFnr zv{69iQV63>rl#7FGZ@g|XTdVeUdf)+p55`w)9K6OyAND``FTrlso-4d5-t5$pk1=# zu}j*#dKoJMARbrqYTw+s9%U8!J3W_rhm}r$7Os zPAx5^ayOqeuMVz`edtY4BsERcYt$~VF4nJ>o`>nnh9~ncA z!`2|T5wmae!PpRYqI_(`EJ9^>yZgH1FT5mM${v0P*X;~q5HimF2up|!3{W&i~0+1 zI<&uF^mY1*%4&r(Wf0aFpg7E|(2NvD>4HOJiaNX)^kL{g*)PN9B3MO@&XAeni)T{} z^s`;HuD)qyUUk>G>XuwYQM71uH;j=qtVF=#N#mG-w=2tkyd=A>>_;^P@uN}L)m?#;~Yos9!!ejs+#6xQjg$9HhhJ1`Aoo4S^sF+}dsUK?SPnXe5Fj^*5pMt5h@4lp{M1AnAu`=HKJyzbf~;qlyYgY zyjqsd{baFhw=WQ6m8K*Hbt2WtVo@|xI}?3n<#?w-guRdIB!^NQ{zvGjoxD(&<%Ri9 zZ6K=;g^@kq_)2HIw95}u$m;V&JCgF(dHPDJzOX=z5c+ghj@BCufVGZ2BMX@-`a(p~ zfCr1m*N_vnW@qG(RHyG{M0ep$%1GmIcnCvcqtT=hVCaj8V+lvY!{ri`2{3lN{tYX) z;Uo1!WDx38Ap|36kAv#GKEKYh`idFDunt&PLQn1;8F8VX!{vju40@(mj9qCRh>wi) z!b@erD!Qirgm9rg`$b0zHcM4CbbtiE=z51dl07&2_8)e4xxGuhJoEPGx!Do<9bJE3 z?=o=Wv^;3e0X-q6T$okE6$FGI5Q~5b2t%{}I;!vCDym{ID8f)eX7I_g4=ZK(2;sE{LG9cCrKvi(oGVUaUzv{F%m@8G6$& zOE5^NFQ&+b-R>4J2#nfBIN<%dzp}Wvco_3{C7c3JAKZTgQ2@pXGUAJJrVv}4gcWNV zZAYGK7^cwT3c`hes9>`KKCZwSgg^4DP*gGacAL{zYVS!6y5+o6POYmX@~*5pWpB8* zoXJRWr@QQzot~h#&n-trt*X`@`uj*e!_WupSsL$}LLMj07VGEUjnQ|+&&Mi=zQ z{0PGGP21oalrPJQB<-|a>vrWW*YuvC+ zuIbUB%j46~7IMYjR5aGr*PDmeQ{dl@j83*K6C`#Zd;SyeOBvJgdG5p`UU^{w+~jl@ zOh?8+`_@Qn40YlPJPf2z{A|QJ^Gs{xlWKdV^Fg9{2bA;rp3?@)x`X-#_6m!Uljtw4V3{3d#`_v!|4~14f2G?Y$p4S4viPR)912`4JXd)~zg58xof|KdZPZzx6 z#^1|3j-MSgd&Zr*wX(MsGo93aPxfQJqNjV1pB0C*sefa?pNo&Ahw^1Rk?wJ(trOS7 zhvCGM&uVi9fFIh#y~6ay>3qFsT@T)H zj0QnIwOHI##2c}scne#8I&{9LI?us;7{Ypo-FOboUxaaz%kG=t(4Z9$6cb5LltU(vAL1D183)1BY%kCy}jBLO-=_8N;o$)3F$lozzY6E7eFFT@d%Y0di%WJsDDn!N_>@0 zn>EIO3Z2!%7#IOZ5bQQA5eyB$`IzCgupm&$G#;mt%3tn2=*o*rzUV*kQ+FZi05;{$V5DBgNh(lvie|!=`aEEy{szp3?jyQ>#Gv(_-lR3r zTNksz$3$rC(HpZ12K|2LptGG#n6m*d;!?+TlJ{7;`_&rtu(xFahw<%KIF3%uBZY`rS(efwx?+Zra%)2Q;w3U zZ!Th~llK;HgImw%%S*F>`Abk9MgS?{gPrx>lFzR^4v_zNU10lg+<^j6z`~fUO zHob_A_-NTM6NNZps3W@JB3Rl$kh4|j(v?V@%*%Rdg9|^BWkg~gypWm#j2hDuQe211 zp+^wKWJHymZ<{&YNx^VwX|^3nml7)Ou^d}7OeY4TLh9_2s==J?m%0+!yHzWLg~(0> z@S*7HI#%CpNTsrtBPD{E;S~(n0uhDS#$+bif#P-;hn+TH`_;k;0)*T{wkF~gH-SK_8|BiOs{|NIrd}d8NGE}UJ z>Qg%!vGdLIf9Kqtu?x)$p53v-JpcR?J9nBFTtIvX>+1o*LK{h&F9u0+pb!I^g1w6D zCE$vyoaht=4-M}DSdnJl<|-FmAw_P1mZ_Sn%xJBntv>2h(y^YC#vV1&1#X1US4_s4 zkSEQr^|@WJAvW#XP{jmaA|6Q`lH&3P1ee6D4-1!kUfD4Di2;z^AI0)+$FyC*8p1VY zf=e4*yyTVRCygyW%Hf?VM)lC4L)WV}5Iz?3xP)h0VN4*nGt?APH6a)PRj5UhR0^2P z@JI-W+zEYBPZ~GIl?C13?WzYaQrxq3|C666Y*XBu%F5B$7>q5(iO;!mNp{uQi3J%d za2tQF$^op|3LikylqM(TT%qUCl1W7L-0iB+X-Rq```h_pg_yp2_$1}5>yQ6d_oD22 z#O9H4N5*7BZ^{|rDk91Y!w}pwTswq3(N?tzR& z)lBjMBV|~ncv>DEji#NFqahl&K}pM$E7}>r$Uw@p zgbFJ2-;RctTF5B8bNIB3&J6EZb2AQ+co30oIus$e|` z*noXmQE`YR2{>{Pys<`tRg2Yf6A>M{Qjg{EqJGc_8$0}qDnG>GQV<`qqXd0rI z;+7Ss1s2dEvA8%-@mojt@2^W-k|kAgBH%z=^06#4YRHZj4cCazKu229922W=uy9g} zCK9kI%HU-(c7Gt-;JcT6x}MgU;Z9mWgBR9sUClhTKA zdn#H|j96)*>~Rb=X--{-z;1mWt8N>f(Ljir;X$pD6gYqstcuvt?kC0gj;92t9 zK~j+BPSQGT(lT**bOi#+CZW$M>IpaHL0QWO2vb&l(~5S-`fL-ehtT9`)W`b#6RzB7 zM2hQ5(MAKI>TY6eb4=DX%Sd{b)HML!8uG7au#-HE@ga=xi%9OYp^}0Xg%rv&74|N9 zF`-^gRZ?^Cc~Q|qffKF{MW@50JxtbbAZr!Ha}YHkLW1s3lR-LN^mBG1Y6gz3dzzed z-B?wFvlMHNEm{3D+n|DFa|y+aX?ol&QbeguH=(s-Di-j>W3uYj!_ZVa&2#>Bastt_ zvIfspJS!iJ#orN?>;$wk%XMEW8?jzHW-7Qui%QqU-0(gt-IaKZLr~d@9E-aKs^6aD z8Xv_t*o@e{i&1}Ya~k#tl$nH42+CtP0VvKkNQUvYXp`y;#nFg1fF&8>@rZ^(ohyCx ziEp%U6O9KazVbh*Fj!%nACe;x3oGe81Z)ImG+~4BBgu6+T=$@Y`-w<*fBKkabZUZi zQB)zU`f^?uwW)Jsaa)%o?+Cjw5|M|HePA29r$$_~o_x6!)w;USifCs9P>m){gnuOE zuF_=0>9qE}hC_`RPgpOFMr7T_7sa%Islm7LpMyxR>IDLsMQdC{JJ8iI?}0LCJy^IJ zj6$N}dJ5f8ScHdmf_nywD5Oe?9FYiIpl0a=Gt$tQLKFcFnLO5N3sD?OzUws$i`Xnz zwLIMk+oL@~JWEaCd{}oZryEgS3;XJaLjWVirkY}$sD@{%7(i5hH_=_N3O!b#VD%KN zzls5IKb=S+`xF5Y)=jelcVDlT$P8Fj(MosIoR{7M}})*jh{l}fjEba74#Sj>ibg)rUVAon)<6)a)@S<_`*vfwi7Z1$2bCx6pN@BecHnb zWR}Z~yJ;8i*I=$9zwHR2MA9Ay?fD|c!Ns)y;(uWroIY8eHzqohN1FLBjEGayWi49` z2gmB$--nw+fCk6CaKb&lKlxEKC_Qo3o{{MV~OhrM>HpZ@ICj ztJ_@29;)B8oeUaK9;l=6-#2<`&+QV;PK6f6)9}O25eSk9WovaB`cegauB-y zMfT_y*io_kJG@vSF+eL?VM~OoAp8*@HEdadA836&G&7u@36Lcg7IVaPdOZp@e!$}1 zXv&J~rYosR+*bz&5e}oMSjmdT^;RlsVrvQfV3|60!ol)Y03k(IRaxbRhHxsiC!UF8 z>2SnwlY>JE7a=!#Gto7gj$=vP7{!Q=X;``nbGqYor?86Fi(oCiDPaYut|g7`xPw?B z$8g4B!-`}fG_(j-?9+}H3O2H#mChD+#)#OK5>F5364@lq$`;&GfKpL-uo$QRM}rvm zk zw7FMyEFX>9ChV=UjD^0kPSDLniroRYmUmOGsz=~Gu(0_CHv2;BMY)@D3Rr6$&5vgW zx6#I9gFWkqj7TJdETUMPs~Olq2n%g!g*L)+V_L-WD?!{(KrS;R6ibk;*EKkYR{_SenB@ zgvfumm=G;A4txNIKQ^hssLEqeR1Jt~IK&88R*h?@6~evK2DZ_zB$22UxLAFTj>0ZU zfU>&U(}On9u}mDBk|<~>tZD{^Rvi-?H9(_}a!ErRo(u(^w&&>{@s0l4T&>^mN4neF zvW59S^J7^qs#XLn6jPtD1GIJ^WUOY^Bb4gs1%MPAp=LUlu~;2GAMD?NmPGav_G!RQ zZ7Fok$ojd-TyAo1{YYr;3;|V$A7aor^N@`buy}4ky!g3f&p2&$VSssrb|5{YNF!nj zySU6uV=Xl19gZn*0zq>#H46MtaEc}vR0)Weas@-Fn5rpc>v*`g-rHNBr;nHEc`v3Q zgh3wRk#T7Ym$viBnJ~M%h8|ZEQOies8n&Q_@R8{eqa1kpxM$R`XNMP*OrD`!dU`0U z27;u5u6i`$Scc|f!yte&DBE!HZpmk}`L48@^*p=V_OT(7Gb+b>;GzXs+X@ zAZ(Cg6|w`i_xd8wIGNIb46sKBKoHhABQ7&E$pPUbcx`I2447Pp%t`22%gy64pxw(S z{e9MK6q`r-#~Ob9lNGEbOXn(GJ_J(QYIxDQjh`NH??PNed(37Lw-l}kE@90f{qc-g zU&xhZsO}is9s9WhD>cPkbOY~^1wD*Q4e>igu!YJG*{jILONvlr{2c=jYaLt|` z)A{iU9d^KSw_krwx)L`Fu|mx8KmP$u`+ydI+uOQdscEm&<1cy1%dXJ0D>SIy?K1aZ zo+%W2gjLGqf~EjnD9=+627$^mPb043fK}LPH|)X{R@th1`qL*rexR_`Y7`EXNsS@w z3LcdW^XaTHhY6&UAK(<(H7H7lh>pW-u|D)jx!fq1#X*=cA|^^@{MDg{t+o}Fk0S80 z7}vBr6XX|=+OKb%wGEhi`lo)$C>cg6=O1aO3+=S*oqW2~3IBL(S%ILy<$TQ^fGvW8s5(-uYpP#&B{fSI*_i`e7OmI?THdbk=`udEObXj2F+qaI2p@ z7!Dl6D}~F-jM9?$?$3tn$MiC`X6uY?*m=5X-?vgIhH0M(NaN5*p^L)#)(C zbxeXMlD?A^7pYK7R31pMcV@dXaMBr>uB>52C2-eUZc!t8QZ^1;2^lP_QPuDh2wcsG zGzxM2RWK5)Z-9kU$0`TQN2G?U+;WSexxNm6%Yg&YSPV=Pn@nk%tYtEkLbNI-!d=n+ zLZ);h1|c8n_;a+Y2}Fg8rXv?#Cva1xz;9TNaQ11>ih2IVEp@c%!ig9 zG9IyX5%Y}f8PwbG0Q~mtmXBsHqbof7_N|nb8r-|ljw7&Q9vd7Tj@vixyB7!Z_ija< zLK_)I=eIGsNGn(;W(Mgo$PT;8RL}!8iq<3eL|b$rxCCMk{;d!QkU!#1$C+^5i5p-H zi(rcqY@|W*Ys|^P+SAjc7+emPmlqFBOdMLbZUUQr=;0nM!0m^|T;6ZM+M`|z-mw}l zKoPoQ?HzFlX9_zGstoG{#&tNfQQsyB=;} zi8wrK>&M-3tOLi2#|E$o_C3<)m&WxzwK`zhSn`6wgx!pG`fwZgD|*@RusCvB9gWTC zo-v>%v8xGm2i1%osNXCNmgO-6`=01FhLS!7FUTodCi#DTjB}K|2D2hSagzKLp{-FE zGjXyug;1wy?REO}$(3&RgI z`H)StHZ+Wa$wSgoH1n7|CqvhOGDpKQG<0z2Zs8`K#P1RQ;-tM;(ywjoO622`l`RkV zc)c;t#NKujQ^`zLE@b0nuaL%zXJp8zxihlqjASG5Wpt!JYyLEnZ~&N-UL2}db;G0$ zQ2S<&mM*mIxE0KAiflq`8Tx`AiXMPSh*lsHz?9Igp0~1pKmM!U%cpual}`HpBHVI* z&&xkDrR<%<7&zs3CChUXYvcOCttUfm74i)bLro=UfrEYOeI*79^F9ulQd)EXs_Uu2)g=DItD&Up7}HzX-5B^F+OZh|s$qh1&C!hQoD*4cL+vtFpMsGG2L7tw!7%(GdH z51>t~(2(6elG|k^yRsGbL5QGfrw!UaSZy20$e^@Zyw{cHa&~q5)*-Bu>l;n?OsB1p zP3wzpcex^3fM*7`o-=LdHkC3XMQ^3Je$$ARp6;Q|9uKZ6<)OaEp29c+rvr?rg#jSY z%t+6`q*2QPQRew^=`zU%r&p9RfNxCND;buil$D4+id~vuJ5IdX)g!8;s$7XBU+wD( zwZGt{~KF6{uXa!f!V`Yh7=;NAK1)%U}tKq)$rF8G6p>HD0Dpnq5#LC0Mf+Y#yR3UFM|v zGW}(GF^OHCXg@*l%Vd$py(k;SOPxjkK?!&bx*BbDG65wvK?h*G2qS<-OYaHj!KB>= z6VOp0e#EL36csFc4janBOFl!)6GlDS9%TXueVPt{UvV*Qx`_7#snP8X7|F>mHef_c z1XOWSv{j|JDCscLL4DxZL?Ya45yts7TPs4Vp#2$1@qqe)ZJU*Ip_{b#XQVrD!RdEE z|9Q?GCw�F5-nf7h&%A$e(c97K;k+?6DX%Rd8YK)u=c;(ujQ6j&nU*K5|wbt3YyADM`NdLUxx@J~b)N0Z{hgVPRr9K=5l)!>>^PMAxFNo)D#)A zi9;wb!TwcHj7603yk$D7k3m+~rG-emyENj#rIPN6r}7w_3njf<58_yqgsmx1JQMqW z$d=91(VpQ{cRAw8ISSwyR`*-BR}A#~>>%Eg*5zn_fPHK(&v)xN-IpWts5IDO1hG%@ zDn_T6#+eXvo*2GF?^!{A#zR?`K;UO%?N4WMs4K0D<01LoBQ|O_N zi>!uDKv*-FPLYr*U>BmjvF88zOa0$w+;WTY;;%0NLEhAR{+>QZ%~UksO`hL-laYuF zKW}M2Pw#Yh>~OU$TQ<+{sMU<_lx5qs9hSbyc>Xf}ReSZRa>By#zbs|P4Evv#&F=}9 z>HpdS+3h9yAx^})AyEb|jEn|z3H1qR!{pxwJPSl~z2127i;Y`uU068qwVRB^zCGvf z3|nQf{gl})n>W{Xpx$?ac69h2*%zrFR`5J`+d1nz`LqKN*_=aLxDZGWsjvPfho+=AqmX^YD z{V(zfT@a^g7Ut8b+cD&U*RN_90^8_P7&CD1R8`c%_m{j`+6ae}0?(ntSX1 zQs>?k+)ZuTk-^XD?=}60?LbAFp{&35`cvcM=+Vyg|0l=CkyF>BHorl6PS9e)ka>jv zlYz!-XRnskew5L6A^L5%q`IbMf*`mI@5{!+1V=CK9Pp9gnE>x+TF*R#gYc@$-rG57 zKa=(jIPIBhpA&3`0!^Du2Vl8tp1BaJyUI~H~QWGtuzYUGGmXtLk)a&DpEULdEv zK>!bpJ4POAnpubkzTucksuFlMfK%9i>}TK~6xqmNa}>A**2rH`7?>r)vQExazX=0A z45N8O#fK$u{1i%%vZe-QIWNigVexWawP0rcRZq^3p-}Q#OiBKc6y`JLZ#aR7Ird_d z0>p!rRiVbC70I;r8}Y)_ zu2`FlC)~WP9|xrH{4Os-w?tg1gK~d5g7Z5&2jZHzcj_9{LGXpn-h|-h#L)-} zAh@}@*jQXzT3!KnBsotif14kkx*ptl?Hv@cQ4Y61Sy@@L{I@d)3CDN#q@1Gv(25v- zYVeLpEo9J89>NfSFa#!CytkQ8g3+ZM3Efl-5FHV^m9S(QlLwF((Ily<&C)ovdl>dK zU4{`mj8(_}TtLVP=vRmjpL$%pz6P5$msG4BQ!rFqg2_aFDQ?m~mJfdk(K1$r;|F?0 zu)hf1g^?v=yIFt}82p(!JETakKGgjSI4~QO7rbE0!exNN*x6i8n$~*wRbbx2FSHwM zm@gg1ke$dKp9*$R#YuP@sEymadesIgS{RmP>J$I?aavh?;>4+55&rSDeS)r{{U=GG zZ__3U|H4Ac6Gx6fmiRs-9jqpZ!o=s&@&BW_H-V4qy6<~&?#$e6=H6NEEEr$_3^2e9 zNf0}+a1l3|+Mvx8E!ma`8w7?RL=XV6h$3S6`XBu#3kuYC#gvekY~+C*tnzh~!t|L4vCpry#l`@GNlbO_Ep_s(6;JqdHdg=vAzIus z3>@&i_w=?7rgKEkXY$F?$wWt6%J33FKS0|SMr*^i5^YJ7DD6kn4?2}d)Jt}nzF*v5 zPOB4@iK%XtPUkzs4ZwH+hsoBCb}QlZ?mrB7n@p$RMDuOiHcr8YMl(t{1oTt}nkry= z>>8dJ?urGmzNzC=eX$#D{jIJ2ZRN3!j_*eX2DkFqcpl_Pg z;ZTQ#V1NaTl@o%204-RMV)be^!oPL_Vd%-K#9{YvLd8!g1J7t@c-T?p9w6=!Yn({c z&Sg-TIf>46?5l1f*RwBkRSTgMFE#C%g)Xl{!7ng^lyZCTLi>;~Y%X(}|0bXqI!HKt=dX}`vx){CUqBtmKav~CWyQ2FHWo>-A%2i7a5M)D7uNnE zg@Egm&VwIN7ky!mzsJjo-5OwY9|yiR@Y5~NjAP8s9T3QLv|kb+6>H`IWNEANW-kjF644F1`@)zz& zd*teQi%^-XTn}(#UI@-ud-hmo9{t5%?D}yDx$DClb8E|}`hAhE`DTGKyy@;YOeuXmE9igP$cvQ;&o%X$|;EqX*N!XyPi0n(D!Gp>G;bku@jCY?n z(d~_l)b+R5ePXVB{CL?L9{vYjSa`G?l>HHJcz}c6h+md&3wZ>QV@2QJK%Ij768Ui) zu1XlbF`#>PgkxFWFAJdKP!$;1=e|Oamg_#h#YYiKK)}p2oM{k7$GGqSnQ3`W*q=pJ z(6;W-rXoZF)|&1V9hv|*@P?u(C#lte`%|g=4>cUp4P@ zX5N1IUmP~3@At~x%^w@j5SxFB-XnrR#ta%Q-hw)dA(ftlzR8Pe&%T$A8^QDp(LB!k zq7%8$Nlz6{pi`f|l_Az6}*SG57Bnp4{7?k zFU)99_aJEcy2EM7-SHcV;JP1NHd1|ON)h1Qj90^_Drq=I;ulyKTS6}t6xlh(gO(z0 z$D$wTqR-PP0)Z>$cD!UHI5~K6`yx*+>lse(jUoMMcYfvZxegy@6N&@ zIXE7}llV!=>pV$^jV+KS}SE0!giE$bV$+B9jRN=}AQRuNST!^6q!$au0*NFVJdN62+_t3;7 zt2PG-$!W-IwWca!tXTlSU3-g>JtE;}PG*W3CuSiS<H!;^!$hL7`DL3>Hv}%sHL+L_T~OYtFT8H`lti{49`^iDG~$ zK;$@hc~-S}G;%uKn%@3vyt81-3XSX$Ol67W)1d)+7>o4TV^wgcMTIJY2+Dti5^*~B z)fA+}J)3(Uq$HJwi0zy?71X*K)4qO3No&eo(RzqdNf;bdniwqQcRh z;LP<&xFc}_rX%piXxLI^K!_h*Gj9=k70t(^T$ya>DTp?}l94Zri8)FuFhuu)5lgNi z_ykK7jIw4OAp-d)dwLw-iU)p=6=^k{!1##k5BfnI-2RwF9F7$S<&x$$i1aWAu_hkq zA>ApwOlySvV?o^VKj(ze1`b}ua>v;3ifDtq7tyAxittW;PQn5bNj&eYn1_#l#B|&8 z*dM{1`O(00dlL3uFN*;twr|`puDMzNu$|bCkxUs0dw;?{;yrK-PD>rTi_vBo&rqN7 zeK9msS#PhM=yAQ@3ti;N$Cs|^yUN-duD=%aET?6kZq4fu^CAOFG$>6C@Yr}nh8dmJ zl(7-jiHZyf!i`rXr)c;gUNXaPuL|vv&)5I-)hfg##GYx+-&YwyV&50*EUTob8{w=3 zwgQYUa4V3tiQBTqe`qOTt*@K$i_vNK_`&qg%*!B4oUuq*Q*$p)Al7!QU0!$DTU}CEW2&fcK zB3YmaG)?E9GNN%amPi3}{T7m8xv}V358nvTGK}jG1`@+$0)e%Ah36fY=fqJ`imL__ly{9WHV9*tu?BZKVt zZaGQMeTeQPM%Yj^rE(aZCkvB>UC`iZuixu^#0!xXG`zw?`aqNa5!@4#HXq_nVw6Vp zibyYH5LE#)_3wl~dB%I2_eihz_?tpLdH3UT?u&00@}x=AshiM}idZ)%wHZ(b9|pi3 z0=%0UuN&C0)C7w&$AU0tZ{CgE6aVmb|qKTh!G$QtyM z-T`v)%|SZV{4;0#%%L}r=Jb>HRBFn8*Tc1j4(Y$pmKy6(Y_%+K0zK%>spHm8|hZAHY zCAs&MbF$PQIe0MAUpnbbO|2&+kLc8t7GJ_O-)s2`^ngj8P}A!Hkv8bd|9YwWO`E-yx>IYNl6fg|vd6)MFc|Y!F+Ox&9Pny6&GF6!g(~uFta&+=z znPeh^u>$Dx!Uu-@MDFMTKY=2#q2H%n#2&e$-LHf^?lyai}BEvQ1$J=-{UncK`nB27%^vkycJXbGcgVr)NJ^Lzh zyw<8otLIowP`9Ap8UK&nK_#Ebj~{Wpd{Ak3?%ulm-m`DbSflTH?(HU*gkxR&=@Rg3 zN05Q;j7bSy>fnYk_o2W?eQ%9vJ+hG%%^ZqRxMS$lQG;cND!;H3IMH1iE~)n6DFBa$ zR4kcJl3K5Tt}O=367dNz$wyJxnbGKA4(y7ZIEmY(p{e0gNiO`s7>YX&mRMY_Y$uA^ zl5BjWC?vgJ+)K>l8#L5aqBHKH1<;R56tgH%5zf$Qz2?A&D&+`K%x$^$j-jFN>)qZN z9?X9^Ki1pY-@dOp{&0I`cey#Pij8*agC^YF@-Wik<2;kc)O27D4FnpMWVZ?r72q$h zIkN<2%}E?TA@2n_0@juG+JRJrQN1jJdPN^p#KALVD%KP^JktRH7|B%DOOVnOQl9WW zM$nQAw3+Am04=3_k5i@*2al)y3(53x{GmM3pAr<$YJ}+yU%+&=n4U=eO0LSe`$zVt zJ-?bwb#cSiwpKD9bUozjl9%Y}?)nfv?rofSl61o#x4XOTkDC$=iZI90fv+GM)>u38k*FMP>6*+Eb0ZuU{N#8jG^*`j%mN@{+HH|0*~Upi24LWz%V0jN)-6nt2r{8wWb5o%qC~K;h!%wpnibO9yt

QIL#>y%CVi`Qr<0@Jo{Zn?THz@vbQw!bMh{Bnrv`W#GftjDPv{@G8^Z8{t)kx`KUL#*`SNFr)b)@Y_!6jP>Hz5XMF2 zDtao4iaF2<(=fs$R40inKu<{*N;k=NyGyaPS3c73w;d6iKs=r;m9j_L{QgtVy6&^? zv-9)!P#E1a57b%XBZX{s-@g1`aaFpQ$tsfJDK7c?-@2c6`Fs9ZzOv6Bx#!!m^7)t9 zBm8U9Z-@0Nv=g#?RIvVp*566=EfI-`fBWbOH)u<@9X#G2>+Oma`!dnC{;?6+yh`|3 zUvTV5SA6)yxSO#n!(;n9tdwkIh=)8TY6YYSkZ|F-LbWtc2{qI5>aS#m#i}~o*pRwF zS%*7P9i6F;Lx(z2ofMx$>mAPb0hM8`5uZfye&5j?je+5z#jEiG$`M%lP_&c@uflMoBlfS4qu+lK78n+`^8*uF4wzHzH+JdRI0t)o=mm_Vn=iwszRU#P%|xA zvB!V9+(z)suP!xC=86v|IXS$77;PsLq%#5MZ@+uXUoy)>>>V`muu1yqo=!aa z=;t1KC~^Aq)d!~Ik0u^{JjCJIUQ=&~dexRgpy9tAG=ue) zZ)y3~mJcxpvB44rT$9m`$|;!Vj?yyF5o)&eqhWdc-$y|(AsHOGhH?6~V$atS zK{CF7e>9d!9QHC%2ed#?H!aflqGlk*cYgw-zXi)>5h9yTAf=emNr`5)Y!rw#@kj4% zYFJk#U*1<8zcp!@4;(=6;9GX=;XR3<1C5Xw>BuC!askhe7(t#y*E$(=6QCU`^^e&h z<$z)lN3m3h!@pU0jbtKz)b;^p1JJ202_+OT%d=-u*3JZ%X>RS;hA)BGK?J+-5cB*V zTAD#*=|;t`0xDfAjOAr@?ZFC@8^h%&>WaIj z_|8k*E>R7in?B=8%ji!mHWe$J#0oVOkmEg`Ci)j&?Q*pm96WgWI+>Re=1Z=quLHQc zh~Y~93EZaLGk~wLv;mb^`ZAC=0qRfyqE-U{eu4~PDIqNrUbS2ML+h#v$-Nd;KO5M zDyzc&2PD3ZIT@ApUh;!?dcEzO_2S1kt*y@+-{GBYtW;F6%Has)6~=n_ZDX2 zMB|z0M6h}JFL55G9tM$&rYbhrg8Im}2Tz2ACl;6@7>Evi?agq0m~(QfjOFH8Hf3Xk=!LT zs1y&`olg;IeF%}6Km91ltoX`Hl39@#UzNknc9-`MACGpZ=%9=UjpoZUy9^%4_{E%S zO8CIUWDX<`8PSts7Bq2b;6*1z&|ykXsMOG4U+=?CWYwB-x`V=BjT8dwX{)_({CFx? z=^Y-5bQXFG_w@xYo3Wta@n01SLANty5yJFvZ{Oh1nbvkL2nr*)jQK zOnuDJ7kIITtS;Dhg8DiRzl+CY11EKim=ItMh<2y~8b`wqp;R-ssY-4P`F)!c+m^=y zfzn)Zb0Fm1W5vb>mP}xQ-nIZ@srxoTx+$cpna)aAI^9+2%$yY1n)ddW?-8iZ!NhZb zW?Y6%5Y)Vp*b_h<0cS%Ny>z;>w=fplz!Pw(tXsLs)v8ihQv%$c_gB+L+iv4Xs zUN>w=qNfQn?!dh;!ssM40kY^4pkf8@@!xaQdXIHSAJK|REZ1QnVr z^oTC<#k*cpj~BywXc4@rYn5C#CFUT!jrM^8-VmQF@r@M|uLPiBa6{c~3D^rqawB&4%gx!D#IY#6K4LVu7)rA$Y%e>q- zlPc))O($8No)#@@e~qqCo5tTCNtCGF=6EV|fcG@|SMjF7#|oS5=|I{F1nCW^Vs_VVWCD`)QsYIZC|k zEM}OX@K=N`H1)9%0`b+-S|MaqY0L^oSn;N`ZFmacf~mjC9E1@70r564#{}0A@{OSE zoWNO^ryT#8SE z(;I)-&$Qn22x|0h>6ehl-VbhJQZy3cTb!5aC8lfqw{zQT2FUy9?SAWdUUC;Ti;{SuzVCDu= zFD#`M{Y>@Nt7t5zw#Pz<1t9DF+giwzDEv#v&o&qs5v%E@syOapW0Tycs4eo4nHmE7 zc3}CNJPi&gb9?IrkYR71jRAt3Q7Yq-JvNAeuPHmo$FTx_7*5=&%P~47EypsucM5g_ zb{{>Cd+p$JK;sToZ{$=&BXYVa6ziza!SNDk_B3L3ZV2gy3od1i2uwXkQ*Ok_7f$rJ8v`A9z08k;BjH5HEy3eMY8wQ-ig*@YeD{hTPI$Zp*=qV79RolV#(^tj z1>e>Q2u%&+|Jt=RE=1%YQwWysu-h72E!hZBW!?#gE#1~Ub}|Uoj#$A&fg| z4ukK~yQJUZqpTS>u$|z914eD|LUno-K}bNYGM~OY-M777lS!@8Utq_j`<4v6*hGBR(y0k zFUUkuy@zXKJL{SFJ;_QoUeN7{4ni{n%#R`Hn79Yi;*gT@$pW5qHym>&!CH0De9P8@ z)6<8}KGo?D4tam9f_<+0>rR=L-52cL|G zMP|sx7ubHfslyOHBSi0#n3*0lX2S0Zae`H?i3;3e3hWM<)>ESCwr*|V7#>Mxu)$)V zf%0e_AjYSeAP;O<)dQ3f&*#BN@=#FiJJ>fJx}bu;f3SM}zPw+p`fy7^lfZNr-#E## zeNhE)vjL(%j$^+ln7p+rN8XAkP4H&hk*t!;THn(<(S5B+wbM9nBCVcJBmhy^T@xs}-xXFH-JD2hkuty|yh z+VP!h^##pKiPGHt+zdE?pKSRt=0FvD5AfEcLKNaMD##>)u8r1wQaooQcm@>}K+{5B z@Ek|*#Cf-nha83ed~&{K%c`|PUUvG?fuelDqo&3UP{~xo4mqYw>6;LS64f5zpwdZ@ zH98ZD7E&)fQ234X2|P{|^`f4xTtE|pn{Ow%=t-iT!q6H4F{2hU%yfb9zW1g|d53r# zyf%TGB(@T-z)XzTzI1C_Mv|{s$;3QCl<4=DUAt9fe4LAppg+T*#{#XKh?$Zb?amPa zNCE~>%5fNu27Zw8(ngF-xo+Ho^T;YJ+S zAdEJq;)RY>J`E(fgI^GuTgO2mp3eXd9ubp)6^W9ZC}{rCqmgLi5&vTTYM}qW)W@PMWQs}9V^dn z*J6t&@AscRy?u*&dFH^_BRk_(?6wis3TTlQb>5uG7Up;OO<8MSnSS$zS}GOt{X!=t zZbxeaVCu$2bI!7o6Sf=yhdh!b0~$iFW)Yo_n0Q+vJzk+P8rP%Wu*AoRi3PWXCIG&W zUV|CLc(5JmlN)OU^Syfc!J0QUDBJP90vA%>ID1#q_-!tM{jEs`fXM!jNBYmeVI?N#%a9Je^?7c0}wzIZh;m8d43E#8GHXeUmg*r4N& zlEL*Ht)@*bvdoF2Ja(7R1j^!qpB~=oVw*B++OTp|Jj_Lgx^u1Ma2`-F76GV*{z;B( zFQeDnhWo(VYs;3hDjV^W@i4KOa&h&rlU@5$mTN@2#_rMqn&792Vtidwr{x2_Pr?JXYE)SRPT{{kM#aElqg}R`pYRBZpT7}rEmL6xYT}x4Pey` zP$BX=$-Rz;n`S>XW30u$LXU7!Q17->3TDXl>o+wb2`*OxB1*8UgxCVE5y~Vo9uu0Q zl2yC9J+2s+3@n!JP}?G`4$?}f3zwCAE0Cc4>B|8aj~L$g`v`Gz)6>=IX*|g#q;*OJ zibnjd9ml2XY_Q$0@=VD&89sAgxSk2Kz@1U+u!RnZUYbG2lePDN%n+Hz%EE}nB+aZ& zzs0Iz$dre#&d9?#s@Vkn_`tH7Oo9kH+P19cP|II1zT;Z6C#q0U>OotediaxAA4wlg z?(OzJ)VZgSzIWn-r;Z*y4g^HU@$z@%?`wDFzGLP&p)cV)k+y4kz)94f7Hg1bP!KYy zYlt@%IdGFR=`GiluTP&j<2>=+C#-ANzBF_)eI_kmAK!ORHB~#d|B1WqM{5)EoFXSm zo=|$VnVDMay0n&S3^7z^JcBGuJxBU5$qI%p=$}Oo-oA}PT!T)ugX>tpiYKTYGC8!r z0NP+eDkRpVX#%T!sn{1e6fJaQG988JAtTq-Q%V}ZLWG*=;C8vyOGU7TVHr!e`_Z7Y zQcACCtai~mH}qxr=4IfJB@08HC$b0=-!p*&3d=de2q-I{wF~*2PIsgYhx{&RZs_+X zNAo#Le7m%Ho{Sk)<|4Ktj9ZZZ{A6C*Q){aWqd2qFbYc?_zQ5fi62l|9)=Uwg5dx0t(5)SP)Ja>0&ARUt{2b|y95anM6z~wd+uY!jh%BUHa0)3_e301Od|)9f zzROgk`pc7z!ipdGsQDny{tm#^9_Ce*j>i*jG>ef7?p$OF__f{3gFK4hu7)1tq30DV@10{4Nd;BQ_~h5l1}M~Kg0t?m zx4rGrcf8{rGiS~ahMu~dlCK{gogF+eK0b2yXnk>SbC*&wZ+U zAJJ-4!Su7Pk?gFL1A~0oO!nN>!GQ2!S@&DI&d5JW9>TbL|2CDh$ z|BrZi4054$4c>#k7kvlTY3Q*2-%v@(YQcZeM2XOMQ;0F6Qa18M81?p^Bw{`*xS`GY zP(n8?7!G?`=}+qT%a#CvL00Y_?O-af{8}M|#}n3V%sS0S!|%vIu0g;V(s+9IAkzV! zDPl$F{ssY|q7yjQ6CgmypXG|9gg9=R56*jYk7b62_*?S2yPJQ9B8e2CsTR(!mP&)r z0uRj7aFJeUmZxS}UXFf6a?Q*M3U-L%XaTRYI0y+=^hyaPg zq3auAdOrYZ4{3do7>agQUgi?^FNuP~k3nqwA?^?6b4$uFu}m@4=GS<9GY*?OwOvv(uN-lXuJdfQ<(n z0C6TbsO6 zkt}zjcEYpjRHyyd@kq?C^2#Usz;QGp?bEnAkwPkl+14}#SU4P?jXdp0F=A;G)?L&@j?2)M{YGh;VlqU0SwiY=vvW za9$a55W$@<$XLOyi+TusU&A-9u-lyti(fWRMKns?4>$bO61&{g`tfK}+P6)d z%24s2!bc6<%|w*Y8Xvb&%r*SIa^uFK*Y`oonh$h|>skqCX>nZZZaSZ_nBsi~IoZW~ zhL~op$Qx+bw%?Q%w6ykH%Qp~~-8;?76GcG7VmHc6&4~Z*!AxHOT3vXMWTSF~w37N4 z+3q}-IVUn$n9ro2IY76`kQvt=#X{QPwiGH(-oy1@85lJ>>M2>><1Q1erjRsZ#2Rjy8-w;oR?6 z5_uL{%g}Tnp0X~BZ5O;x(w7VxGP{I5?Tm2HT1d9tHBm;9RZG^A1=Y5H z{ZfaP$>y^N0!CK`Q9w~I5r+akT9DdR8_$XCz3U)Js88KL{BJnIvkPkQzEjy`>d=we z$HRwo4S8*)cz0*|&``nOQ}gqEhl2KUyuCFw49Cm|9o=i=N1Dji4bET00MTtpG`-9z zP4$^`dYx%ZX%R`jM)b#R_x8=3xV24@Rg@3CueU%Y2*%w_Czv8B0DnQ>LD1_lYe<}7 zvmXSzTG~L6euPotwIv@Go}rizEo_9$7;$aX;Pi9|mPIq?M__mU=A8N7S#MuvUthsc z*)*|+lGG*X-5)Xf&a9u23=~GXz0*Gh;fuW2JGajTamdZ}CH8d_QEZxf9#E0$nT>-k z4k)o?F=?2mwCLO5t2M7Bp8r}8yzS0E$=bMWCEWHj`G%t?!t{E`qS**cd`yEN>96S! zlU6s#e-lb@izrZQR9m5>Kr>N0xK6tcQ)lAu>pr# zVDuA=URG;lwy+~}V|QQl=2@ry===JYKchdNJL^B*li1fq8izi(x~4o~^4=jfK{Fq( z1RG;L;*Z<%Cv1S8kuods?;zF*w~Wfy@Oj#A9XX9;AyA-uhddIW2+hNDgrHG9hY#nHQD0nDXe{yPi_Tl@R@0L*& z+h*}o zwt&(R&TQ~J)Ta?L3xUck2SGY85P!&TWEgEx0lqA#4_lid*FZs;sd;qvb{ zK=^sgPN0-^5*d(;W2Adeuo!{MfRV`2Q64XR{ZHT|@MLdhOSv&KL&C` zS^TYedBd>L1$;h?@cN8~r)Wt^jwF282U-Z8!e3%QjbjjaKs~BXt0&Zqnp5*?S#3ZY zdhi`COpIGZ0V7evU|QG=P=&)7jZF@V^4rQzj966;pbH-{^$HDxTIq}wsu;DgaCbpP z`IsxkBCHFS1#EYYE!yz0NpZ~?9ka}ly!OgL zuRbaTM6l5s8Jr5$kzAf&R*dV}3WE&hcjUl`Jg*0|Z^B-4BRwz$Oh~f;Zr4cOnmB;b zor=~>%HtykCiSqc>A-uQ4Ub1gKv5nPCP&AG{mxMl%ap-6K0?+kYxp2jfajRB$Ef%X zRcraeWKU%@Um30y@T@OL+O7j=?ghm>%XReiWS&WDPLoAxLN~0xisVq22@D-UcQHo$$k*H85fsx=gX!>~$uwo1`?m%c= z8^%kt@}}IBtK|mrE!S(ba<+0OLhd+^nUbnz4KjpEUGOm=D}dA1>hnvk%V$U;2@p6y zjn9}Qb#~fYkx3A=OefA!+`Xd{qT2^~fJe%^6=NnI7;UNsYyoe>Gb8GGCZ+WU6sZ+2 z+^;@nW2a5I0mF}LqXytq_KKPVcrK@SzM1(n5&Aq_9p;~B_N z>{u4AG(T+I*c3|NO z*V+v8|D7#A({hVYVe$GDxHLwm)*wUbL*#Zbnj1_JJxj2+iiyiOFfoqdkQo}OLCr)e zsvQu=nh;Q*$sxFFxomBe0xYG;AL=W)HD zgI!Ca@9EHJhb5{xf?9yxaGWAN4+BJcJb~n~2u`pa6^m!UpLZmboh2k;zmE>)62_vQ zzmnz-u@QeOW;DU63`-d*Jd55V0-c@~;}%Eg-EbO8cgwS}w{gJmP}JjW;7YnVt_938 zc6XH8Xc{4Ba5K4uj4mhv13U|2goI1jQWK_}pxrU#r3N4iy2ml;G2F;ZN0cTrz#wZe z%dXTxD1maG#NdWzff3KJ=Iv27Fj*QvK>}XDOkr$t$c}js9qR5FmYXGp!)*mV#!TQu znFtCA4>S@p<7D%m`%&JAu`6#&m3ddm93c%MZ3VzA?V{(9)D_SH8kUa`JDHR+FFBE{ zJbxs!7T5EXejn1;z$HNUXnmTKSw_{AEgAVZT{^-jV5AiCXIWw-^=Lp|*doYNY?n5S zEpH+@f4CoQz{xpDLI>&OW5<$FsI@c@x(;lxVCPsmq%hI|Vdz!6C(eKWcKP;0ks0HzQ{L!Z4ykFJzjPw*fBmz_?;AgmF@mAVWUYoo8QwSa zuWDqW*+$9NB5^}p2t@^wR%0a>JGo{AE-&1=)v$M)ns>>nZZrUCB>oX%&z^u9Y9YkZ(GrHJ$O(4{)H+ zmh>Y@D}^(L>Wl2X9#1Co$>fJogOjHwp8KNd!!MamHXg&tJd^EX<%v4!XrgT0pDDZL zcy~6IOeJI4?l^msR(Cv-25uwb_hrS?vMD2pT~_+6;Sb%^uGGYMX%(6x`S*J#PkNv& zY{TA<`X}QjJ>V#tebk2REuJD7?eUFuSrScIu<>GPmNM-FqR{@L)9)7dw)AsHg}&sPqgL5@E#gO0eMKh1$U{iRedI(J^Q`%X-jHh)ive;0-Sv-PX(sbCLwD@X@fDgfWTSjWrIzZb-o%0w{%5ZZd>j zk)?K$TL}n4jb*e}s71W?HU{;fgP3ffJdTy??P>E$9Q#8EGK+|z_T9r$asLff-k(gM z^G#;mSWm_4`Sp^YNT}#UoYr#tv!(C!4k00tu|9GbjBRKbB=jqhT47Hz8qcj-ye_-fNG2wZcjWfJ*E?e8 z$>9o5b;LU&m7zlue=V~E$f#1V>G_P;ozfbg7cqQ4tZ7rtcwC3~MTK-m| zYWkp!Ff4c(=QH473PG@*(yA7hc_boBNQ z?91f#r4j{JsTdxLDKnAq;*yA$1=#h9U8$6cl1ew9wNXQ7Qh#jwrj_af^SU*WNEmTH z0i($hXgIb{br>bSXPF5%hq|8i*kMcRQ73TKt~F-cYK_@g2%*+jZQH9W$hi&uGs-E^ z-is3JYvp5E7tC5Gd$ijT|5|nEAU-}*?)9mezMDW4%sBiw?aYMExQ{=sx7Q9H+>(Tl z(ses)-1hUsHO|_p#P*ZXx*$XId~v+SurT&D5<04bhm=L@l^M$RCJon6k1NSYFk1$HDQ8A2u52I#Q~cIKyBQ<*$U`w8NlJ|3*BT&Yu%lw zfSSH)U+XTDfQX!$q~j|&ynHWbgxM$Ed&^SlDeIHJ z5KN15mzAhV`>B)Ya|f6~*xq?A&aSwThx$tfDjWrMq@Sn-#7U+Z6|0QD5MUYU!N0Vz zJ!hUeWj>7N@X*0WVy8~U9yv&H>LoG>b#oR^%Pg2W1 zOl$TDcD{ zFOj7&K}OR!IBLlVHs4GVCs=j|%6@qe#6?{ga09v6+7l_2^lfzMGJ=~z#jt@c!5fmzDOG+-6lG$=gab%f%6qXMwb$}6e^aqa+FEz*t% zgbD@sNCY}0J#vL3t{@B{rr=<1p#_1#MH)k=!Opq>B6v8={~$i|C^S>IzEN3t1~yHu zPI>J-295~BrEQY?40{(%W7<6kg2E}m6cgiv9F&blk`6i&fPChRt~t<{gL=)7DKb8`J_?F~%a* zG`?ZXX%;cj;$L?8@(ogdgBUuM!8Ni3MyZ%?gB#aprUPQcf+@nMXPnTMj^Fnn+=t+% zuv$sP5yl&MCUoj@TRgIMJX5f0L3{}tvg3bn7P`LR{770Nwj^$gn6IgUWUVz(MpLn1 zMIXD-RSYuj=Qk2MpesD-^x?#Tz?TS7KIpo`=k_Bn65;%M&qjNL`V^H4Mwtd)i&pl) z;IbgGX0bBtuFuUK<4ZQ#mgEnMO|G4w9WZ17Uy(4SU6otdG3{(6+dA8lSZnTXN7ro+ zX6&|hZO#sDjyrYzd)4!s*6o|uN1BQ{{O#8p{S>19y-q(tD&h12>_XOou7vUdqE0P$ zM=e~SyF@2xxITcugr98hWniuDY@XO_&S_lX;;=})cH}MXOBpU_VvrbT@W4~>twZ1! zrmizsNbkn|KkveDGcaDd(WH;Ej)i!r!`M5H%WRaP$0+1ZVw=xt<0V$+@DR7hUq-9r zFx8_QM>@jsO}wZW5n{zZ9eM~{XC0-~C3~3%fTexjPPN+4+yBTwwz%pCg2`Z;Acgah z&^#uIz91O1?HBAqn)3@kC~DiQ;IQ~4Bb5OWu5Tj0Nu0B2O=Ltsj1aZi>Yt1 z|C_ya@!!2m@&f;f=iU5Q+#JV=urK+3mFrFT0WH1gcSY@iNkDUcn#2o#T-a@~e1T-@ zrF^lNhs%@=oaVJ%<2M+ZdS_z)=>EiB$JyH~a6;1<$wNcB*K(U@H}by(=tT7t6W1Bt zZKzF&a6gP~5X`fMjKs@lN;sxYm2hoDwIQ)p869K%Xw2u9|BjBL#5+k` zTMJxtxBQ1;teD(Y40bqSSmP68qbPJ`)k3c`F%Gf-&&rK(SXQ+jalnw{lI12)X7Kgj zd4Ec|xm3ERE1yXwv%RTeA`a+W>R39RXwBw}`{F5&K&w)Eh7cI?hNr!bShNivuqygA zU`^e$-=6&5yR+@BZC!_bFH^{+gKT3B5MR_#r`FPB#$?pW_|+pisnjH8F<6jWu@l9g~fC&&HhX;J0_To{kz z-DI&COYU&IPza<}21#O3xJDxvMWce^B$E*y$ckIh42n#2m|9T`V+8*)gSOQqXO^7- z(KP0GzPN$`tiw_t{ST7I;XO5fV#2SkeMMVBB9W|wsFBSJ(&AZT>6BBt-bs5Lh_t?aFSVR;R67hIY?CMSv2h-Ep7P#@&e9ld@eK@x_oJnCU6Ex8@LUi|yr}Owm&Bt{Ij!Mw?w^oQ1Te`F@Knmv_A(juks^NZ=4-?)BcV z)-=T+Z9t?%`p`TyLluN$9VIX3j)_9v5^;)Cw%Z{OzMO6cf`h+#JEYxr!`lg;hu)j9 zpbJJU$@pNOvEwJrPD=c}aT{S!d*enj6FwX~%6fSOpuxh4qcRizRzieqEEo*bS$Prz z{QVwhkY7>)><4NEL8a9$LfiB;tViXW z*Q16E{D#kOJ$v?zAAVMJ8!fEJzZPok_!h4Ut-*s=5lSDHLu7}r9OY=PaXbbeQfib< zj@KGx7y2^TC`ZIom1@juWgn;ieyM%g8& z#4k0<@s_G`=2qqx=T??a*B3UIX4e{fjm_irwe`i7K3-z*`UOvCFyusI6 z`SHc|&Do{$V;h_Ei!0^3SLW*%Ha1od4GqZ|^`)hi!MT-7Epsg^E%Pmldb`X^)ms)? zHd~ee4P5(%-|jr~an4-hWf!@Axup#IK8O?Yo#&iEsa@x{=H1JPzH;^k$E38z_Hlk) z=ZUjCvrJ(B24$(w3VV0+JRhqJ8H4(%m!#JDRodC!cu)igQ*=;$JGgSQr)fI zqE4xM)V=CHbw9o`)9OL>ka}1>g4fJj@tb)}ol$R7kK;e{cJ&VRPW7aEN}a`*=3VOD zYF3?7b824I)p@m`E~rKIw7RI4)Frj7R@ADxtk%@J+EAP78FfWHtFEeR>RZ%%)O*$Y z)VHels}HDeQ(Nje^+EL^_3i4z>O0hTs*m6f@q&6$eN=sn_W6YR2kN`jcdP5_d(`*h z0q_si_p48;A5cH2KBYdben|Zz^~35%)Q_qkQ$Magqi(35P(P_YtA0v-PW@x`)9Po` zOX_FUKT-cw{WJBl`seEB)c>MBuU=9AtNMBM3+fluFR5QvzoLFseL?-2`WNb7s(+<^ zUHxnI8|vSvo9dSOP4!#qx7EK@zoULv{X6wV^(FOt>ffvXP5lS;AJzY^eqa58x~=|D z{U7R&)E}!qQGcrbO#LVIW%U*Hf2#ki{#^Zq`Y-Cgs=ri!rCwEkt^S+(@9J;V|4?65 z|Cjo|)z{S5)!!N|tf*q!(EbdVe{GzaTqABI4A1b5q>(bx28K~1i$OMT6pU7*XtWva zM#<Wt=r;jCUFDHfD`;#+)&4)Q$7Tf^orEG@dpt8cW6{W7$|S zR*lQXnz3$d7@Nj3#uejPZN`@Iobf^9L&mooA2zE!NM^&92uet<26- z+OQ~HS+B1}&TTH(bF)kJ<@wn)kHXTx;xaUKad{!!TiM)LpxG9Dxqe{1zP!Fjlh&QN z3-!5+1DqezrEq^~aeX7f{xfSU%esZOccgW^<}bQs+~yuFFn3{XBy5tJ6Abb#HEQZEmSPaDH)VsXiYx_E>Bdn#Zzt9OHeK7MJUO z<6vVq(b!#Inq9x3Z@Ia+!LXQJn|HYT?3%o(Ik&X9x_XrZR5N^aDf#Sg&g<7*qIDDD z?&hlO#Pm*-^{t+mTUlC~T@9~v*;!c|xWsXb);>p#GHfr^m+8O7^|{S;SsLXhIpnil zon2oa(8IYNZ|>65a*F)KBUZ1*=ho`;)O(Ia+v*%<8%-891seQ6p z+8EG7di$4+TKLP(oEczI=EhWMc4=U9`I-9K;`zn;eCdtOE5GJPslu+SbFX_s?`w{p z-&|%EGoW@JT>Lvv>UzyDODhYzuFSsP@2`E2&E@sY)zy`?jrzP7UO@}2uPoIY*R!{= zxV*`PxI|0(+o$M*+q<;W>_R;i{wm$Nvb1#IH_zZLFy4xHm|yZ0fdD~-3+zcZV5|GYw-+-5~qR%5!z!`3fC*S04N@A%B(998Gt z)@BEuS)8x0@Q%BVHTN#9oLgL~yYq|Z&ksPv>+=a+TwGX&5YSO_oGGQpX86-u{SuXE zoVQkA<`K*c&avF4>xufM)s3qIR~DBc_AyOLt@^Wb zOPlj`xBl$v?DD*(3KSVA9N7@!$S`s1R~xi!K0?txU$4(g%f+El^!VcP?AldFmxV64 zxpE!usYp-ez;Do)34gUSgh*s9Frtdf`JK+tkEv`moFD75> z9^V_RC2Sy&X1EtSzeH0w=UGK`KUli7$#op@HNUP z)zy0J0&TNlU7%g)v*-mDy5xnGwZ&_Y5UA-I{TritD;u%J<#Q{~Mi-aQuUL!A>#KBf zd~tmpBBS5Z56f%yM$7Bnb#sxMEY6uv%j~}zeR_Rm*}qsnH+ybC-f)oxJ#w*rHL^5& z#bb1HQlnSh#vZfZ42y+u^oPGMZd^Ubq9-rj`Z~w;0-kLAFvkj2Xa4z(eO9bZE)E*I z%#-@kKzLI2j$==6u5T=!znZ?|pgb~j#}WOo#O_1QTdzYZn$>LHx_L}rm1&|U1F;+G=R?aUz>uewK^kkD+y~e5+mA$y|H!?st#)(p1n%zj~ z(#jfBMj9a;|4Z~9v>-fdW365ff7pal>GRwrn5cpE3(N;g7zH>idufFc#YHZKi{Z)= zm7;lRc44``;ar+sl$kO+AC;0VOrLO}&ZYVSqjY7tZV9u%4WiNoF+IhcOF{!S_|d$y zD9m8u62ywG)m%YTsAKBV=F-OEDx@i-bnDSen;Ug|xqd~@1y>jJG`A?qYUM7k3^a<- z<&}+kTE2u29oT?m(j;8nIAX6rs?N{O)e|yo2Ugdh>-8&%m9>T0<;83Ibxk^Cl|EU8 zM6z7ktFtUCbF<5F&GLj~D=KA|`NjAa(r<=EXLS)uOCxSXRu`8O{D&q9f!w%ihC6Yp zb9Er(?xIrWYjeS)9x%W3fN-@|qgJWaH8@P+ZU@#cZ%WUsuB|*xN5-I0>vda`D4I8R zd6Tz`uhDBlF|IHe=oQ`H>v3o^T|B^~TQ|dUlwq;rLJk-o%X9U0iz1J|5L>G+)Spet z5`}=mDgsAXU*jU#*PCZ}NS#WvIKpLcoi20T>e5wixVj?ra=FeeD55Umyw%P13v!X( zzgVBAW|W1-HcRUlsL<*P50GVxYa5jJ!tC-wojNn%>KmE0l@&&JxDJE_C%)@YWDSmU zZS&k!2Oec$_8gd#zrM05?J4}!+R9RDeRYYoYKLz7;ejTR zwHYu>ulkZJJkx+?92{MgmkUc5W|z*#MWSmA$He;8ONem;$bqw0{l*Tn2ytV%`P&@w z$olq<$PCHGiBydHFK=WT`^@-Dtg4q-wc@)DHLtBdLxVMU;N6$zn`g;-mug(W#H+8# zY;_w47{<+-QM|&)_8Pxjs&8Ca*}lmoxT)q%gvnZGGSi0P3sN%#hPh_V8BS}ntcA_< z;R(2c2RBckKRIRNYO}hsM6NY&w!SRu>_)R1>l { - const connParams: RpcConnectParams = { uri } - const result: RpcConnected = await client.sendRequest('$/lean/rpc/connect', connParams) - return result.sessionId -} - -class RpcSessionAtPos implements Disposable { - keepAliveInterval?: NodeJS.Timeout - client: LeanClient - - constructor (client: LeanClient, public sessionId: string, public uri: ls.DocumentUri) { - this.client = client - this.keepAliveInterval = setInterval(async () => { - const params: RpcKeepAliveParams = { uri, sessionId } - try { - await client.sendNotification('$/lean/rpc/keepAlive', params) - } catch (e) { - console.log(`[InfoProvider] failed to send keepalive for ${uri}: ${e}`) - if (this.keepAliveInterval != null) clearInterval(this.keepAliveInterval) - } - }, keepAlivePeriodMs) - } - - dispose () { - if (this.keepAliveInterval != null) clearInterval(this.keepAliveInterval) - // TODO: at this point we could close the session - } -} - -export class InfoProvider implements Disposable { - /** Instance of the panel, if it is open. Otherwise `undefined`. */ - private infoviewApi?: InfoviewApi - private editor?: monaco.editor.IStandaloneCodeEditor - private readonly subscriptions: Disposable[] = [] - private readonly clientSubscriptions: Disposable[] = [] - - public readonly client?: LeanClient - // private readonly clientProvider: LeanClientProvider - - // Subscriptions are counted and only disposed of when count becomes 0. - private readonly serverNotifSubscriptions: Map = new Map() - private readonly clientNotifSubscriptions: Map = new Map() - - private rpcSessions: Map = new Map() - - // the key is the uri of the file who's worker has failed. - private readonly workersFailed: Map = new Map() - - private subscribeDidChangeNotification (client: LeanClient, method: string) { - const h = client.didChange((params) => { - void this.infoviewApi?.sentClientNotification(method, params) - }) - return h - } - - private subscribeDidCloseNotification (client: LeanClient, method: string) { - const h = client.didClose((params) => { - void this.infoviewApi?.sentClientNotification(method, params) - }) - return h - } - - private subscribeDiagnosticsNotification (client: LeanClient, method: string) { - const h = client.diagnostics((params) => { - void this.infoviewApi?.gotServerNotification(method, params) - }) - return h - } - - private subscribeCustomNotification (client: LeanClient, method: string) { - const h = client.customNotification(({ method: thisMethod, params }) => { - if (thisMethod !== method) return - void this.infoviewApi?.gotServerNotification(method, params) - }) - return h - } - - private readonly editorApi: EditorApi = { - sendClientRequest: async (uri: string, method: string, params: any): Promise => { - const client = this.client // clientProvider.findClient(uri) - if (client != null) { - try { - const result = await client.sendRequest(method, params) - return result - } catch (ex: any) { - if (ex.code === RpcErrorCode.WorkerCrashed) { - // ex codes related with worker exited or crashed - console.log(`[InfoProvider]The Lean Server has stopped processing this file: ${ex.message}`) - await this.onWorkerStopped(uri, client, { message: 'The Lean Server has stopped processing this file: ', reason: ex.message as string }) - } - throw ex - } - } - return undefined - }, - sendClientNotification: async (uri: string, method: string, params: any): Promise => { - const client = this.client // this.clientProvider.findClient(uri) - if (client != null) { - await client.sendNotification(method, params) - } - }, - subscribeServerNotifications: async (method) => { - const el = this.serverNotifSubscriptions.get(method) - if (el != null) { - const [count, h] = el - this.serverNotifSubscriptions.set(method, [count + 1, h]) - return - } - - // NOTE(WN): For non-custom notifications we cannot call LanguageClient.onNotification - // here because that *overwrites* the notification handler rather than registers an extra one. - // So we have to add a bunch of event emitters to `LeanClient.` - if (method === 'textDocument/publishDiagnostics') { - const subscriptions: Disposable[] = [] - for (const client of [this.client]/* this.clientProvider.getClients() */) { - subscriptions.push(this.subscribeDiagnosticsNotification(client!, method)) - } - this.serverNotifSubscriptions.set(method, [1, subscriptions]) - } else if (method.startsWith('$')) { - const subscriptions: Disposable[] = [] - for (const client of [this.client]/* this.clientProvider.getClients() */) { - subscriptions.push(this.subscribeCustomNotification(client!, method)) - } - this.serverNotifSubscriptions.set(method, [1, subscriptions]) - } else { - throw new Error(`subscription to ${method} server notifications not implemented`) - } - }, - unsubscribeServerNotifications: async (method) => { - const el = this.serverNotifSubscriptions.get(method) - if (el == null) return - const [count, subscriptions] = el - if (count === 1) { - for (const h of subscriptions) { - h.dispose() - } - this.serverNotifSubscriptions.delete(method) - } else { - this.serverNotifSubscriptions.set(method, [count - 1, subscriptions]) - } - }, - - subscribeClientNotifications: async (method) => { - const el = this.clientNotifSubscriptions.get(method) - if (el != null) { - const [count, d] = el - this.clientNotifSubscriptions.set(method, [count + 1, d]) - return - } - - if (method === 'textDocument/didChange') { - const subscriptions: Disposable[] = [] - for (const client of [this.client]/* this.clientProvider.getClients() */) { - subscriptions.push(this.subscribeDidChangeNotification(client!, method)) - } - this.clientNotifSubscriptions.set(method, [1, subscriptions]) - } else if (method === 'textDocument/didClose') { - const subscriptions: Disposable[] = [] - for (const client of [this.client]/* this.clientProvider.getClients() */) { - subscriptions.push(this.subscribeDidCloseNotification(client!, method)) - } - this.clientNotifSubscriptions.set(method, [1, subscriptions]) - } else { - throw new Error(`Subscription to '${method}' client notifications not implemented`) - } - }, - - unsubscribeClientNotifications: async (method) => { - const el = this.clientNotifSubscriptions.get(method) - if (el == null) return - const [count, subscriptions] = el - if (count === 1) { - for (const d of subscriptions) { - d.dispose() - } - this.clientNotifSubscriptions.delete(method) - } else { - this.clientNotifSubscriptions.set(method, [count - 1, subscriptions]) - } - }, - copyToClipboard: async (text) => { - navigator.clipboard.writeText(text) - }, - insertText: async (text, kind, tdpp) => { - let uri: Uri | undefined - let pos: Position | undefined - if (tdpp != null) { - uri = p2cConverter.asUri(tdpp.textDocument.uri) - pos = fromLanguageServerPosition(tdpp.position) - } - await this.handleInsertText(text, kind, uri, pos) - }, - applyEdit: async (e: ls.WorkspaceEdit) => { - const we = await p2cConverter.asWorkspaceEdit(e) - await workspace.applyEdit(we) - }, - showDocument: async (show) => { - void this.revealEditorSelection( - Uri.parse(show.uri), - fromLanguageServerRange(show.selection) - ) - }, - restartFile: async uri => { - - return // TODO! - - - // const extUri = parseExtUri(uri) - // if (extUri === undefined) { - // return - // } - - // const client = this.clientProvider.findClient(extUri) - // if (!client) { - // return - // } - - // const document = workspace.textDocuments.find(doc => extUri.equalsUri(doc.uri)) - // if (!document || document.isClosed) { - // return - // } - - // await client.restartFile(document) - }, - createRpcSession: async uri => { - const client = this.client // this.clientProvider.findClient(uri) - if (client == null) return '' - const sessionId = await rpcConnect(client, uri) - const session = new RpcSessionAtPos(client, sessionId, uri) - // if (this.webviewPanel == null) { - // session.dispose() - // throw Error('infoview disconnect while connecting to RPC session') - // } else { - this.rpcSessions.set(sessionId, session) - return sessionId - // } - }, - closeRpcSession: async sessionId => { - const session = this.rpcSessions.get(sessionId) - if (session != null) { - this.rpcSessions.delete(sessionId) - session.dispose() - } - } - } - - constructor (private readonly myclient: LeanClient | undefined) { - // this.clientProvider = provider - this.client = myclient - - this.onClientAdded(this.client!) - - this.subscriptions.push( - window.onDidChangeActiveTextEditor(async () => await this.sendPosition()), - window.onDidChangeTextEditorSelection(async () => await this.sendPosition()), - workspace.onDidChangeConfiguration(async (_e) => { - // regression; changing the style needs a reload. :/ - await this.sendConfig() - }), - workspace.onDidChangeTextDocument(async () => { - await this.sendPosition() - }) - ) - } - - private async onClientRestarted (client: LeanClient) { - // if we already have subscriptions for a previous client, we need to also - // subscribe to the same things on this new client. - for (const [method, [count, subscriptions]] of this.clientNotifSubscriptions) { - if (method === 'textDocument/didChange') { - subscriptions.push(this.subscribeDidChangeNotification(client, method)) - } else if (method === 'textDocument/didClose') { - subscriptions.push(this.subscribeDidCloseNotification(client, method)) - } - } - - for (const [method, [count, subscriptions]] of this.serverNotifSubscriptions) { - if (method === 'textDocument/publishDiagnostics') { - subscriptions.push(this.subscribeDiagnosticsNotification(client, method)) - } else if (method.startsWith('$')) { - subscriptions.push(this.subscribeCustomNotification(client, method)) - } - } - - await this.initInfoView(this.editor, client) - } - - private async onClientAdded (client: LeanClient) { - console.log(`[InfoProvider] Adding client`) - - this.clientSubscriptions.push( - client.restarted(async () => { - console.log('[InfoProvider] got client restarted event') - // This event is triggered both the first time the server starts - // as well as when the server restarts. - - this.clearRpcSessions(client) - - // Need to fully re-initialize this newly restarted client with all the - // existing subscriptions and resend position info and so on so the - // infoview updates properly. - await this.onClientRestarted(client) - }), - client.restartedWorker(async (uri) => { - console.log('[InfoProvider] got worker restarted event') - await this.onWorkerRestarted(uri) - }), - client.didSetLanguage(() => this.onLanguageChanged()) - ) - - // Note that when new client is first created it still fires client.restarted - // event, so all onClientRestarted can happen there so we don't do it twice. - } - - async onWorkerRestarted (uri: string): Promise { - await this.infoviewApi?.serverStopped(undefined) // clear any server stopped state - if (this.workersFailed.has(uri)) { - this.workersFailed.delete(uri) - console.log('[InfoProvider] Restarting worker for file: ' + uri) - } - await this.sendPosition() - } - - async onWorkerStopped (uri: string, client: LeanClient, reason: any) { - await this.infoviewApi?.serverStopped(reason) - - if (!this.workersFailed.has(uri)) { - this.workersFailed.set(uri, reason) - } - console.log(`[InfoProvider]client crashed: ${uri}`) - await client.showRestartMessage() - } - - onClientRemoved (client: LeanClient) { - // todo: remove subscriptions for this client... - } - - async onActiveClientStopped (client: LeanClient, activeClient: boolean, reason: any) { - // Will show a message in case the active client stops - // add failed client into a list (will be removed in case the client is restarted) - if (activeClient) { - // means that client and active client are the same and just show the error message - await this.infoviewApi?.serverStopped(reason) - } - - console.log(`[InfoProvider] client stopped`) - - await client.showRestartMessage() - } - - dispose (): void { - // active client is changing. - this.clearNotificationHandlers() - this.clearRpcSessions(null) - for (const s of this.clientSubscriptions) { s.dispose() } - for (const s of this.subscriptions) { s.dispose() } - } - - isOpen (): boolean { - return /* this.webviewPanel?.visible === */ true - } - - async runTestScript (javaScript: string): Promise { - if (this.infoviewApi != null) { - return await this.infoviewApi.runTestScript(javaScript) - } else { - throw new Error('Cannot run test script, infoview is closed.') - } - } - - async getHtmlContents (): Promise { - if (this.infoviewApi != null) { - return await this.infoviewApi.getInfoviewHtml() - } else { - throw new Error('Cannot retrieve infoview HTML, infoview is closed.') - } - } - - async sleep (ms: number) { - return await new Promise((resolve) => setTimeout(resolve, ms)) - } - - async toggleAllMessages (): Promise { - if (this.infoviewApi != null) { - await this.infoviewApi.requestedAction({ kind: 'toggleAllMessages' }) - } - } - - private clearNotificationHandlers () { - for (const [, [, subscriptions]] of this.clientNotifSubscriptions) { for (const h of subscriptions) h.dispose() } - this.clientNotifSubscriptions.clear() - for (const [, [, subscriptions]] of this.serverNotifSubscriptions) { for (const h of subscriptions) h.dispose() } - this.serverNotifSubscriptions.clear() - } - - private clearRpcSessions (client: LeanClient | null) { - const remaining = new Map() - for (const [sessionId, sess] of this.rpcSessions) { - if (client === null || sess.client === client) { - sess.dispose() - } else { - remaining.set(sessionId, sess) - } - } - this.rpcSessions = remaining - } - - getApi () { - return this.editorApi - } - - async openPreview (editor: monaco.editor.IStandaloneCodeEditor, infoviewApi: InfoviewApi) { - this.infoviewApi = infoviewApi - this.editor = editor - await this.initInfoView(editor, this.client!) - } - - private async initInfoView (editor: monaco.editor.IStandaloneCodeEditor | undefined, client: LeanClient | null) { - if (editor != null) { - const loc = this.getLocation(editor) - if (loc != null) { - console.log('initialize infoview api') - await this.infoviewApi?.initialize(loc) - } - } - - // The infoview gets information about file progress, diagnostics, etc. - // by listening to notifications. Send these notifications when the infoview starts - // so that it has up-to-date information. - if ((client?.initializeResult) != null) { - await this.infoviewApi?.serverStopped(undefined) // clear any server stopped state - await this.infoviewApi?.serverRestarted(client.initializeResult) - await this.sendDiagnostics(client) - await this.sendProgress(client) - await this.sendPosition() - await this.sendConfig() - } - } - - private async sendConfig () { - await this.infoviewApi?.changedInfoviewConfig({ - allErrorsOnLine: true, //getInfoViewAllErrorsOnLine(), - autoOpenShowsGoal: true, // getInfoViewAllErrorsOnLine(), - debounceTime: 50, // getInfoViewAutoOpenShowGoal() - - // TODO: I set all of these to false to get things working, - // but what would be correct? - showExpectedType: false, - showGoalNames: false, - emphasizeFirstGoal: false, - reverseTacticState: false, - showTooltipOnHover: false, - }) - } - - private async sendDiagnostics (client: LeanClient) { - if (this.infoviewApi !== undefined) { - client.getDiagnostics()?.forEach(async (uri, diags) => { - const params = client.getDiagnosticParams(uri, diags) - await this.infoviewApi!.gotServerNotification('textDocument/publishDiagnostics', params) - }) - } - } - - private async sendProgress (client: LeanClient) { - if (this.infoviewApi == null) return - for (const [uri, processing] of client.progress) { - const params: LeanFileProgressParams = { - textDocument: { - uri: c2pConverter.asUri(uri), - version: 0 // HACK: The infoview ignores this - }, - processing - } - await this.infoviewApi.gotServerNotification('$/lean/fileProgress', params) - } - } - - private onLanguageChanged () { - this.sendPosition().then(() => this.sendConfig()) - } - - private getLocation (editor: monaco.editor.IStandaloneCodeEditor): ls.Location | undefined { - if (!editor) return undefined - const uri = editor.getModel()?.uri - const selection = editor.getSelection()! - return { - uri: uri!.toString(), - range: toLanguageServerRange(selection) - } - } - - private async sendPosition () { - const editor = this.editor - if (editor == null) return - const loc = this.getLocation(editor) - if (!this.client.running){ - await this.infoviewApi?.serverStopped(undefined) - } else if (this.workersFailed.size > 0) { - const uri = window.activeTextEditor?.document.uri.toString() ?? '' - let reason: any | undefined - if (this.workersFailed.has(uri)) { - reason = this.workersFailed.get(uri) - } - if (reason) { - // send stopped event - await this.infoviewApi?.serverStopped(reason) - } else { - await this.updateStatus(loc) - } - } else { - await this.updateStatus(loc) - } - } - - private async updateStatus (loc: ls.Location | undefined): Promise { - await this.infoviewApi?.changedCursorLocation(loc) - } - - private async revealEditorSelection (uri: Uri, selection?: monaco.Range) { - if (this.editor == null) { - console.error("Editor not set") - return - } - if (selection !== undefined) { - this.editor.revealRange(selection)//TextEditorRevealType.InCenterIfOutsideViewport - this.editor.setSelection(selection) - // ensure the text document has the keyboard focus. - this.editor.focus() - } - } - - private async handleInsertText (text: string, kind: TextInsertKind, uri?: Uri, pos?: monaco.Position) { - if (this.editor == null) { - return - } - pos = (pos != null) ? pos : this.editor.getSelection().getStartPosition() - if (kind === 'above') { - // in this case, assume that we actually want to insert at the same - // indentation level as the neighboring text - const spaces = this.editor.getModel().getLineFirstNonWhitespaceColumn(pos.lineNumber) - 1 - const margin_str = [...Array(spaces).keys()].map(x => ' ').join('') - let new_command = text.replace(/\n/g, '\n' + margin_str) - new_command = `${margin_str}${new_command}\n` - const insertPosition = monaco.Range.fromPositions({lineNumber: pos.lineNumber, column: 0}) - - await this.editor.pushUndoStop() - await this.editor.executeEdits( - "infoview", - [{ range: insertPosition, text: new_command, forceMoveMarkers: true }], - ) - } else { - if (pos != null) { - await this.editor.pushUndoStop() - await this.editor.executeEdits( - "infoview", - [{ range: monaco.Range.fromPositions(pos), text: text, forceMoveMarkers: true }], - ) - } - } - this.editor.focus() - } -} diff --git a/client/src/editor/leanclient.ts b/client/src/editor/leanclient.ts deleted file mode 100644 index 40618101..00000000 --- a/client/src/editor/leanclient.ts +++ /dev/null @@ -1,343 +0,0 @@ -/* This file is based on `vscode-lean4/src/leanclient.ts` */ - -import { - TextDocument, EventEmitter, Diagnostic, - DocumentHighlight, Range, DocumentHighlightKind, - Disposable, Uri, DiagnosticCollection, - WorkspaceFolder, workspace -} from 'vscode' -import { - DidChangeTextDocumentParams, - DidCloseTextDocumentParams, - InitializeResult, - MonacoLanguageClient as LanguageClient, - LanguageClientOptions, - PublishDiagnosticsParams, - CloseAction, ErrorAction, IConnectionProvider, -} from 'monaco-languageclient' -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import { State } from 'vscode-languageclient' -import * as ls from 'vscode-languageserver-protocol' - -import { getElaborationDelay } from './config' -import { LeanFileProgressParams, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api' -import { c2pConverter, p2cConverter, patchConverters } from './utils/converters' - -const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&') - -export type ServerProgress = Map - -export function getFullRange (diag: Diagnostic): Range { - return (diag as any)?.fullRange || diag.range -} - -export class LeanClient implements Disposable { - running: boolean = false - private client: LanguageClient | undefined - private noPrompt: boolean = false - - private readonly didChangeEmitter = new EventEmitter() - didChange = this.didChangeEmitter.event - - private readonly diagnosticsEmitter = new EventEmitter() - diagnostics = this.diagnosticsEmitter.event - - private readonly didSetLanguageEmitter = new EventEmitter() - didSetLanguage = this.didSetLanguageEmitter.event - - private readonly didCloseEmitter = new EventEmitter() - didClose = this.didCloseEmitter.event - - private readonly customNotificationEmitter = new EventEmitter<{ method: string, params: any }>() - /** Fires whenever a custom notification (i.e. one not defined in LSP) is received. */ - customNotification = this.customNotificationEmitter.event - - /** saved progress info in case infoview is opened, it needs to get all of it. */ - progress: ServerProgress = new Map() - - private readonly progressChangedEmitter = new EventEmitter<[string, LeanFileProgressProcessingInfo[]]>() - progressChanged = this.progressChangedEmitter.event - - private readonly stoppedEmitter = new EventEmitter() - stopped = this.stoppedEmitter.event - - private readonly restartedEmitter = new EventEmitter() - restarted = this.restartedEmitter.event - - private readonly restartingEmitter = new EventEmitter() - restarting = this.restartingEmitter.event - - private readonly restartedWorkerEmitter = new EventEmitter() - restartedWorker = this.restartedWorkerEmitter.event - - private readonly serverFailedEmitter = new EventEmitter() - serverFailed = this.serverFailedEmitter.event - - constructor ( - private readonly connectionProvider: IConnectionProvider, - public readonly showRestartMessage: () => void, - private readonly initializationOptions = {}) { - - } - - dispose (): void { - if (this.client.isRunning()) { - this.client.dispose() - } else { - this.client.onDidChangeState((ev) => { - if (ev.newState == State.Running) { - setTimeout(() => { // Wait for client to send `initialized` before `shutdown` - this.client.dispose() - }, 0) - } - }) - } - } - - async restart (project): Promise { - const startTime = Date.now() - - if (!project) { - project = 'mathlib-demo' - } - - console.log(`[LeanClient] Restarting Lean Server with project ${project}`) - if (this.isStarted()) { - // TODO: This times out in lean4game... - await this.stop() - } - - this.restartingEmitter.fire(undefined) - - const clientOptions: LanguageClientOptions = { - // use a language id as a document selector - documentSelector: ['lean4'], - workspaceFolder: {uri: "hello"}, - initializationOptions: { - editDelay: getElaborationDelay(), - hasWidgets: true, - ...this.initializationOptions - }, - connectionOptions: { - maxRestartCount: 0, - cancellationStrategy: undefined as any - }, - // disable the default error handler - errorHandler: { - error: () => { this.showRestartMessage(); return { action: ErrorAction.Continue }}, - closed: () => ({ action: CloseAction.DoNotRestart }) - }, - middleware: { - handleDiagnostics: (uri, diagnostics, next) => { - next(uri, diagnostics) - if (this.client == null) return - const uri_ = c2pConverter.asUri(uri) - const diagnostics_ = [] - for (const d of diagnostics) { - const d_: ls.Diagnostic = { - ...c2pConverter.asDiagnostic(d) - } - diagnostics_.push(d_) - } - this.diagnosticsEmitter.fire({ uri: uri_, diagnostics: diagnostics_ }) - }, - - // Closing does not work properly, so we deactivate it here: - didClose: async (data, next) => {}, - - didChange: async (data, next) => { - await next(data) - if (!this.running || (this.client == null)) return // there was a problem starting lean server. - const params = c2pConverter.asChangeTextDocumentParams(data) - this.didChangeEmitter.fire(params) - }, - - provideDocumentHighlights: async (doc, pos, ctok, next) => { - const leanHighlights = await next(doc, pos, ctok) - if (leanHighlights?.length) return leanHighlights - - // vscode doesn't fall back to textual highlights, - // so we need to do that manually - await new Promise((res) => setTimeout(res, 250)) - if (ctok.isCancellationRequested) return - - const wordRange = doc.getWordRangeAtPosition(pos) - if (wordRange == null) return - const word = doc.getText(wordRange) - - const highlights: DocumentHighlight[] = [] - const text = doc.getText() - const nonWordPattern = '[`~@$%^&*()-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\\\|;:\",./\\s]|^|$' - const regexp = new RegExp(`(?<=${nonWordPattern})${escapeRegExp(word)}(?=${nonWordPattern})`, 'g') - for (const match of text.matchAll(regexp)) { - const start = doc.positionAt(match.index ?? 0) - highlights.push({ - range: new Range(start, start.translate(0, match[0].length)), - kind: DocumentHighlightKind.Text - }) - } - - return highlights - } - } - } - if (!this.client) { - this.client = new LanguageClient({ - id: 'lean4', - name: 'Lean 4', - clientOptions, - connectionProvider: this.connectionProvider - }) - } - - // HACK: Prevent monaco from panicking when the Lean server crashes - this.client.handleFailedRequest = (type, token: any, error: any, defaultValue, showNotification?: boolean) => { - return defaultValue - } - - let insideRestart = true - patchConverters(this.client.protocol2CodeConverter, this.client.code2ProtocolConverter) - try { - this.client.onDidChangeState(async (s) => { - // see https://github.com/microsoft/vscode-languageserver-node/issues/825 - if (s.newState === State.Starting) { - console.log('[LeanClient] starting') - } else if (s.newState === State.Running) { - const end = Date.now() - console.log(`[LeanClient] running, started in ${end - startTime} ms`) - this.running = true // may have been auto restarted after it failed. - if (!insideRestart) { - this.restartedEmitter.fire() - } - } else if (s.newState === State.Stopped) { - this.running = false - console.log('[LeanClient] has stopped or it failed to start') - if (!this.noPrompt) { - // only raise this event and show the message if we are not the ones - // who called the stop() method. - this.stoppedEmitter.fire({ message: 'Lean server has stopped.', reason: '' }) - } - } - }) - await this.client.start() - this.running = true - } catch (error) { - console.log(error) - this.serverFailedEmitter.fire('' + error) - insideRestart = false - return - } - - // HACK(WN): Register a default notification handler to fire on custom notifications. - // A mechanism to do this is provided in vscode-jsonrpc. One can register a `StarNotificationHandler` - // here: https://github.com/microsoft/vscode-languageserver-node/blob/b2fc85d28a1a44c22896559ee5f4d3ba37a02ef5/jsonrpc/src/common/connection.ts#L497 - // which fires on any LSP notifications not in the standard, for example the `$/lean/..` ones. - // However this mechanism is not exposed in vscode-languageclient, so we hack around its implementation. - const starHandler = (method: string, params_: any) => { - if (method === '$/lean/fileProgress' && (this.client != null)) { - const params = params_ as LeanFileProgressParams - const uri = p2cConverter.asUri(params.textDocument.uri) - this.progressChangedEmitter.fire([uri.toString(), params.processing]) - // save the latest progress on this Uri in case infoview needs it later. - this.progress.set(uri, params.processing) - } - - this.customNotificationEmitter.fire({ method, params: params_ }) - } - // eslint-disable-next-line @typescript-eslint/no-unsafe-argument - this.client.onNotification(starHandler as any, () => {}) - - this.restartedEmitter.fire({project: project}) - insideRestart = false - } - - // async start (project): Promise { - // return await this.restart(project) - // } - - isStarted (): boolean { - return this.client !== undefined - } - - isRunning (): boolean { - if (this.client != null) { - return this.running - } - return false - } - - async stop (): Promise { - // assert(() => this.isStarted()) - if ((this.client != null) && this.running) { - this.noPrompt = true - try { - // some timing conditions can happen while running unit tests that cause - // this to throw an exception which then causes those tests to fail. - await this.client.stop() - } catch (e) { - console.log(`[LeanClient] Error stopping language client: ${e}`) - } - } - - this.noPrompt = false - this.progress = new Map() - this.client = undefined - this.running = false - } - - async restartFile (doc: TextDocument): Promise { - if (!this.running) return // there was a problem starting lean server. - - const uri = doc.uri.toString() - console.log(`[LeanClient] Restarting File: ${uri}`) - // This causes a text document version number discontinuity. In - // (didChange (oldVersion) => restartFile => didChange (newVersion)) - // the client emits newVersion = oldVersion + 1, despite the fact that the - // didOpen packet emitted below initializes the version number to be 1. - // This is not a problem though, since both client and server are fine - // as long as the version numbers are monotonous. - void this.client?.sendNotification('textDocument/didClose', { - textDocument: { - uri - } - }) - void this.client?.sendNotification('textDocument/didOpen', { - textDocument: { - uri, - languageId: 'lean4', - version: 1, - text: doc.getText() - } - }) - this.restartedWorkerEmitter.fire(uri) - } - - // eslint-disable-next-line @typescript-eslint/explicit-module-boundary-types - async sendRequest (method: string, params: any): Promise { - return this.running && (this.client != null) - ? await this.client.sendRequest(method, params) - : await new Promise((_, reject) => { reject('Client is not running') }) - } - - // eslint-disable-next-line @typescript-eslint/explicit-module-boundary-types - sendNotification (method: string, params: any): Promise | undefined { - return this.running && (this.client != null) ? this.client.sendNotification(method, params) : undefined - } - - async getDiagnosticParams (uri: Uri, diagnostics: readonly Diagnostic[]): Promise { - const params: PublishDiagnosticsParams = { - uri: c2pConverter.asUri(uri), - diagnostics: await c2pConverter.asDiagnostics(diagnostics as Diagnostic[]) - } - return params - } - - getDiagnostics (): DiagnosticCollection | undefined { - return this.running ? this.client?.diagnostics : undefined - } - - get initializeResult (): InitializeResult | undefined { - return this.running ? this.client?.initializeResult : undefined - } - -} diff --git a/client/src/editor/taskgutter.ts b/client/src/editor/taskgutter.ts deleted file mode 100644 index 0490eb3d..00000000 --- a/client/src/editor/taskgutter.ts +++ /dev/null @@ -1,119 +0,0 @@ -/* This file is based on `vscode-lean4/src/taskgutter.ts` */ - -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import { LeanFileProgressKind, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api'; -import { LeanClient } from './leanclient'; -import { fromLanguageServerRange } from './utils/converters'; - -class LeanFileTaskGutter { - private timeout?: NodeJS.Timeout - private decoIds: string[] = [] - - constructor(private editor: monaco.editor.IStandaloneCodeEditor, private decorations: Map, private processed: LeanFileProgressProcessingInfo[]) { - this.schedule(100) - } - - setProcessed(processed: LeanFileProgressProcessingInfo[]) { - if (processed === this.processed) return; - const oldProcessed = this.processed; - this.processed = processed; - if (processed === undefined) { - this.processed = [] - this.clearTimeout(); - this.updateDecos(); - } else if (this.timeout === undefined) { - this.schedule(oldProcessed === undefined ? 500 : 20) - } - } - - private schedule(ms: number) { - this.timeout = setTimeout(() => { - this.timeout = undefined - this.updateDecos() - }, ms) - } - - private clearTimeout() { - if (this.timeout !== undefined) { - clearTimeout(this.timeout) - this.timeout = undefined; - } - } - - private updateDecos() { - this.decoIds = this.editor.getModel().deltaDecorations(this.decoIds, - this.processed - .map(info => ({ - options: this.decorations.get(info.kind === undefined ? LeanFileProgressKind.Processing : info.kind), - range : fromLanguageServerRange(info.range) - })) - ) - } - - dispose() { - this.clearTimeout(); - } -} - -export class LeanTaskGutter { - private decorations: Map = - new Map(); - private status: { [uri: string]: LeanFileProgressProcessingInfo[] } = {}; - private gutters: { [uri: string]: LeanFileTaskGutter | undefined } = {}; - private subscriptions: any[] = []; - - constructor(private client: LeanClient, private editor: monaco.editor.IStandaloneCodeEditor) { - this.decorations.set(LeanFileProgressKind.Processing, - { - overviewRuler: { - position: monaco.editor.OverviewRulerLane.Left, - color: 'rgba(255, 165, 0, 0.5)', - }, - glyphMarginClassName: 'processing', - hoverMessage: {value: 'busily processing...'} - }) - this.decorations.set(LeanFileProgressKind.FatalError, - { - overviewRuler: { - position: monaco.editor.OverviewRulerLane.Left, - color: 'rgba(255, 0, 0, 0.5)', - }, - glyphMarginClassName: 'glyph-margin-error', - hoverMessage: {value: 'processing stopped'} - }, - ) - - this.subscriptions.push( - client.progressChanged(([uri, processing]) => { - this.status[uri.toString()] = processing - this.updateDecos() - })); - } - - private updateDecos() { - const uris: { [uri: string]: boolean } = {} - // for (const editor of window.visibleTextEditors) { - const uri = this.editor.getModel().uri.toString(); - uris[uri] = true - const processed = uri in this.status ? this.status[uri] : [] - if (this.gutters[uri]) { - const gutter = this.gutters[uri]; - if (gutter) gutter.setProcessed(processed) - } else { - this.gutters[uri] = new LeanFileTaskGutter(this.editor, this.decorations, processed) - } - // } - for (const uri of Object.getOwnPropertyNames(this.gutters)) { - if (!uris[uri]) { - this.gutters[uri]?.dispose(); - this.gutters[uri] = undefined; - // TODO: also clear this.status for this uri ? - } - } - } - - dispose(): void { - // for (const decoration of this.decorations.values()) { decoration.dispose() } - for (const s of this.subscriptions) { s.dispose(); } - } -} diff --git a/client/src/editor/utils/converters.ts b/client/src/editor/utils/converters.ts deleted file mode 100644 index ab4cce07..00000000 --- a/client/src/editor/utils/converters.ts +++ /dev/null @@ -1,76 +0,0 @@ -/* This file is based on `vscode-lean4/src/utils/converters.ts` */ - -/** - * For LSP communication, we need a way to translate between LSP types and corresponding VSCode types. - * By default this translation is provided as a bunch of methods on a `LanguageClient`, but this is - * awkward to use in multi-client workspaces wherein we need to look up specific clients. In fact the - * conversions are *not* stateful, so having them depend on the client is unnecessary. Instead, we - * provide global converters here. - * - * Some of the conversions are patched to support extended Lean-specific structures. - * - * @module - */ - -import { createConverter as createP2CConverter } from 'vscode-languageclient/lib/common/protocolConverter' -import { createConverter as createC2PConverter } from 'vscode-languageclient/lib/common/codeConverter' -import * as ls from 'vscode-languageserver-protocol' -import * as code from 'vscode' -import { Code2ProtocolConverter, Protocol2CodeConverter } from 'vscode-languageclient' -import { MonacoLanguageClient} from 'monaco-languageclient/.' -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' - -interface Lean4Diagnostic extends ls.Diagnostic { - fullRange: ls.Range -} - -export const p2cConverter = createP2CConverter(undefined, true, true) -export const c2pConverter = createC2PConverter(undefined) - -export function patchConverters (p2cConverter: Protocol2CodeConverter, c2pConverter: Code2ProtocolConverter) { - // eslint-disable-next-line @typescript-eslint/unbound-method - const oldAsDiagnostic = p2cConverter.asDiagnostic - p2cConverter.asDiagnostic = function (protDiag: Lean4Diagnostic): code.Diagnostic { - if (!protDiag.message) { - // Fixes: Notification handler 'textDocument/publishDiagnostics' failed with message: message must be set - protDiag.message = ' ' - } - const diag = oldAsDiagnostic.apply(this, [protDiag]) - // diag.fullRange = p2cConverter.asRange(protDiag.fullRange) - return diag - } - p2cConverter.asDiagnostics = async (diags) => diags.map(d => p2cConverter.asDiagnostic(d)) - - // eslint-disable-next-line @typescript-eslint/unbound-method - const c2pAsDiagnostic = c2pConverter.asDiagnostic - c2pConverter.asDiagnostic = function (diag: code.Diagnostic & { fullRange: code.Range }): Lean4Diagnostic { - const protDiag = c2pAsDiagnostic.apply(this, [diag]) - return { ...protDiag, fullRange: c2pConverter.asRange(diag.fullRange) } - } - c2pConverter.asDiagnostics = async (diags) => diags.map(d => c2pConverter.asDiagnostic(d)) -} - -patchConverters(p2cConverter, c2pConverter) - -export function toLanguageServerRange (range: monaco.Range): ls.Range { - return { - start: { line: range.startLineNumber - 1, character: range.startColumn - 1}, - end: { line: range.endLineNumber - 1, character: range.endColumn - 1} - } -} - -export function fromLanguageServerPosition (pos: ls.Position): monaco.Position { - return new monaco.Position( - pos.line + 1, - pos.character + 1 - ) -} - -export function fromLanguageServerRange (range: ls.Range): monaco.Range { - return new monaco.Range( - range.start.line + 1, - range.start.character + 1, - range.end.line + 1, - range.end.character + 1 - ) -} diff --git a/client/src/monacoSetup.ts b/client/src/monacoSetup.ts index 493b9d4d..4dc13434 100644 --- a/client/src/monacoSetup.ts +++ b/client/src/monacoSetup.ts @@ -3,7 +3,7 @@ import { wireTmGrammars } from 'monaco-editor-textmate' import * as leanSyntax from './syntaxes/lean.json' import * as leanMarkdownSyntax from './syntaxes/lean-markdown.json' import * as codeblockSyntax from './syntaxes/codeblock.json' -import languageConfig from '../vscode-lean4/vscode-lean4/language-configuration.json'; +import languageConfig from '../monaco-lean4/vscode-lean4/language-configuration.json'; import { loadWASM } from 'onigasm' import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { MonacoServices } from 'monaco-languageclient'; diff --git a/client/vscode-lean4 b/client/vscode-lean4 deleted file mode 160000 index a4d92e5c..00000000 --- a/client/vscode-lean4 +++ /dev/null @@ -1 +0,0 @@ -Subproject commit a4d92e5c9354bfe4a92d915208137a5e98d43689