Skip to content

Commit

Permalink
Merge pull request #3 from leanprover-community/vite
Browse files Browse the repository at this point in the history
feat: change from webpack to vite
  • Loading branch information
joneugster authored Oct 27, 2023
2 parents b02044f + d98daa9 commit 149f1c7
Show file tree
Hide file tree
Showing 18 changed files with 1,933 additions and 5,164 deletions.
2 changes: 2 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,5 @@ node_modules
client/dist
server/build
client/public/package_versions.json
dist
**/.DS_Store
Binary file removed client/public/onigasm.wasm
Binary file not shown.
2 changes: 1 addition & 1 deletion client/src/App.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import PrivacyPolicy from './PrivacyPolicy'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import { faUpload, faArrowRotateRight, faArrowUpRightFromSquare, faDownload, faBars, faXmark } from '@fortawesome/free-solid-svg-icons'
const Editor = React.lazy(() => import('./Editor'))
import Logo from "./logo.svg";
import { ReactComponent as Logo } from './assets/logo.svg'
import { saveAs } from 'file-saver';
import LoadUrl from './LoadUrl'
import Settings from './Settings'
Expand Down
2 changes: 1 addition & 1 deletion client/src/logo.svg → client/src/assets/logo.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
1 change: 1 addition & 0 deletions client/src/css/App.css
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@
/* The Lean logo */
.nav .logo {
height: 2.2rem;
width: unset;
vertical-align: middle;
margin-left: .5rem;
margin-right: 1rem;
Expand Down
8 changes: 5 additions & 3 deletions client/src/custom.d.ts
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
declare module "*.svg" {
const content: any;
export default content;
declare module '*.svg' {
import React = require('react')
export const ReactComponent: React.FC<React.SVGProps<SVGSVGElement>>
const src: string
export default src
}
1 change: 0 additions & 1 deletion client/src/editor/abbreviation/AbbreviationProvider.ts
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@ export class AbbreviationProvider {
// );
}

@computed
private get symbolsByAbbreviation(): SymbolsByAbbreviation {
// There are only like 1000 symbols. Building an index is not required yet.
return {
Expand Down
7 changes: 3 additions & 4 deletions client/src/editor/infoview.css
Original file line number Diff line number Diff line change
Expand Up @@ -401,7 +401,7 @@ button, select {/* 1 */ text-transform: none; }
/**
* Correct the inability to style clickable types in iOS and Safari.
*/
button, [type="button"], [type="reset"], [type="submit"] { -webkit-appearance: button; }
button, [type="button"], [type="reset"], [type="submit"] { appearance: button; -webkit-appearance: button; }
/**
* Remove the inner border and padding in Firefox.
*/
Expand Down Expand Up @@ -445,7 +445,7 @@ textarea { overflow: auto; }
* 1. Correct the odd appearance in Chrome and Safari.
* 2. Correct the outline style in Safari.
*/
[type="search"] { -webkit-appearance: textfield; /* 1 */ outline-offset: -2px; /* 2 */ }
[type="search"] { appearance: textfield; -webkit-appearance: textfield; /* 1 */ outline-offset: -2px; /* 2 */ }
/**
* Remove the inner padding in Chrome and Safari on macOS.
*/
Expand Down Expand Up @@ -867,7 +867,6 @@ Media Query Extensions:
Ref: http://nicolasgallagher.com/micro-clearfix-hack/ */
.cf:before, .cf:after { content: " "; display: table; }
.cf:after { clear: both; }
.cf { *zoom: 1; }
.cl { clear: left; }
.cr { clear: right; }
.cb { clear: both; }
Expand Down Expand Up @@ -1078,7 +1077,7 @@ code, .code { font-family: Consolas, monaco, monospace; }
FORMS
*/
.input-reset { -webkit-appearance: none; -moz-appearance: none; }
.input-reset { appearance: none; -webkit-appearance: none; -moz-appearance: none; }
.button-reset::-moz-focus-inner, .input-reset::-moz-focus-inner { border: 0; padding: 0; }
/*
Expand Down
26 changes: 13 additions & 13 deletions client/src/editor/leanclient.ts
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ import {
PublishDiagnosticsParams,
CloseAction, ErrorAction,
RevealOutputChannelOn,
State
} from 'monaco-languageclient'
import { State } from 'vscode-languageclient'
import * as ls from 'vscode-languageserver-protocol'
import { toSocket, WebSocketMessageReader, WebSocketMessageWriter } from 'vscode-ws-jsonrpc'

Expand Down Expand Up @@ -606,16 +606,16 @@ export class LeanClient implements Disposable {
// return false
// }

private extractVersion (v: string | undefined): SemVer {
if (!v) return new SemVer('0.0.0')
const prefix = 'Lake version'
if (v.startsWith(prefix)) v = v.slice(prefix.length).trim()
const pos = v.indexOf('(')
if (pos > 0) v = v.slice(0, pos).trim()
try {
return new SemVer(v)
} catch {
return new SemVer('0.0.0')
}
}
// private extractVersion (v: string | undefined): SemVer {
// if (!v) return new SemVer('0.0.0')
// const prefix = 'Lake version'
// if (v.startsWith(prefix)) v = v.slice(prefix.length).trim()
// const pos = v.indexOf('(')
// if (pos > 0) v = v.slice(0, pos).trim()
// try {
// return new SemVer(v)
// } catch {
// return new SemVer('0.0.0')
// }
// }
}
4 changes: 3 additions & 1 deletion client/src/monacoSetup.ts
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
import { MonacoServices } from 'monaco-languageclient';
import { StandaloneServices } from 'vscode/services';
import getMessageServiceOverride from 'vscode/service-override/messages';
//@ts-ignore
import onigasmUrl from 'onigasm/lib/onigasm.wasm?url'

export function monacoSetup () {

Expand Down Expand Up @@ -62,7 +64,7 @@ export function monacoSetup () {
// Load onigasm
(async () => {
try {
await loadWASM('./onigasm.wasm')
await loadWASM(onigasmUrl)
} catch (err) {
// Hot module replacement can cause us to run this code twice and that's ok.
if (!(err as Error).message?.startsWith('Onigasm#init has been called')) {
Expand Down
2 changes: 1 addition & 1 deletion client/public/index.html → index.html
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
+49 211 81-12173<br />
</p>
</noscript>
<script src="bundle.js"></script>
<script type="module" src="/client/src/index.tsx"></script>
</body>

</html>
Loading

0 comments on commit 149f1c7

Please sign in to comment.