This repository was archived by the owner on Apr 2, 2025. It is now read-only.
Refactor so that all vscode-specific infoview stuff is in vscode_info_server.ts#204
Draft
EdAyers wants to merge 9 commits intoleanprover:masterfrom
Draft
Refactor so that all vscode-specific infoview stuff is in vscode_info_server.ts#204EdAyers wants to merge 9 commits intoleanprover:masterfrom
vscode_info_server.ts#204EdAyers wants to merge 9 commits intoleanprover:masterfrom
Conversation
This is to maximise code reuse with the lean-web-editor project. All code that is specific to vscode is now in extension.ts. So it should only be necessary to implement this file to get the system to work in lean-web-editor. Additionally: - index.tsx has been split in to Main.tsx and index.tsx. index.tsx is vscode specific - Main has been split in to `Main` and `InfoView` components. This is to separate the stateful parts of Main. - onPin is now optional, if onPin is not provided then Info will not show the pin button - rename DOM id `react_root` to `infoview_root`
gebner
reviewed
Jul 8, 2020
It's an abstraction that tells you what the editor needs to implement to get infoviews to work. Note that config and position are not included as events, they should be passed in as props.
- Remove extension.ts - Move types needed by lean-web-editor to types.ts - Move trythis.ts to infoview - Change rootDir of tsconfig from `./src` to `.` - Hardcode copy-to-comment svg in to infoview code. This means there is duplication but there is already duplication for the light/dark versions. Seems neater to just have all the svgs inline. Also means we can remove dependency on webpack svg loader.
EdAyers
changed the title
extension.tsvscode_info_server.ts
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A refactoring, no new functionality.
This is to maximise code reuse with the lean-web-editor project.
All code that is specific to vscode is now in
infoview/vscode_info_server.tsandinfoview/index.tsx, which contains an instance ofInfoServer.So it should only be necessary to re-implement this file to get the infoview system
to work in lean-web-editor.
Additionally:
show the pin button
react_roottoinfoview_rootsince lean-web-editor uses React and so react_root is no longer the roottodo