Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: change from webpack to vite #3

Merged
merged 14 commits into from
Oct 27, 2023
Merged

feat: change from webpack to vite #3

Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
60ee990
vite
abentkamp Oct 21, 2023
edf8478
copy automatically
abentkamp Oct 21, 2023
a35381d
repair state import
abentkamp Oct 21, 2023
c9d04c4
ignore olean
abentkamp Oct 21, 2023
020157d
remove webpack
abentkamp Oct 21, 2023
0a475a7
fix path
abentkamp Oct 22, 2023
8f05f02
reenable logo
joneugster Oct 24, 2023
5ea37b4
drop IE6/7 support and drop build warning
joneugster Oct 24, 2023
ab0a394
path-browserify
abentkamp Oct 24, 2023
3b98f40
change port to 3000
joneugster Oct 25, 2023
783bc6c
get logo working
joneugster Oct 27, 2023
10386bd
fix typescript error for svg import
joneugster Oct 27, 2023
b93d449
npm update
joneugster Oct 27, 2023
d98daa9
add svg logo; modify gitignore; removepublic/index.html
joneugster Oct 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,4 @@ node_modules
client/dist
server/build
client/public/package_versions.json
dist
Binary file removed client/public/onigasm.wasm
View file
Open in desktop
Binary file not shown.
1 change: 0 additions & 1 deletion client/src/editor/abbreviation/AbbreviationProvider.ts
View file
Open in desktop
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
26 changes: 13 additions & 13 deletions client/src/editor/leanclient.ts
View file
Open in desktop
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')
// }
// }
joneugster marked this conversation as resolved.
Show resolved Hide resolved
}
4 changes: 3 additions & 1 deletion client/src/monacoSetup.ts
View file
Open in desktop
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
28 changes: 28 additions & 0 deletions index.html
View file
Open in desktop
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I thought files from client/public are copied to the server. Why do we need this copy?

Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
<!DOCTYPE html>
<html>

<head>
<meta charset="UTF-8" />
<title>Lean 4 Web</title>
<meta name="viewport" content="width=device-width, initial-scale=1.0">
</head>

<body>
<div id="root"></div>
<noscript>
<p>You need to enable JavaScript to use the lean4web editor, as it is a <a href="https://react.dev">React app</a>.</p>
<p>Contact details:</p>
<p>
<a href="https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/dr-alexander-bentkamp">Alexander Bentkamp</a>,&nbsp;
<a href="https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Jon Eugster</a><br />
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
Universitätsstr. 1<br />
40225 Düsseldorf<br />
Germany<br />
+49 211 81-12173<br />
</p>
</noscript>
<script type="module" src="/client/src/index.tsx"></script>
</body>

</html>
Loading